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 ⊢ 𝐹 = rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) )
Assertion ttrclselem2 ( ( 𝑁 ∈ ω ∧ 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑁 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc 𝑁 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc 𝑁 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ 𝑦 ∈ ( 𝐹 ‘ 𝑁 ) ) )

Proof

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