Theorem nfrsucc-P8 1119

Description: If '𝑥' is ENF in a term '𝑡', then '𝑥' is also ENF in its successor, 's‘𝑡'. †

Hypothesis

Ref	Expression
nfrsucc-P8.1	⊢ Ⅎt𝑥 𝑡

Assertion

Ref	Expression
nfrsucc-P8	⊢ Ⅎt𝑥 s‘𝑡

Proof of Theorem nfrsucc-P8

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

Step	Hyp	Ref	Expression
1		ndnfrv-P7.1 826	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 = s‘𝑧
2	1	rcp-NDIMP0addall 207	. . . . 5 ⊢ (𝑧 = 𝑡 → Ⅎ𝑥 𝑦 = s‘𝑧)
3		nfrsucc-P8.1	. . . . . . . 8 ⊢ Ⅎt𝑥 𝑡
4		df-nfreet-D8.1 1116	. . . . . . . 8 ⊢ (Ⅎt𝑥 𝑡 ↔ ∀𝑧Ⅎ𝑥 𝑧 = 𝑡)
5	3, 4	bimpf-P4.RC 532	. . . . . . 7 ⊢ ∀𝑧Ⅎ𝑥 𝑧 = 𝑡
6	5	alle-P7r.RC 993	. . . . . 6 ⊢ Ⅎ𝑥 𝑧 = 𝑡
7		ndsubsucc-P7.24a.CL 917	. . . . . . 7 ⊢ (𝑧 = 𝑡 → s‘𝑧 = s‘𝑡)
8	7	ndsubeqr-P7.22b 848	. . . . . 6 ⊢ (𝑧 = 𝑡 → (𝑦 = s‘𝑧 ↔ 𝑦 = s‘𝑡))
9	6, 8	ndnfrleq-P7.11 836	. . . . 5 ⊢ (𝑧 = 𝑡 → (Ⅎ𝑥 𝑦 = s‘𝑧 ↔ Ⅎ𝑥 𝑦 = s‘𝑡))
10	2, 9	bimpf-P4 531	. . . 4 ⊢ (𝑧 = 𝑡 → Ⅎ𝑥 𝑦 = s‘𝑡)
11		axL6ex-P7 925	. . . 4 ⊢ ∃𝑧 𝑧 = 𝑡
12	10, 11	exe-P7r.RC.VR 1003	. . 3 ⊢ Ⅎ𝑥 𝑦 = s‘𝑡
13	12	axGEN-P7 933	. 2 ⊢ ∀𝑦Ⅎ𝑥 𝑦 = s‘𝑡
14		df-nfreet-D8.1 1116	. 2 ⊢ (Ⅎt𝑥 s‘𝑡 ↔ ∀𝑦Ⅎ𝑥 𝑦 = s‘𝑡)
15	13, 14	bimpr-P4.RC 534	1 ⊢ Ⅎt𝑥 s‘𝑡

Syntax hints:  term-obj 1  s‘term_succ 3   = wff-equals 6  ∀wff-forall 8  Ⅎ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-succ 22  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)