Metamath Proof Explorer

Theorem ttrclselem2

Description: Lemma for ttrclse . Show that a suc N element long chain gives membership in the N -th predecessor class and vice-versa. (Contributed by Scott Fenton, 31-Oct-2024)

Ref Expression
Hypothesis ttrclselem.1 ⊢F=rec⁡b∈V⟼⋃w∈bPredRAwPredRAX
Assertion ttrclselem2 ⊢N∈ω∧RSeA∧X∈A→∃ffFnsuc⁡suc⁡N∧f⁡∅=y∧f⁡suc⁡N=X∧∀a∈suc⁡Nf⁡aR↾Af⁡suc⁡a↔y∈F⁡N

Proof

Step Hyp Ref Expression
1 ttrclselem.1 ⊢F=rec⁡b∈V⟼⋃w∈bPredRAwPredRAX
2 suceq ⊢m=∅→suc⁡m=suc⁡∅
3 df-1o ⊢1𝑜=suc⁡∅
4 2 3 eqtr4di ⊢m=∅→suc⁡m=1𝑜
5 suceq ⊢suc⁡m=1𝑜→suc⁡suc⁡m=suc⁡1𝑜
6 4 5 syl ⊢m=∅→suc⁡suc⁡m=suc⁡1𝑜
7 6 fneq2d ⊢m=∅→fFnsuc⁡suc⁡m↔fFnsuc⁡1𝑜
8 4 fveqeq2d ⊢m=∅→f⁡suc⁡m=X↔f⁡1𝑜=X
9 8 anbi2d ⊢m=∅→f⁡∅=y∧f⁡suc⁡m=X↔f⁡∅=y∧f⁡1𝑜=X
10 df1o2 ⊢1𝑜=∅
11 4 10 eqtrdi ⊢m=∅→suc⁡m=∅
12 11 raleqdv ⊢m=∅→∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔∀a∈∅f⁡aR↾Af⁡suc⁡a
13 0ex ⊢∅∈V
14 fveq2 ⊢a=∅→f⁡a=f⁡∅
15 suceq ⊢a=∅→suc⁡a=suc⁡∅
16 15 3 eqtr4di ⊢a=∅→suc⁡a=1𝑜
17 16 fveq2d ⊢a=∅→f⁡suc⁡a=f⁡1𝑜
18 14 17 breq12d ⊢a=∅→f⁡aR↾Af⁡suc⁡a↔f⁡∅R↾Af⁡1𝑜
19 13 18 ralsn ⊢∀a∈∅f⁡aR↾Af⁡suc⁡a↔f⁡∅R↾Af⁡1𝑜
20 12 19 bitrdi ⊢m=∅→∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔f⁡∅R↾Af⁡1𝑜
21 7 9 20 3anbi123d ⊢m=∅→fFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔fFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜
22 21 exbidv ⊢m=∅→∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜
23 fveq2 ⊢m=∅→F⁡m=F⁡∅
24 23 eleq2d ⊢m=∅→y∈F⁡m↔y∈F⁡∅
25 22 24 bibi12d ⊢m=∅→∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔y∈F⁡m↔∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜↔y∈F⁡∅
26 25 albidv ⊢m=∅→∀y∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔y∈F⁡m↔∀y∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜↔y∈F⁡∅
27 26 imbi2d ⊢m=∅→RSeA∧X∈A→∀y∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔y∈F⁡m↔RSeA∧X∈A→∀y∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜↔y∈F⁡∅
28 suceq ⊢m=n→suc⁡m=suc⁡n
29 suceq ⊢suc⁡m=suc⁡n→suc⁡suc⁡m=suc⁡suc⁡n
30 28 29 syl ⊢m=n→suc⁡suc⁡m=suc⁡suc⁡n
31 30 fneq2d ⊢m=n→fFnsuc⁡suc⁡m↔fFnsuc⁡suc⁡n
32 28 fveqeq2d ⊢m=n→f⁡suc⁡m=X↔f⁡suc⁡n=X
33 32 anbi2d ⊢m=n→f⁡∅=y∧f⁡suc⁡m=X↔f⁡∅=y∧f⁡suc⁡n=X
34 28 raleqdv ⊢m=n→∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔∀a∈suc⁡nf⁡aR↾Af⁡suc⁡a
35 fveq2 ⊢a=c→f⁡a=f⁡c
36 suceq ⊢a=c→suc⁡a=suc⁡c
37 36 fveq2d ⊢a=c→f⁡suc⁡a=f⁡suc⁡c
38 35 37 breq12d ⊢a=c→f⁡aR↾Af⁡suc⁡a↔f⁡cR↾Af⁡suc⁡c
39 38 cbvralvw ⊢∀a∈suc⁡nf⁡aR↾Af⁡suc⁡a↔∀c∈suc⁡nf⁡cR↾Af⁡suc⁡c
40 34 39 bitrdi ⊢m=n→∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔∀c∈suc⁡nf⁡cR↾Af⁡suc⁡c
41 31 33 40 3anbi123d ⊢m=n→fFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔fFnsuc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡n=X∧∀c∈suc⁡nf⁡cR↾Af⁡suc⁡c
42 41 exbidv ⊢m=n→∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔∃ffFnsuc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡n=X∧∀c∈suc⁡nf⁡cR↾Af⁡suc⁡c
43 fneq1 ⊢f=g→fFnsuc⁡suc⁡n↔gFnsuc⁡suc⁡n
44 fveq1 ⊢f=g→f⁡∅=g⁡∅
45 44 eqeq1d ⊢f=g→f⁡∅=y↔g⁡∅=y
46 fveq1 ⊢f=g→f⁡suc⁡n=g⁡suc⁡n
47 46 eqeq1d ⊢f=g→f⁡suc⁡n=X↔g⁡suc⁡n=X
48 45 47 anbi12d ⊢f=g→f⁡∅=y∧f⁡suc⁡n=X↔g⁡∅=y∧g⁡suc⁡n=X
49 fveq1 ⊢f=g→f⁡c=g⁡c
50 fveq1 ⊢f=g→f⁡suc⁡c=g⁡suc⁡c
51 49 50 breq12d ⊢f=g→f⁡cR↾Af⁡suc⁡c↔g⁡cR↾Ag⁡suc⁡c
52 51 ralbidv ⊢f=g→∀c∈suc⁡nf⁡cR↾Af⁡suc⁡c↔∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c
53 43 48 52 3anbi123d ⊢f=g→fFnsuc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡n=X∧∀c∈suc⁡nf⁡cR↾Af⁡suc⁡c↔gFnsuc⁡suc⁡n∧g⁡∅=y∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c
54 53 cbvexvw ⊢∃ffFnsuc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡n=X∧∀c∈suc⁡nf⁡cR↾Af⁡suc⁡c↔∃ggFnsuc⁡suc⁡n∧g⁡∅=y∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c
55 42 54 bitrdi ⊢m=n→∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔∃ggFnsuc⁡suc⁡n∧g⁡∅=y∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c
56 fveq2 ⊢m=n→F⁡m=F⁡n
57 56 eleq2d ⊢m=n→y∈F⁡m↔y∈F⁡n
58 55 57 bibi12d ⊢m=n→∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔y∈F⁡m↔∃ggFnsuc⁡suc⁡n∧g⁡∅=y∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔y∈F⁡n
59 58 albidv ⊢m=n→∀y∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔y∈F⁡m↔∀y∃ggFnsuc⁡suc⁡n∧g⁡∅=y∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔y∈F⁡n
60 eqeq2 ⊢y=z→g⁡∅=y↔g⁡∅=z
61 60 anbi1d ⊢y=z→g⁡∅=y∧g⁡suc⁡n=X↔g⁡∅=z∧g⁡suc⁡n=X
62 61 3anbi2d ⊢y=z→gFnsuc⁡suc⁡n∧g⁡∅=y∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c
63 62 exbidv ⊢y=z→∃ggFnsuc⁡suc⁡n∧g⁡∅=y∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c
64 eleq1 ⊢y=z→y∈F⁡n↔z∈F⁡n
65 63 64 bibi12d ⊢y=z→∃ggFnsuc⁡suc⁡n∧g⁡∅=y∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔y∈F⁡n↔∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n
66 65 cbvalvw ⊢∀y∃ggFnsuc⁡suc⁡n∧g⁡∅=y∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔y∈F⁡n↔∀z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n
67 59 66 bitrdi ⊢m=n→∀y∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔y∈F⁡m↔∀z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n
68 67 imbi2d ⊢m=n→RSeA∧X∈A→∀y∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔y∈F⁡m↔RSeA∧X∈A→∀z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n
69 suceq ⊢m=suc⁡n→suc⁡m=suc⁡suc⁡n
70 suceq ⊢suc⁡m=suc⁡suc⁡n→suc⁡suc⁡m=suc⁡suc⁡suc⁡n
71 69 70 syl ⊢m=suc⁡n→suc⁡suc⁡m=suc⁡suc⁡suc⁡n
72 71 fneq2d ⊢m=suc⁡n→fFnsuc⁡suc⁡m↔fFnsuc⁡suc⁡suc⁡n
73 69 fveqeq2d ⊢m=suc⁡n→f⁡suc⁡m=X↔f⁡suc⁡suc⁡n=X
74 73 anbi2d ⊢m=suc⁡n→f⁡∅=y∧f⁡suc⁡m=X↔f⁡∅=y∧f⁡suc⁡suc⁡n=X
75 69 raleqdv ⊢m=suc⁡n→∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a
76 72 74 75 3anbi123d ⊢m=suc⁡n→fFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a
77 76 exbidv ⊢m=suc⁡n→∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a
78 fveq2 ⊢m=suc⁡n→F⁡m=F⁡suc⁡n
79 78 eleq2d ⊢m=suc⁡n→y∈F⁡m↔y∈F⁡suc⁡n
80 77 79 bibi12d ⊢m=suc⁡n→∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔y∈F⁡m↔∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔y∈F⁡suc⁡n
81 80 albidv ⊢m=suc⁡n→∀y∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔y∈F⁡m↔∀y∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔y∈F⁡suc⁡n
82 81 imbi2d ⊢m=suc⁡n→RSeA∧X∈A→∀y∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔y∈F⁡m↔RSeA∧X∈A→∀y∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔y∈F⁡suc⁡n
83 suceq ⊢m=N→suc⁡m=suc⁡N
84 suceq ⊢suc⁡m=suc⁡N→suc⁡suc⁡m=suc⁡suc⁡N
85 83 84 syl ⊢m=N→suc⁡suc⁡m=suc⁡suc⁡N
86 85 fneq2d ⊢m=N→fFnsuc⁡suc⁡m↔fFnsuc⁡suc⁡N
87 83 fveqeq2d ⊢m=N→f⁡suc⁡m=X↔f⁡suc⁡N=X
88 87 anbi2d ⊢m=N→f⁡∅=y∧f⁡suc⁡m=X↔f⁡∅=y∧f⁡suc⁡N=X
89 83 raleqdv ⊢m=N→∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔∀a∈suc⁡Nf⁡aR↾Af⁡suc⁡a
90 86 88 89 3anbi123d ⊢m=N→fFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔fFnsuc⁡suc⁡N∧f⁡∅=y∧f⁡suc⁡N=X∧∀a∈suc⁡Nf⁡aR↾Af⁡suc⁡a
91 90 exbidv ⊢m=N→∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔∃ffFnsuc⁡suc⁡N∧f⁡∅=y∧f⁡suc⁡N=X∧∀a∈suc⁡Nf⁡aR↾Af⁡suc⁡a
92 fveq2 ⊢m=N→F⁡m=F⁡N
93 92 eleq2d ⊢m=N→y∈F⁡m↔y∈F⁡N
94 91 93 bibi12d ⊢m=N→∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔y∈F⁡m↔∃ffFnsuc⁡suc⁡N∧f⁡∅=y∧f⁡suc⁡N=X∧∀a∈suc⁡Nf⁡aR↾Af⁡suc⁡a↔y∈F⁡N
95 94 albidv ⊢m=N→∀y∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔y∈F⁡m↔∀y∃ffFnsuc⁡suc⁡N∧f⁡∅=y∧f⁡suc⁡N=X∧∀a∈suc⁡Nf⁡aR↾Af⁡suc⁡a↔y∈F⁡N
96 95 imbi2d ⊢m=N→RSeA∧X∈A→∀y∃ffFnsuc⁡suc⁡m∧f⁡∅=y∧f⁡suc⁡m=X∧∀a∈suc⁡mf⁡aR↾Af⁡suc⁡a↔y∈F⁡m↔RSeA∧X∈A→∀y∃ffFnsuc⁡suc⁡N∧f⁡∅=y∧f⁡suc⁡N=X∧∀a∈suc⁡Nf⁡aR↾Af⁡suc⁡a↔y∈F⁡N
97 eqeq2 ⊢x=X→f⁡1𝑜=x↔f⁡1𝑜=X
98 97 anbi2d ⊢x=X→f⁡∅=y∧f⁡1𝑜=x↔f⁡∅=y∧f⁡1𝑜=X
99 98 anbi2d ⊢x=X→fFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=x↔fFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X
100 99 exbidv ⊢x=X→∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=x↔∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X
101 vex ⊢y∈V
102 vex ⊢x∈V
103 101 102 ifex ⊢ifb=∅yx∈V
104 eqid ⊢b∈suc⁡1𝑜⟼ifb=∅yx=b∈suc⁡1𝑜⟼ifb=∅yx
105 103 104 fnmpti ⊢b∈suc⁡1𝑜⟼ifb=∅yxFnsuc⁡1𝑜
106 equid ⊢y=y
107 equid ⊢x=x
108 106 107 pm3.2i ⊢y=y∧x=x
109 1oex ⊢1𝑜∈V
110 109 sucex ⊢suc⁡1𝑜∈V
111 110 mptex ⊢b∈suc⁡1𝑜⟼ifb=∅yx∈V
112 fneq1 ⊢f=b∈suc⁡1𝑜⟼ifb=∅yx→fFnsuc⁡1𝑜↔b∈suc⁡1𝑜⟼ifb=∅yxFnsuc⁡1𝑜
113 fveq1 ⊢f=b∈suc⁡1𝑜⟼ifb=∅yx→f⁡∅=b∈suc⁡1𝑜⟼ifb=∅yx⁡∅
114 1on ⊢1𝑜∈On
115 114 onordi ⊢Ord⁡1𝑜
116 0elsuc ⊢Ord⁡1𝑜→∅∈suc⁡1𝑜
117 iftrue ⊢b=∅→ifb=∅yx=y
118 117 104 101 fvmpt ⊢∅∈suc⁡1𝑜→b∈suc⁡1𝑜⟼ifb=∅yx⁡∅=y
119 115 116 118 mp2b ⊢b∈suc⁡1𝑜⟼ifb=∅yx⁡∅=y
120 113 119 eqtrdi ⊢f=b∈suc⁡1𝑜⟼ifb=∅yx→f⁡∅=y
121 120 eqeq1d ⊢f=b∈suc⁡1𝑜⟼ifb=∅yx→f⁡∅=y↔y=y
122 fveq1 ⊢f=b∈suc⁡1𝑜⟼ifb=∅yx→f⁡1𝑜=b∈suc⁡1𝑜⟼ifb=∅yx⁡1𝑜
123 109 sucid ⊢1𝑜∈suc⁡1𝑜
124 eqeq1 ⊢b=1𝑜→b=∅↔1𝑜=∅
125 124 ifbid ⊢b=1𝑜→ifb=∅yx=if1𝑜=∅yx
126 1n0 ⊢1𝑜≠∅
127 126 neii ⊢¬1𝑜=∅
128 127 iffalsei ⊢if1𝑜=∅yx=x
129 125 128 eqtrdi ⊢b=1𝑜→ifb=∅yx=x
130 129 104 102 fvmpt ⊢1𝑜∈suc⁡1𝑜→b∈suc⁡1𝑜⟼ifb=∅yx⁡1𝑜=x
131 123 130 ax-mp ⊢b∈suc⁡1𝑜⟼ifb=∅yx⁡1𝑜=x
132 122 131 eqtrdi ⊢f=b∈suc⁡1𝑜⟼ifb=∅yx→f⁡1𝑜=x
133 132 eqeq1d ⊢f=b∈suc⁡1𝑜⟼ifb=∅yx→f⁡1𝑜=x↔x=x
134 121 133 anbi12d ⊢f=b∈suc⁡1𝑜⟼ifb=∅yx→f⁡∅=y∧f⁡1𝑜=x↔y=y∧x=x
135 112 134 anbi12d ⊢f=b∈suc⁡1𝑜⟼ifb=∅yx→fFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=x↔b∈suc⁡1𝑜⟼ifb=∅yxFnsuc⁡1𝑜∧y=y∧x=x
136 111 135 spcev ⊢b∈suc⁡1𝑜⟼ifb=∅yxFnsuc⁡1𝑜∧y=y∧x=x→∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=x
137 105 108 136 mp2an ⊢∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=x
138 100 137 vtoclg ⊢X∈A→∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X
139 138 adantl ⊢RSeA∧X∈A→∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X
140 139 biantrurd ⊢RSeA∧X∈A→y∈A∧yRX↔∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧y∈A∧yRX
141 101 elpred ⊢X∈A→y∈PredRAX↔y∈A∧yRX
142 141 adantl ⊢RSeA∧X∈A→y∈PredRAX↔y∈A∧yRX
143 brres ⊢X∈A→yR↾AX↔y∈A∧yRX
144 143 adantl ⊢RSeA∧X∈A→yR↾AX↔y∈A∧yRX
145 144 anbi2d ⊢RSeA∧X∈A→∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧yR↾AX↔∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧y∈A∧yRX
146 140 142 145 3bitr4rd ⊢RSeA∧X∈A→∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧yR↾AX↔y∈PredRAX
147 df-3an ⊢fFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜↔fFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜
148 breq12 ⊢f⁡∅=y∧f⁡1𝑜=X→f⁡∅R↾Af⁡1𝑜↔yR↾AX
149 148 adantl ⊢fFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X→f⁡∅R↾Af⁡1𝑜↔yR↾AX
150 149 pm5.32i ⊢fFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜↔fFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧yR↾AX
151 147 150 bitri ⊢fFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜↔fFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧yR↾AX
152 151 exbii ⊢∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜↔∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧yR↾AX
153 19.41v ⊢∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧yR↾AX↔∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧yR↾AX
154 152 153 bitri ⊢∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜↔∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧yR↾AX
155 154 a1i ⊢RSeA∧X∈A→∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜↔∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧yR↾AX
156 1 fveq1i ⊢F⁡∅=rec⁡b∈V⟼⋃w∈bPredRAwPredRAX⁡∅
157 setlikespec ⊢X∈A∧RSeA→PredRAX∈V
158 157 ancoms ⊢RSeA∧X∈A→PredRAX∈V
159 rdg0g ⊢PredRAX∈V→rec⁡b∈V⟼⋃w∈bPredRAwPredRAX⁡∅=PredRAX
160 158 159 syl ⊢RSeA∧X∈A→rec⁡b∈V⟼⋃w∈bPredRAwPredRAX⁡∅=PredRAX
161 156 160 eqtrid ⊢RSeA∧X∈A→F⁡∅=PredRAX
162 161 eleq2d ⊢RSeA∧X∈A→y∈F⁡∅↔y∈PredRAX
163 146 155 162 3bitr4d ⊢RSeA∧X∈A→∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜↔y∈F⁡∅
164 163 alrimiv ⊢RSeA∧X∈A→∀y∃ffFnsuc⁡1𝑜∧f⁡∅=y∧f⁡1𝑜=X∧f⁡∅R↾Af⁡1𝑜↔y∈F⁡∅
165 eliun ⊢y∈⋃z∈F⁡nPredRAz↔∃z∈F⁡ny∈PredRAz
166 df-rex ⊢∃z∈F⁡ny∈PredRAz↔∃zz∈F⁡n∧y∈PredRAz
167 165 166 bitri ⊢y∈⋃z∈F⁡nPredRAz↔∃zz∈F⁡n∧y∈PredRAz
168 101 elpred ⊢z∈V→y∈PredRAz↔y∈A∧yRz
169 168 elv ⊢y∈PredRAz↔y∈A∧yRz
170 169 anbi2i ⊢z∈F⁡n∧y∈PredRAz↔z∈F⁡n∧y∈A∧yRz
171 anbi1 ⊢∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n→∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz↔z∈F⁡n∧y∈A∧yRz
172 170 171 bitr4id ⊢∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n→z∈F⁡n∧y∈PredRAz↔∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
173 172 alexbii ⊢∀z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n→∃zz∈F⁡n∧y∈PredRAz↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
174 173 3ad2ant3 ⊢n∈ω∧RSeA∧X∈A∧∀z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n→∃zz∈F⁡n∧y∈PredRAz↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
175 167 174 bitrid ⊢n∈ω∧RSeA∧X∈A∧∀z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n→y∈⋃z∈F⁡nPredRAz↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
176 nnon ⊢n∈ω→n∈On
177 fvex ⊢F⁡n∈V
178 1 ttrclselem1 ⊢n∈ω→F⁡n⊆A
179 178 adantr ⊢n∈ω∧RSeA→F⁡n⊆A
180 dfse3 ⊢RSeA↔∀z∈APredRAz∈V
181 180 biimpi ⊢RSeA→∀z∈APredRAz∈V
182 181 adantl ⊢n∈ω∧RSeA→∀z∈APredRAz∈V
183 ssralv ⊢F⁡n⊆A→∀z∈APredRAz∈V→∀z∈F⁡nPredRAz∈V
184 179 182 183 sylc ⊢n∈ω∧RSeA→∀z∈F⁡nPredRAz∈V
185 184 adantrr ⊢n∈ω∧RSeA∧X∈A→∀z∈F⁡nPredRAz∈V
186 iunexg ⊢F⁡n∈V∧∀z∈F⁡nPredRAz∈V→⋃z∈F⁡nPredRAz∈V
187 177 185 186 sylancr ⊢n∈ω∧RSeA∧X∈A→⋃z∈F⁡nPredRAz∈V
188 nfcv ⊢Ⅎ_bPredRAX
189 nfcv ⊢Ⅎ_bn
190 nfmpt1 ⊢Ⅎ_bb∈V⟼⋃w∈bPredRAw
191 190 188 nfrdg ⊢Ⅎ_brec⁡b∈V⟼⋃w∈bPredRAwPredRAX
192 1 191 nfcxfr ⊢Ⅎ_bF
193 192 189 nffv ⊢Ⅎ_bF⁡n
194 nfcv ⊢Ⅎ_bPredRAz
195 193 194 nfiun ⊢Ⅎ_b⋃z∈F⁡nPredRAz
196 predeq3 ⊢w=z→PredRAw=PredRAz
197 196 cbviunv ⊢⋃w∈bPredRAw=⋃z∈bPredRAz
198 iuneq1 ⊢b=F⁡n→⋃z∈bPredRAz=⋃z∈F⁡nPredRAz
199 197 198 eqtrid ⊢b=F⁡n→⋃w∈bPredRAw=⋃z∈F⁡nPredRAz
200 188 189 195 1 199 rdgsucmptf ⊢n∈On∧⋃z∈F⁡nPredRAz∈V→F⁡suc⁡n=⋃z∈F⁡nPredRAz
201 176 187 200 syl2an2r ⊢n∈ω∧RSeA∧X∈A→F⁡suc⁡n=⋃z∈F⁡nPredRAz
202 201 3adant3 ⊢n∈ω∧RSeA∧X∈A∧∀z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n→F⁡suc⁡n=⋃z∈F⁡nPredRAz
203 202 eleq2d ⊢n∈ω∧RSeA∧X∈A∧∀z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n→y∈F⁡suc⁡n↔y∈⋃z∈F⁡nPredRAz
204 eqeq2 ⊢x=X→f⁡suc⁡suc⁡n=x↔f⁡suc⁡suc⁡n=X
205 204 anbi2d ⊢x=X→f⁡∅=y∧f⁡suc⁡suc⁡n=x↔f⁡∅=y∧f⁡suc⁡suc⁡n=X
206 205 3anbi2d ⊢x=X→fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a
207 206 exbidv ⊢x=X→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a
208 eqeq2 ⊢x=X→g⁡suc⁡n=x↔g⁡suc⁡n=X
209 208 anbi2d ⊢x=X→g⁡∅=z∧g⁡suc⁡n=x↔g⁡∅=z∧g⁡suc⁡n=X
210 209 3anbi2d ⊢x=X→gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c
211 210 exbidv ⊢x=X→∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c
212 211 anbi1d ⊢x=X→∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz↔∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
213 212 exbidv ⊢x=X→∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
214 207 213 bibi12d ⊢x=X→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz↔∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
215 214 imbi2d ⊢x=X→n∈ω→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz↔n∈ω→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
216 fvex ⊢f⁡suc⁡b∈V
217 eqid ⊢b∈suc⁡suc⁡n⟼f⁡suc⁡b=b∈suc⁡suc⁡n⟼f⁡suc⁡b
218 216 217 fnmpti ⊢b∈suc⁡suc⁡n⟼f⁡suc⁡bFnsuc⁡suc⁡n
219 218 a1i ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→b∈suc⁡suc⁡n⟼f⁡suc⁡bFnsuc⁡suc⁡n
220 peano2 ⊢n∈ω→suc⁡n∈ω
221 220 adantr ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→suc⁡n∈ω
222 nnord ⊢suc⁡n∈ω→Ord⁡suc⁡n
223 221 222 syl ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→Ord⁡suc⁡n
224 0elsuc ⊢Ord⁡suc⁡n→∅∈suc⁡suc⁡n
225 223 224 syl ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→∅∈suc⁡suc⁡n
226 suceq ⊢b=∅→suc⁡b=suc⁡∅
227 226 fveq2d ⊢b=∅→f⁡suc⁡b=f⁡suc⁡∅
228 fvex ⊢f⁡suc⁡∅∈V
229 227 217 228 fvmpt ⊢∅∈suc⁡suc⁡n→b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡∅=f⁡suc⁡∅
230 225 229 syl ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡∅=f⁡suc⁡∅
231 vex ⊢n∈V
232 231 sucex ⊢suc⁡n∈V
233 232 sucid ⊢suc⁡n∈suc⁡suc⁡n
234 suceq ⊢b=suc⁡n→suc⁡b=suc⁡suc⁡n
235 234 fveq2d ⊢b=suc⁡n→f⁡suc⁡b=f⁡suc⁡suc⁡n
236 fvex ⊢f⁡suc⁡suc⁡n∈V
237 235 217 236 fvmpt ⊢suc⁡n∈suc⁡suc⁡n→b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡n=f⁡suc⁡suc⁡n
238 233 237 mp1i ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡n=f⁡suc⁡suc⁡n
239 simpr2r ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→f⁡suc⁡suc⁡n=x
240 238 239 eqtrd ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡n=x
241 fveq2 ⊢a=suc⁡c→f⁡a=f⁡suc⁡c
242 suceq ⊢a=suc⁡c→suc⁡a=suc⁡suc⁡c
243 242 fveq2d ⊢a=suc⁡c→f⁡suc⁡a=f⁡suc⁡suc⁡c
244 241 243 breq12d ⊢a=suc⁡c→f⁡aR↾Af⁡suc⁡a↔f⁡suc⁡cR↾Af⁡suc⁡suc⁡c
245 simplr3 ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a∧c∈suc⁡n→∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a
246 ordsucelsuc ⊢Ord⁡suc⁡n→c∈suc⁡n↔suc⁡c∈suc⁡suc⁡n
247 223 246 syl ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→c∈suc⁡n↔suc⁡c∈suc⁡suc⁡n
248 247 biimpa ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a∧c∈suc⁡n→suc⁡c∈suc⁡suc⁡n
249 244 245 248 rspcdva ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a∧c∈suc⁡n→f⁡suc⁡cR↾Af⁡suc⁡suc⁡c
250 elelsuc ⊢c∈suc⁡n→c∈suc⁡suc⁡n
251 suceq ⊢b=c→suc⁡b=suc⁡c
252 251 fveq2d ⊢b=c→f⁡suc⁡b=f⁡suc⁡c
253 fvex ⊢f⁡suc⁡c∈V
254 252 217 253 fvmpt ⊢c∈suc⁡suc⁡n→b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡c=f⁡suc⁡c
255 250 254 syl ⊢c∈suc⁡n→b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡c=f⁡suc⁡c
256 255 adantl ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a∧c∈suc⁡n→b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡c=f⁡suc⁡c
257 suceq ⊢b=suc⁡c→suc⁡b=suc⁡suc⁡c
258 257 fveq2d ⊢b=suc⁡c→f⁡suc⁡b=f⁡suc⁡suc⁡c
259 fvex ⊢f⁡suc⁡suc⁡c∈V
260 258 217 259 fvmpt ⊢suc⁡c∈suc⁡suc⁡n→b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡c=f⁡suc⁡suc⁡c
261 248 260 syl ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a∧c∈suc⁡n→b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡c=f⁡suc⁡suc⁡c
262 249 256 261 3brtr4d ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a∧c∈suc⁡n→b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡cR↾Ab∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡c
263 262 ralrimiva ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→∀c∈suc⁡nb∈suc⁡suc⁡n⟼f⁡suc⁡b⁡cR↾Ab∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡c
264 232 sucex ⊢suc⁡suc⁡n∈V
265 264 mptex ⊢b∈suc⁡suc⁡n⟼f⁡suc⁡b∈V
266 fneq1 ⊢g=b∈suc⁡suc⁡n⟼f⁡suc⁡b→gFnsuc⁡suc⁡n↔b∈suc⁡suc⁡n⟼f⁡suc⁡bFnsuc⁡suc⁡n
267 fveq1 ⊢g=b∈suc⁡suc⁡n⟼f⁡suc⁡b→g⁡∅=b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡∅
268 267 eqeq1d ⊢g=b∈suc⁡suc⁡n⟼f⁡suc⁡b→g⁡∅=f⁡suc⁡∅↔b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡∅=f⁡suc⁡∅
269 fveq1 ⊢g=b∈suc⁡suc⁡n⟼f⁡suc⁡b→g⁡suc⁡n=b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡n
270 269 eqeq1d ⊢g=b∈suc⁡suc⁡n⟼f⁡suc⁡b→g⁡suc⁡n=x↔b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡n=x
271 268 270 anbi12d ⊢g=b∈suc⁡suc⁡n⟼f⁡suc⁡b→g⁡∅=f⁡suc⁡∅∧g⁡suc⁡n=x↔b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡∅=f⁡suc⁡∅∧b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡n=x
272 fveq1 ⊢g=b∈suc⁡suc⁡n⟼f⁡suc⁡b→g⁡c=b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡c
273 fveq1 ⊢g=b∈suc⁡suc⁡n⟼f⁡suc⁡b→g⁡suc⁡c=b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡c
274 272 273 breq12d ⊢g=b∈suc⁡suc⁡n⟼f⁡suc⁡b→g⁡cR↾Ag⁡suc⁡c↔b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡cR↾Ab∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡c
275 274 ralbidv ⊢g=b∈suc⁡suc⁡n⟼f⁡suc⁡b→∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔∀c∈suc⁡nb∈suc⁡suc⁡n⟼f⁡suc⁡b⁡cR↾Ab∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡c
276 266 271 275 3anbi123d ⊢g=b∈suc⁡suc⁡n⟼f⁡suc⁡b→gFnsuc⁡suc⁡n∧g⁡∅=f⁡suc⁡∅∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔b∈suc⁡suc⁡n⟼f⁡suc⁡bFnsuc⁡suc⁡n∧b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡∅=f⁡suc⁡∅∧b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡n=x∧∀c∈suc⁡nb∈suc⁡suc⁡n⟼f⁡suc⁡b⁡cR↾Ab∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡c
277 265 276 spcev ⊢b∈suc⁡suc⁡n⟼f⁡suc⁡bFnsuc⁡suc⁡n∧b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡∅=f⁡suc⁡∅∧b∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡n=x∧∀c∈suc⁡nb∈suc⁡suc⁡n⟼f⁡suc⁡b⁡cR↾Ab∈suc⁡suc⁡n⟼f⁡suc⁡b⁡suc⁡c→∃ggFnsuc⁡suc⁡n∧g⁡∅=f⁡suc⁡∅∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c
278 219 230 240 263 277 syl121anc ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→∃ggFnsuc⁡suc⁡n∧g⁡∅=f⁡suc⁡∅∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c
279 simpr2l ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→f⁡∅=y
280 15 fveq2d ⊢a=∅→f⁡suc⁡a=f⁡suc⁡∅
281 14 280 breq12d ⊢a=∅→f⁡aR↾Af⁡suc⁡a↔f⁡∅R↾Af⁡suc⁡∅
282 simpr3 ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a
283 281 282 225 rspcdva ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→f⁡∅R↾Af⁡suc⁡∅
284 279 283 eqbrtrrd ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→yR↾Af⁡suc⁡∅
285 eqeq2 ⊢z=f⁡suc⁡∅→g⁡∅=z↔g⁡∅=f⁡suc⁡∅
286 285 anbi1d ⊢z=f⁡suc⁡∅→g⁡∅=z∧g⁡suc⁡n=x↔g⁡∅=f⁡suc⁡∅∧g⁡suc⁡n=x
287 286 3anbi2d ⊢z=f⁡suc⁡∅→gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔gFnsuc⁡suc⁡n∧g⁡∅=f⁡suc⁡∅∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c
288 287 exbidv ⊢z=f⁡suc⁡∅→∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔∃ggFnsuc⁡suc⁡n∧g⁡∅=f⁡suc⁡∅∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c
289 breq2 ⊢z=f⁡suc⁡∅→yR↾Az↔yR↾Af⁡suc⁡∅
290 288 289 anbi12d ⊢z=f⁡suc⁡∅→∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az↔∃ggFnsuc⁡suc⁡n∧g⁡∅=f⁡suc⁡∅∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Af⁡suc⁡∅
291 228 290 spcev ⊢∃ggFnsuc⁡suc⁡n∧g⁡∅=f⁡suc⁡∅∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Af⁡suc⁡∅→∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az
292 278 284 291 syl2anc ⊢n∈ω∧fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az
293 292 ex ⊢n∈ω→fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az
294 293 exlimdv ⊢n∈ω→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a→∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az
295 fvex ⊢g⁡⋃b∈V
296 101 295 ifex ⊢ifb=∅yg⁡⋃b∈V
297 eqid ⊢b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b
298 296 297 fnmpti ⊢b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃bFnsuc⁡suc⁡suc⁡n
299 298 a1i ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃bFnsuc⁡suc⁡suc⁡n
300 peano2 ⊢suc⁡n∈ω→suc⁡suc⁡n∈ω
301 220 300 syl ⊢n∈ω→suc⁡suc⁡n∈ω
302 301 3ad2ant1 ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→suc⁡suc⁡n∈ω
303 nnord ⊢suc⁡suc⁡n∈ω→Ord⁡suc⁡suc⁡n
304 302 303 syl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→Ord⁡suc⁡suc⁡n
305 0elsuc ⊢Ord⁡suc⁡suc⁡n→∅∈suc⁡suc⁡suc⁡n
306 304 305 syl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→∅∈suc⁡suc⁡suc⁡n
307 iftrue ⊢b=∅→ifb=∅yg⁡⋃b=y
308 307 297 101 fvmpt ⊢∅∈suc⁡suc⁡suc⁡n→b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡∅=y
309 306 308 syl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡∅=y
310 264 sucid ⊢suc⁡suc⁡n∈suc⁡suc⁡suc⁡n
311 eqeq1 ⊢b=suc⁡suc⁡n→b=∅↔suc⁡suc⁡n=∅
312 unieq ⊢b=suc⁡suc⁡n→⋃b=⋃suc⁡suc⁡n
313 312 fveq2d ⊢b=suc⁡suc⁡n→g⁡⋃b=g⁡⋃suc⁡suc⁡n
314 311 313 ifbieq2d ⊢b=suc⁡suc⁡n→ifb=∅yg⁡⋃b=ifsuc⁡suc⁡n=∅yg⁡⋃suc⁡suc⁡n
315 nsuceq0 ⊢suc⁡suc⁡n≠∅
316 315 neii ⊢¬suc⁡suc⁡n=∅
317 316 iffalsei ⊢ifsuc⁡suc⁡n=∅yg⁡⋃suc⁡suc⁡n=g⁡⋃suc⁡suc⁡n
318 314 317 eqtrdi ⊢b=suc⁡suc⁡n→ifb=∅yg⁡⋃b=g⁡⋃suc⁡suc⁡n
319 fvex ⊢g⁡⋃suc⁡suc⁡n∈V
320 318 297 319 fvmpt ⊢suc⁡suc⁡n∈suc⁡suc⁡suc⁡n→b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡suc⁡n=g⁡⋃suc⁡suc⁡n
321 310 320 mp1i ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡suc⁡n=g⁡⋃suc⁡suc⁡n
322 220 3ad2ant1 ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→suc⁡n∈ω
323 322 222 syl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→Ord⁡suc⁡n
324 ordunisuc ⊢Ord⁡suc⁡n→⋃suc⁡suc⁡n=suc⁡n
325 323 324 syl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→⋃suc⁡suc⁡n=suc⁡n
326 325 fveq2d ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→g⁡⋃suc⁡suc⁡n=g⁡suc⁡n
327 simp22r ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→g⁡suc⁡n=x
328 321 326 327 3eqtrd ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡suc⁡n=x
329 simpl3 ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a=∅→yR↾Az
330 iftrue ⊢a=∅→ifa=∅yg⁡⋃a=y
331 330 adantl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a=∅→ifa=∅yg⁡⋃a=y
332 fveq2 ⊢a=∅→g⁡a=g⁡∅
333 simp22l ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→g⁡∅=z
334 332 333 sylan9eqr ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a=∅→g⁡a=z
335 329 331 334 3brtr4d ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a=∅→ifa=∅yg⁡⋃aR↾Ag⁡a
336 335 ex ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→a=∅→ifa=∅yg⁡⋃aR↾Ag⁡a
337 336 adantr ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→a=∅→ifa=∅yg⁡⋃aR↾Ag⁡a
338 ordsucelsuc ⊢Ord⁡suc⁡n→b∈suc⁡n↔suc⁡b∈suc⁡suc⁡n
339 323 338 syl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→b∈suc⁡n↔suc⁡b∈suc⁡suc⁡n
340 elnn ⊢b∈suc⁡n∧suc⁡n∈ω→b∈ω
341 322 340 sylan2 ⊢b∈suc⁡n∧n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→b∈ω
342 341 ancoms ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧b∈suc⁡n→b∈ω
343 nnord ⊢b∈ω→Ord⁡b
344 342 343 syl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧b∈suc⁡n→Ord⁡b
345 ordunisuc ⊢Ord⁡b→⋃suc⁡b=b
346 344 345 syl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧b∈suc⁡n→⋃suc⁡b=b
347 346 fveq2d ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧b∈suc⁡n→g⁡⋃suc⁡b=g⁡b
348 simp23 ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c
349 fveq2 ⊢c=b→g⁡c=g⁡b
350 suceq ⊢c=b→suc⁡c=suc⁡b
351 350 fveq2d ⊢c=b→g⁡suc⁡c=g⁡suc⁡b
352 349 351 breq12d ⊢c=b→g⁡cR↾Ag⁡suc⁡c↔g⁡bR↾Ag⁡suc⁡b
353 352 rspcv ⊢b∈suc⁡n→∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c→g⁡bR↾Ag⁡suc⁡b
354 348 353 mpan9 ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧b∈suc⁡n→g⁡bR↾Ag⁡suc⁡b
355 347 354 eqbrtrd ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧b∈suc⁡n→g⁡⋃suc⁡bR↾Ag⁡suc⁡b
356 355 ex ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→b∈suc⁡n→g⁡⋃suc⁡bR↾Ag⁡suc⁡b
357 339 356 sylbird ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→suc⁡b∈suc⁡suc⁡n→g⁡⋃suc⁡bR↾Ag⁡suc⁡b
358 357 imp ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧suc⁡b∈suc⁡suc⁡n→g⁡⋃suc⁡bR↾Ag⁡suc⁡b
359 eleq1 ⊢a=suc⁡b→a∈suc⁡suc⁡n↔suc⁡b∈suc⁡suc⁡n
360 359 anbi2d ⊢a=suc⁡b→n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n↔n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧suc⁡b∈suc⁡suc⁡n
361 eqeq1 ⊢a=suc⁡b→a=∅↔suc⁡b=∅
362 unieq ⊢a=suc⁡b→⋃a=⋃suc⁡b
363 362 fveq2d ⊢a=suc⁡b→g⁡⋃a=g⁡⋃suc⁡b
364 361 363 ifbieq2d ⊢a=suc⁡b→ifa=∅yg⁡⋃a=ifsuc⁡b=∅yg⁡⋃suc⁡b
365 nsuceq0 ⊢suc⁡b≠∅
366 365 neii ⊢¬suc⁡b=∅
367 366 iffalsei ⊢ifsuc⁡b=∅yg⁡⋃suc⁡b=g⁡⋃suc⁡b
368 364 367 eqtrdi ⊢a=suc⁡b→ifa=∅yg⁡⋃a=g⁡⋃suc⁡b
369 fveq2 ⊢a=suc⁡b→g⁡a=g⁡suc⁡b
370 368 369 breq12d ⊢a=suc⁡b→ifa=∅yg⁡⋃aR↾Ag⁡a↔g⁡⋃suc⁡bR↾Ag⁡suc⁡b
371 360 370 imbi12d ⊢a=suc⁡b→n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→ifa=∅yg⁡⋃aR↾Ag⁡a↔n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧suc⁡b∈suc⁡suc⁡n→g⁡⋃suc⁡bR↾Ag⁡suc⁡b
372 358 371 mpbiri ⊢a=suc⁡b→n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→ifa=∅yg⁡⋃aR↾Ag⁡a
373 372 com12 ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→a=suc⁡b→ifa=∅yg⁡⋃aR↾Ag⁡a
374 373 rexlimdvw ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→∃b∈ωa=suc⁡b→ifa=∅yg⁡⋃aR↾Ag⁡a
375 elnn ⊢a∈suc⁡suc⁡n∧suc⁡suc⁡n∈ω→a∈ω
376 375 ancoms ⊢suc⁡suc⁡n∈ω∧a∈suc⁡suc⁡n→a∈ω
377 302 376 sylan ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→a∈ω
378 nn0suc ⊢a∈ω→a=∅∨∃b∈ωa=suc⁡b
379 377 378 syl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→a=∅∨∃b∈ωa=suc⁡b
380 337 374 379 mpjaod ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→ifa=∅yg⁡⋃aR↾Ag⁡a
381 elelsuc ⊢a∈suc⁡suc⁡n→a∈suc⁡suc⁡suc⁡n
382 eqeq1 ⊢b=a→b=∅↔a=∅
383 unieq ⊢b=a→⋃b=⋃a
384 383 fveq2d ⊢b=a→g⁡⋃b=g⁡⋃a
385 382 384 ifbieq2d ⊢b=a→ifb=∅yg⁡⋃b=ifa=∅yg⁡⋃a
386 fvex ⊢g⁡⋃a∈V
387 101 386 ifex ⊢ifa=∅yg⁡⋃a∈V
388 385 297 387 fvmpt ⊢a∈suc⁡suc⁡suc⁡n→b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡a=ifa=∅yg⁡⋃a
389 381 388 syl ⊢a∈suc⁡suc⁡n→b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡a=ifa=∅yg⁡⋃a
390 389 adantl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡a=ifa=∅yg⁡⋃a
391 ordsucelsuc ⊢Ord⁡suc⁡suc⁡n→a∈suc⁡suc⁡n↔suc⁡a∈suc⁡suc⁡suc⁡n
392 304 391 syl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→a∈suc⁡suc⁡n↔suc⁡a∈suc⁡suc⁡suc⁡n
393 392 biimpa ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→suc⁡a∈suc⁡suc⁡suc⁡n
394 eqeq1 ⊢b=suc⁡a→b=∅↔suc⁡a=∅
395 unieq ⊢b=suc⁡a→⋃b=⋃suc⁡a
396 395 fveq2d ⊢b=suc⁡a→g⁡⋃b=g⁡⋃suc⁡a
397 394 396 ifbieq2d ⊢b=suc⁡a→ifb=∅yg⁡⋃b=ifsuc⁡a=∅yg⁡⋃suc⁡a
398 nsuceq0 ⊢suc⁡a≠∅
399 398 neii ⊢¬suc⁡a=∅
400 399 iffalsei ⊢ifsuc⁡a=∅yg⁡⋃suc⁡a=g⁡⋃suc⁡a
401 397 400 eqtrdi ⊢b=suc⁡a→ifb=∅yg⁡⋃b=g⁡⋃suc⁡a
402 fvex ⊢g⁡⋃suc⁡a∈V
403 401 297 402 fvmpt ⊢suc⁡a∈suc⁡suc⁡suc⁡n→b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡a=g⁡⋃suc⁡a
404 393 403 syl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡a=g⁡⋃suc⁡a
405 nnord ⊢a∈ω→Ord⁡a
406 377 405 syl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→Ord⁡a
407 ordunisuc ⊢Ord⁡a→⋃suc⁡a=a
408 406 407 syl ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→⋃suc⁡a=a
409 408 fveq2d ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→g⁡⋃suc⁡a=g⁡a
410 404 409 eqtrd ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡a=g⁡a
411 380 390 410 3brtr4d ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az∧a∈suc⁡suc⁡n→b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡aR↾Ab∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡a
412 411 ralrimiva ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→∀a∈suc⁡suc⁡nb∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡aR↾Ab∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡a
413 264 sucex ⊢suc⁡suc⁡suc⁡n∈V
414 413 mptex ⊢b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b∈V
415 fneq1 ⊢f=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b→fFnsuc⁡suc⁡suc⁡n↔b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃bFnsuc⁡suc⁡suc⁡n
416 fveq1 ⊢f=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b→f⁡∅=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡∅
417 416 eqeq1d ⊢f=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b→f⁡∅=y↔b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡∅=y
418 fveq1 ⊢f=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b→f⁡suc⁡suc⁡n=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡suc⁡n
419 418 eqeq1d ⊢f=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b→f⁡suc⁡suc⁡n=x↔b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡suc⁡n=x
420 417 419 anbi12d ⊢f=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b→f⁡∅=y∧f⁡suc⁡suc⁡n=x↔b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡∅=y∧b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡suc⁡n=x
421 fveq1 ⊢f=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b→f⁡a=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡a
422 fveq1 ⊢f=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b→f⁡suc⁡a=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡a
423 421 422 breq12d ⊢f=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b→f⁡aR↾Af⁡suc⁡a↔b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡aR↾Ab∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡a
424 423 ralbidv ⊢f=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b→∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔∀a∈suc⁡suc⁡nb∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡aR↾Ab∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡a
425 415 420 424 3anbi123d ⊢f=b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b→fFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃bFnsuc⁡suc⁡suc⁡n∧b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡∅=y∧b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nb∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡aR↾Ab∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡a
426 414 425 spcev ⊢b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃bFnsuc⁡suc⁡suc⁡n∧b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡∅=y∧b∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nb∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡aR↾Ab∈suc⁡suc⁡suc⁡n⟼ifb=∅yg⁡⋃b⁡suc⁡a→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a
427 299 309 328 412 426 syl121anc ⊢n∈ω∧gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a
428 427 3exp ⊢n∈ω→gFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c→yR↾Az→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a
429 428 exlimdv ⊢n∈ω→∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c→yR↾Az→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a
430 429 impd ⊢n∈ω→∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a
431 430 exlimdv ⊢n∈ω→∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a
432 294 431 impbid ⊢n∈ω→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az
433 vex ⊢z∈V
434 433 brresi ⊢yR↾Az↔y∈A∧yRz
435 434 anbi2i ⊢∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az↔∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
436 435 exbii ⊢∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧yR↾Az↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
437 432 436 bitrdi ⊢n∈ω→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=x∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=x∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
438 215 437 vtoclg ⊢X∈A→n∈ω→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
439 438 impcom ⊢n∈ω∧X∈A→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
440 439 adantrl ⊢n∈ω∧RSeA∧X∈A→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
441 440 3adant3 ⊢n∈ω∧RSeA∧X∈A∧∀z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔∃z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c∧y∈A∧yRz
442 175 203 441 3bitr4rd ⊢n∈ω∧RSeA∧X∈A∧∀z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n→∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔y∈F⁡suc⁡n
443 442 alrimiv ⊢n∈ω∧RSeA∧X∈A∧∀z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n→∀y∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔y∈F⁡suc⁡n
444 443 3exp ⊢n∈ω→RSeA∧X∈A→∀z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n→∀y∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔y∈F⁡suc⁡n
445 444 a2d ⊢n∈ω→RSeA∧X∈A→∀z∃ggFnsuc⁡suc⁡n∧g⁡∅=z∧g⁡suc⁡n=X∧∀c∈suc⁡ng⁡cR↾Ag⁡suc⁡c↔z∈F⁡n→RSeA∧X∈A→∀y∃ffFnsuc⁡suc⁡suc⁡n∧f⁡∅=y∧f⁡suc⁡suc⁡n=X∧∀a∈suc⁡suc⁡nf⁡aR↾Af⁡suc⁡a↔y∈F⁡suc⁡n
446 27 68 82 96 164 445 finds ⊢N∈ω→RSeA∧X∈A→∀y∃ffFnsuc⁡suc⁡N∧f⁡∅=y∧f⁡suc⁡N=X∧∀a∈suc⁡Nf⁡aR↾Af⁡suc⁡a↔y∈F⁡N
447 446 3impib ⊢N∈ω∧RSeA∧X∈A→∀y∃ffFnsuc⁡suc⁡N∧f⁡∅=y∧f⁡suc⁡N=X∧∀a∈suc⁡Nf⁡aR↾Af⁡suc⁡a↔y∈F⁡N
448 447 19.21bi ⊢N∈ω∧RSeA∧X∈A→∃ffFnsuc⁡suc⁡N∧f⁡∅=y∧f⁡suc⁡N=X∧∀a∈suc⁡Nf⁡aR↾Af⁡suc⁡a↔y∈F⁡N