Theorem nfradd-P8 1120

Description: If '𝑥' is ENF in the terms '𝑡₁' and '𝑡₂', then '𝑥' is ENF in the sum term, '(𝑡₁ + 𝑡₂)'. †

Hypotheses

Ref	Expression
nfradd-P8.1	⊢ Ⅎt𝑥 𝑡₁
nfradd-P8.2	⊢ Ⅎt𝑥 𝑡₂

Assertion

Ref	Expression
nfradd-P8	⊢ Ⅎt𝑥(𝑡₁ + 𝑡₂)

Proof of Theorem nfradd-P8

Dummy variables 𝑦 𝑧₁ 𝑧₂ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ndnfrv-P7.1 826	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑦 = (𝑧₁ + 𝑧₂)
2	1	rcp-NDIMP0addall 207	. . . . . . 7 ⊢ ((𝑧₁ = 𝑡₁ ∧ 𝑧₂ = 𝑡₂) → Ⅎ𝑥 𝑦 = (𝑧₁ + 𝑧₂))
3		nfradd-P8.1	. . . . . . . . . . 11 ⊢ Ⅎt𝑥 𝑡₁
4		df-nfreet-D8.1 1116	. . . . . . . . . . 11 ⊢ (Ⅎt𝑥 𝑡₁ ↔ ∀𝑧₁Ⅎ𝑥 𝑧₁ = 𝑡₁)
5	3, 4	bimpf-P4.RC 532	. . . . . . . . . 10 ⊢ ∀𝑧₁Ⅎ𝑥 𝑧₁ = 𝑡₁
6	5	alle-P7r.RC 993	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧₁ = 𝑡₁
7		nfradd-P8.2	. . . . . . . . . . 11 ⊢ Ⅎt𝑥 𝑡₂
8		df-nfreet-D8.1 1116	. . . . . . . . . . 11 ⊢ (Ⅎt𝑥 𝑡₂ ↔ ∀𝑧₂Ⅎ𝑥 𝑧₂ = 𝑡₂)
9	7, 8	bimpf-P4.RC 532	. . . . . . . . . 10 ⊢ ∀𝑧₂Ⅎ𝑥 𝑧₂ = 𝑡₂
10	9	alle-P7r.RC 993	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧₂ = 𝑡₂
11	6, 10	ndnfrand-P7.4.RC 877	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑧₁ = 𝑡₁ ∧ 𝑧₂ = 𝑡₂)
12		ndsubaddd-P7.CL 920	. . . . . . . . 9 ⊢ ((𝑧₁ = 𝑡₁ ∧ 𝑧₂ = 𝑡₂) → (𝑧₁ + 𝑧₂) = (𝑡₁ + 𝑡₂))
13	12	ndsubeqr-P7.22b 848	. . . . . . . 8 ⊢ ((𝑧₁ = 𝑡₁ ∧ 𝑧₂ = 𝑡₂) → (𝑦 = (𝑧₁ + 𝑧₂) ↔ 𝑦 = (𝑡₁ + 𝑡₂)))
14	11, 13	ndnfrleq-P7.11 836	. . . . . . 7 ⊢ ((𝑧₁ = 𝑡₁ ∧ 𝑧₂ = 𝑡₂) → (Ⅎ𝑥 𝑦 = (𝑧₁ + 𝑧₂) ↔ Ⅎ𝑥 𝑦 = (𝑡₁ + 𝑡₂)))
15	2, 14	bimpf-P4 531	. . . . . 6 ⊢ ((𝑧₁ = 𝑡₁ ∧ 𝑧₂ = 𝑡₂) → Ⅎ𝑥 𝑦 = (𝑡₁ + 𝑡₂))
16	15	rcp-NDIMI2 224	. . . . 5 ⊢ (𝑧₁ = 𝑡₁ → (𝑧₂ = 𝑡₂ → Ⅎ𝑥 𝑦 = (𝑡₁ + 𝑡₂)))
17		axL6ex-P7 925	. . . . 5 ⊢ ∃𝑧₁ 𝑧₁ = 𝑡₁
18	16, 17	exe-P7r.RC.VR 1003	. . . 4 ⊢ (𝑧₂ = 𝑡₂ → Ⅎ𝑥 𝑦 = (𝑡₁ + 𝑡₂))
19		axL6ex-P7 925	. . . 4 ⊢ ∃𝑧₂ 𝑧₂ = 𝑡₂
20	18, 19	exe-P7r.RC.VR 1003	. . 3 ⊢ Ⅎ𝑥 𝑦 = (𝑡₁ + 𝑡₂)
21	20	axGEN-P7 933	. 2 ⊢ ∀𝑦Ⅎ𝑥 𝑦 = (𝑡₁ + 𝑡₂)
22		df-nfreet-D8.1 1116	. 2 ⊢ (Ⅎt𝑥(𝑡₁ + 𝑡₂) ↔ ∀𝑦Ⅎ𝑥 𝑦 = (𝑡₁ + 𝑡₂))
23	21, 22	bimpr-P4.RC 534	1 ⊢ Ⅎt𝑥(𝑡₁ + 𝑡₂)

Syntax hints:  term-obj 1   + term-add 4   = wff-equals 6  ∀wff-forall 8   → wff-imp 10   ∧ wff-and 132  Ⅎwff-nfree 681  Ⅎ_twff-nfreet 1114

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19  ax-L9-addl 23  ax-L9-addr 24  ax-L10 27  ax-L11 28  ax-L12 29

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596  df-nfree-D6.1 682  df-psub-D6.2 716  df-nfreet-D8.1 1116

This theorem is referenced by: (None)