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 biimpi ⊢ ( 𝑅 Se 𝐴 → ∀ 𝑧 ∈ 𝐴 Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
182 181 adantl ⊢ ( ( 𝑛 ∈ ω ∧ 𝑅 Se 𝐴 ) → ∀ 𝑧 ∈ 𝐴 Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
183 ssralv ⊢ ( ( 𝐹 ‘ 𝑛 ) ⊆ 𝐴 → ( ∀ 𝑧 ∈ 𝐴 Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V → ∀ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) )
184 179 182 183 sylc ⊢ ( ( 𝑛 ∈ ω ∧ 𝑅 Se 𝐴 ) → ∀ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
185 184 adantrr ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ∀ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
186 iunexg ⊢ ( ( ( 𝐹 ‘ 𝑛 ) ∈ V ∧ ∀ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) → ∪ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
187 177 185 186 sylancr ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ∪ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
188 nfcv ⊢ Ⅎ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑋 )
189 nfcv ⊢ Ⅎ 𝑏 𝑛
190 nfmpt1 ⊢ Ⅎ 𝑏 ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) )
191 190 188 nfrdg ⊢ Ⅎ 𝑏 rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) )
192 1 191 nfcxfr ⊢ Ⅎ 𝑏 𝐹
193 192 189 nffv ⊢ Ⅎ 𝑏 ( 𝐹 ‘ 𝑛 )
194 nfcv ⊢ Ⅎ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑧 )
195 193 194 nfiun ⊢ Ⅎ 𝑏 ∪ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 )
196 predeq3 ⊢ ( 𝑤 = 𝑧 → Pred ( 𝑅 , 𝐴 , 𝑤 ) = Pred ( 𝑅 , 𝐴 , 𝑧 ) )
197 196 cbviunv ⊢ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) = ∪ 𝑧 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑧 )
198 iuneq1 ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑛 ) → ∪ 𝑧 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑧 ) = ∪ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) )
199 197 198 eqtrid ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑛 ) → ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) = ∪ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) )
200 188 189 195 1 199 rdgsucmptf ⊢ ( ( 𝑛 ∈ On ∧ ∪ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) → ( 𝐹 ‘ suc 𝑛 ) = ∪ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) )
201 176 187 200 syl2an2r ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝐹 ‘ suc 𝑛 ) = ∪ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) )
202 201 3adant3 ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝐹 ‘ suc 𝑛 ) = ∪ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) )
203 202 eleq2d ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝑦 ∈ ( 𝐹 ‘ suc 𝑛 ) ↔ 𝑦 ∈ ∪ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
204 eqeq2 ⊢ ( 𝑥 = 𝑋 → ( ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ↔ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑋 ) )
205 204 anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ↔ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑋 ) ) )
206 205 3anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) )
207 206 exbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) )
208 eqeq2 ⊢ ( 𝑥 = 𝑋 → ( ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ↔ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) )
209 208 anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ↔ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ) )
210 209 3anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ↔ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ) )
211 210 exbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ↔ ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ) )
212 211 anbi1d ⊢ ( 𝑥 = 𝑋 → ( ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) ↔ ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) ) )
213 212 exbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) ↔ ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) ) )
214 207 213 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 𝑐 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) ) ) )
215 214 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 𝑐 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) ) ) ) )
216 fvex ⊢ ( 𝑓 ‘ suc 𝑏 ) ∈ V
217 eqid ⊢ ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) = ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) )
218 216 217 fnmpti ⊢ ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) Fn suc suc 𝑛
219 218 a1i ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) Fn suc suc 𝑛 )
220 peano2 ⊢ ( 𝑛 ∈ ω → suc 𝑛 ∈ ω )
221 220 adantr ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → suc 𝑛 ∈ ω )
222 nnord ⊢ ( suc 𝑛 ∈ ω → Ord suc 𝑛 )
223 221 222 syl ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → Ord suc 𝑛 )
224 0elsuc ⊢ ( Ord suc 𝑛 → ∅ ∈ suc suc 𝑛 )
225 223 224 syl ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → ∅ ∈ suc suc 𝑛 )
226 suceq ⊢ ( 𝑏 = ∅ → suc 𝑏 = suc ∅ )
227 226 fveq2d ⊢ ( 𝑏 = ∅ → ( 𝑓 ‘ suc 𝑏 ) = ( 𝑓 ‘ suc ∅ ) )
228 fvex ⊢ ( 𝑓 ‘ suc ∅ ) ∈ V
229 227 217 228 fvmpt ⊢ ( ∅ ∈ suc suc 𝑛 → ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ ∅ ) = ( 𝑓 ‘ suc ∅ ) )
230 225 229 syl ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ ∅ ) = ( 𝑓 ‘ suc ∅ ) )
231 vex ⊢ 𝑛 ∈ V
232 231 sucex ⊢ suc 𝑛 ∈ V
233 232 sucid ⊢ suc 𝑛 ∈ suc suc 𝑛
234 suceq ⊢ ( 𝑏 = suc 𝑛 → suc 𝑏 = suc suc 𝑛 )
235 234 fveq2d ⊢ ( 𝑏 = suc 𝑛 → ( 𝑓 ‘ suc 𝑏 ) = ( 𝑓 ‘ suc suc 𝑛 ) )
236 fvex ⊢ ( 𝑓 ‘ suc suc 𝑛 ) ∈ V
237 235 217 236 fvmpt ⊢ ( suc 𝑛 ∈ suc suc 𝑛 → ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ suc 𝑛 ) = ( 𝑓 ‘ suc suc 𝑛 ) )
238 233 237 mp1i ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ suc 𝑛 ) = ( 𝑓 ‘ suc suc 𝑛 ) )
239 simpr2r ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 )
240 238 239 eqtrd ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ suc 𝑛 ) = 𝑥 )
241 fveq2 ⊢ ( 𝑎 = suc 𝑐 → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ suc 𝑐 ) )
242 suceq ⊢ ( 𝑎 = suc 𝑐 → suc 𝑎 = suc suc 𝑐 )
243 242 fveq2d ⊢ ( 𝑎 = suc 𝑐 → ( 𝑓 ‘ suc 𝑎 ) = ( 𝑓 ‘ suc suc 𝑐 ) )
244 241 243 breq12d ⊢ ( 𝑎 = suc 𝑐 → ( ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ↔ ( 𝑓 ‘ suc 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc suc 𝑐 ) ) )
245 simplr3 ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) ∧ 𝑐 ∈ suc 𝑛 ) → ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) )
246 ordsucelsuc ⊢ ( Ord suc 𝑛 → ( 𝑐 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc suc 𝑛 ) )
247 223 246 syl ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑐 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc suc 𝑛 ) )
248 247 biimpa ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) ∧ 𝑐 ∈ suc 𝑛 ) → suc 𝑐 ∈ suc suc 𝑛 )
249 244 245 248 rspcdva ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) ∧ 𝑐 ∈ suc 𝑛 ) → ( 𝑓 ‘ suc 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc suc 𝑐 ) )
250 elelsuc ⊢ ( 𝑐 ∈ suc 𝑛 → 𝑐 ∈ suc suc 𝑛 )
251 suceq ⊢ ( 𝑏 = 𝑐 → suc 𝑏 = suc 𝑐 )
252 251 fveq2d ⊢ ( 𝑏 = 𝑐 → ( 𝑓 ‘ suc 𝑏 ) = ( 𝑓 ‘ suc 𝑐 ) )
253 fvex ⊢ ( 𝑓 ‘ suc 𝑐 ) ∈ V
254 252 217 253 fvmpt ⊢ ( 𝑐 ∈ suc suc 𝑛 → ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( 𝑓 ‘ suc 𝑐 ) )
255 250 254 syl ⊢ ( 𝑐 ∈ suc 𝑛 → ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( 𝑓 ‘ suc 𝑐 ) )
256 255 adantl ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) ∧ 𝑐 ∈ suc 𝑛 ) → ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( 𝑓 ‘ suc 𝑐 ) )
257 suceq ⊢ ( 𝑏 = suc 𝑐 → suc 𝑏 = suc suc 𝑐 )
258 257 fveq2d ⊢ ( 𝑏 = suc 𝑐 → ( 𝑓 ‘ suc 𝑏 ) = ( 𝑓 ‘ suc suc 𝑐 ) )
259 fvex ⊢ ( 𝑓 ‘ suc suc 𝑐 ) ∈ V
260 258 217 259 fvmpt ⊢ ( suc 𝑐 ∈ suc suc 𝑛 → ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ suc 𝑐 ) = ( 𝑓 ‘ suc suc 𝑐 ) )
261 248 260 syl ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) ∧ 𝑐 ∈ suc 𝑛 ) → ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ suc 𝑐 ) = ( 𝑓 ‘ suc suc 𝑐 ) )
262 249 256 261 3brtr4d ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) ∧ 𝑐 ∈ suc 𝑛 ) → ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ suc 𝑐 ) )
263 262 ralrimiva ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → ∀ 𝑐 ∈ suc 𝑛 ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ suc 𝑐 ) )
264 232 sucex ⊢ suc suc 𝑛 ∈ V
265 264 mptex ⊢ ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ∈ V
266 fneq1 ⊢ ( 𝑔 = ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) → ( 𝑔 Fn suc suc 𝑛 ↔ ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) Fn suc suc 𝑛 ) )
267 fveq1 ⊢ ( 𝑔 = ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) → ( 𝑔 ‘ ∅ ) = ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ ∅ ) )
268 267 eqeq1d ⊢ ( 𝑔 = ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) → ( ( 𝑔 ‘ ∅ ) = ( 𝑓 ‘ suc ∅ ) ↔ ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ ∅ ) = ( 𝑓 ‘ suc ∅ ) ) )
269 fveq1 ⊢ ( 𝑔 = ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) → ( 𝑔 ‘ suc 𝑛 ) = ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ suc 𝑛 ) )
270 269 eqeq1d ⊢ ( 𝑔 = ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) → ( ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ↔ ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ suc 𝑛 ) = 𝑥 ) )
271 268 270 anbi12d ⊢ ( 𝑔 = ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) → ( ( ( 𝑔 ‘ ∅ ) = ( 𝑓 ‘ suc ∅ ) ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ↔ ( ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ ∅ ) = ( 𝑓 ‘ suc ∅ ) ∧ ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ suc 𝑛 ) = 𝑥 ) ) )
272 fveq1 ⊢ ( 𝑔 = ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) → ( 𝑔 ‘ 𝑐 ) = ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ 𝑐 ) )
273 fveq1 ⊢ ( 𝑔 = ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) → ( 𝑔 ‘ suc 𝑐 ) = ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ suc 𝑐 ) )
274 272 273 breq12d ⊢ ( 𝑔 = ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) → ( ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ↔ ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ suc 𝑐 ) ) )
275 274 ralbidv ⊢ ( 𝑔 = ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) → ( ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ↔ ∀ 𝑐 ∈ suc 𝑛 ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( ( 𝑏 ∈ suc suc 𝑛 ↦ ( 𝑓 ‘ suc 𝑏 ) ) ‘ suc 𝑐 ) ) )
276 266 271 275 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 𝑐 ) ) ) )
277 265 276 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 𝑐 ) ) )
278 219 230 240 263 277 syl121anc ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = ( 𝑓 ‘ suc ∅ ) ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) )
279 simpr2l ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ ∅ ) = 𝑦 )
280 15 fveq2d ⊢ ( 𝑎 = ∅ → ( 𝑓 ‘ suc 𝑎 ) = ( 𝑓 ‘ suc ∅ ) )
281 14 280 breq12d ⊢ ( 𝑎 = ∅ → ( ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ↔ ( 𝑓 ‘ ∅ ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc ∅ ) ) )
282 simpr3 ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) )
283 281 282 225 rspcdva ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ ∅ ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc ∅ ) )
284 279 283 eqbrtrrd ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → 𝑦 ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc ∅ ) )
285 eqeq2 ⊢ ( 𝑧 = ( 𝑓 ‘ suc ∅ ) → ( ( 𝑔 ‘ ∅ ) = 𝑧 ↔ ( 𝑔 ‘ ∅ ) = ( 𝑓 ‘ suc ∅ ) ) )
286 285 anbi1d ⊢ ( 𝑧 = ( 𝑓 ‘ suc ∅ ) → ( ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ↔ ( ( 𝑔 ‘ ∅ ) = ( 𝑓 ‘ suc ∅ ) ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ) )
287 286 3anbi2d ⊢ ( 𝑧 = ( 𝑓 ‘ suc ∅ ) → ( ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ↔ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = ( 𝑓 ‘ suc ∅ ) ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ) )
288 287 exbidv ⊢ ( 𝑧 = ( 𝑓 ‘ suc ∅ ) → ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ↔ ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = ( 𝑓 ‘ suc ∅ ) ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ) )
289 breq2 ⊢ ( 𝑧 = ( 𝑓 ‘ suc ∅ ) → ( 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ↔ 𝑦 ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc ∅ ) ) )
290 288 289 anbi12d ⊢ ( 𝑧 = ( 𝑓 ‘ suc ∅ ) → ( ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ↔ ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = ( 𝑓 ‘ suc ∅ ) ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc ∅ ) ) ) )
291 228 290 spcev ⊢ ( ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = ( 𝑓 ‘ suc ∅ ) ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc ∅ ) ) → ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) )
292 278 284 291 syl2anc ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) → ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) )
293 292 ex ⊢ ( 𝑛 ∈ ω → ( ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) → ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ) )
294 293 exlimdv ⊢ ( 𝑛 ∈ ω → ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) → ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ) )
295 fvex ⊢ ( 𝑔 ‘ ∪ 𝑏 ) ∈ V
296 101 295 ifex ⊢ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ∈ V
297 eqid ⊢ ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) = ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) )
298 296 297 fnmpti ⊢ ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) Fn suc suc suc 𝑛
299 298 a1i ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) Fn suc suc suc 𝑛 )
300 peano2 ⊢ ( suc 𝑛 ∈ ω → suc suc 𝑛 ∈ ω )
301 220 300 syl ⊢ ( 𝑛 ∈ ω → suc suc 𝑛 ∈ ω )
302 301 3ad2ant1 ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → suc suc 𝑛 ∈ ω )
303 nnord ⊢ ( suc suc 𝑛 ∈ ω → Ord suc suc 𝑛 )
304 302 303 syl ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → Ord suc suc 𝑛 )
305 0elsuc ⊢ ( Ord suc suc 𝑛 → ∅ ∈ suc suc suc 𝑛 )
306 304 305 syl ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ∅ ∈ suc suc suc 𝑛 )
307 iftrue ⊢ ( 𝑏 = ∅ → if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) = 𝑦 )
308 307 297 101 fvmpt ⊢ ( ∅ ∈ suc suc suc 𝑛 → ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ ∅ ) = 𝑦 )
309 306 308 syl ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ ∅ ) = 𝑦 )
310 264 sucid ⊢ suc suc 𝑛 ∈ suc suc suc 𝑛
311 eqeq1 ⊢ ( 𝑏 = suc suc 𝑛 → ( 𝑏 = ∅ ↔ suc suc 𝑛 = ∅ ) )
312 unieq ⊢ ( 𝑏 = suc suc 𝑛 → ∪ 𝑏 = ∪ suc suc 𝑛 )
313 312 fveq2d ⊢ ( 𝑏 = suc suc 𝑛 → ( 𝑔 ‘ ∪ 𝑏 ) = ( 𝑔 ‘ ∪ suc suc 𝑛 ) )
314 311 313 ifbieq2d ⊢ ( 𝑏 = suc suc 𝑛 → if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) = if ( suc suc 𝑛 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ suc suc 𝑛 ) ) )
315 nsuceq0 ⊢ suc suc 𝑛 ≠ ∅
316 315 neii ⊢ ¬ suc suc 𝑛 = ∅
317 316 iffalsei ⊢ if ( suc suc 𝑛 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ suc suc 𝑛 ) ) = ( 𝑔 ‘ ∪ suc suc 𝑛 )
318 314 317 eqtrdi ⊢ ( 𝑏 = suc suc 𝑛 → if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) = ( 𝑔 ‘ ∪ suc suc 𝑛 ) )
319 fvex ⊢ ( 𝑔 ‘ ∪ suc suc 𝑛 ) ∈ V
320 318 297 319 fvmpt ⊢ ( suc suc 𝑛 ∈ suc suc suc 𝑛 → ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc suc 𝑛 ) = ( 𝑔 ‘ ∪ suc suc 𝑛 ) )
321 310 320 mp1i ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc suc 𝑛 ) = ( 𝑔 ‘ ∪ suc suc 𝑛 ) )
322 220 3ad2ant1 ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → suc 𝑛 ∈ ω )
323 322 222 syl ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → Ord suc 𝑛 )
324 ordunisuc ⊢ ( Ord suc 𝑛 → ∪ suc suc 𝑛 = suc 𝑛 )
325 323 324 syl ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ∪ suc suc 𝑛 = suc 𝑛 )
326 325 fveq2d ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ( 𝑔 ‘ ∪ suc suc 𝑛 ) = ( 𝑔 ‘ suc 𝑛 ) )
327 simp22r ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ( 𝑔 ‘ suc 𝑛 ) = 𝑥 )
328 321 326 327 3eqtrd ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc suc 𝑛 ) = 𝑥 )
329 simpl3 ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 = ∅ ) → 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 )
330 iftrue ⊢ ( 𝑎 = ∅ → if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) = 𝑦 )
331 330 adantl ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 = ∅ ) → if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) = 𝑦 )
332 fveq2 ⊢ ( 𝑎 = ∅ → ( 𝑔 ‘ 𝑎 ) = ( 𝑔 ‘ ∅ ) )
333 simp22l ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ( 𝑔 ‘ ∅ ) = 𝑧 )
334 332 333 sylan9eqr ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 = ∅ ) → ( 𝑔 ‘ 𝑎 ) = 𝑧 )
335 329 331 334 3brtr4d ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 = ∅ ) → if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ 𝑎 ) )
336 335 ex ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ( 𝑎 = ∅ → if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ 𝑎 ) ) )
337 336 adantr ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → ( 𝑎 = ∅ → if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ 𝑎 ) ) )
338 ordsucelsuc ⊢ ( Ord suc 𝑛 → ( 𝑏 ∈ suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛 ) )
339 323 338 syl ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ( 𝑏 ∈ suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛 ) )
340 elnn ⊢ ( ( 𝑏 ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω ) → 𝑏 ∈ ω )
341 322 340 sylan2 ⊢ ( ( 𝑏 ∈ suc 𝑛 ∧ ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ) → 𝑏 ∈ ω )
342 341 ancoms ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑏 ∈ suc 𝑛 ) → 𝑏 ∈ ω )
343 nnord ⊢ ( 𝑏 ∈ ω → Ord 𝑏 )
344 342 343 syl ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑏 ∈ suc 𝑛 ) → Ord 𝑏 )
345 ordunisuc ⊢ ( Ord 𝑏 → ∪ suc 𝑏 = 𝑏 )
346 344 345 syl ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑏 ∈ suc 𝑛 ) → ∪ suc 𝑏 = 𝑏 )
347 346 fveq2d ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑏 ∈ suc 𝑛 ) → ( 𝑔 ‘ ∪ suc 𝑏 ) = ( 𝑔 ‘ 𝑏 ) )
348 simp23 ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) )
349 fveq2 ⊢ ( 𝑐 = 𝑏 → ( 𝑔 ‘ 𝑐 ) = ( 𝑔 ‘ 𝑏 ) )
350 suceq ⊢ ( 𝑐 = 𝑏 → suc 𝑐 = suc 𝑏 )
351 350 fveq2d ⊢ ( 𝑐 = 𝑏 → ( 𝑔 ‘ suc 𝑐 ) = ( 𝑔 ‘ suc 𝑏 ) )
352 349 351 breq12d ⊢ ( 𝑐 = 𝑏 → ( ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ↔ ( 𝑔 ‘ 𝑏 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑏 ) ) )
353 352 rspcv ⊢ ( 𝑏 ∈ suc 𝑛 → ( ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) → ( 𝑔 ‘ 𝑏 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑏 ) ) )
354 348 353 mpan9 ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑏 ∈ suc 𝑛 ) → ( 𝑔 ‘ 𝑏 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑏 ) )
355 347 354 eqbrtrd ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑏 ∈ suc 𝑛 ) → ( 𝑔 ‘ ∪ suc 𝑏 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑏 ) )
356 355 ex ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ( 𝑏 ∈ suc 𝑛 → ( 𝑔 ‘ ∪ suc 𝑏 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑏 ) ) )
357 339 356 sylbird ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ( suc 𝑏 ∈ suc suc 𝑛 → ( 𝑔 ‘ ∪ suc 𝑏 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑏 ) ) )
358 357 imp ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ suc 𝑏 ∈ suc suc 𝑛 ) → ( 𝑔 ‘ ∪ suc 𝑏 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑏 ) )
359 eleq1 ⊢ ( 𝑎 = suc 𝑏 → ( 𝑎 ∈ suc suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛 ) )
360 359 anbi2d ⊢ ( 𝑎 = suc 𝑏 → ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) ↔ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ suc 𝑏 ∈ suc suc 𝑛 ) ) )
361 eqeq1 ⊢ ( 𝑎 = suc 𝑏 → ( 𝑎 = ∅ ↔ suc 𝑏 = ∅ ) )
362 unieq ⊢ ( 𝑎 = suc 𝑏 → ∪ 𝑎 = ∪ suc 𝑏 )
363 362 fveq2d ⊢ ( 𝑎 = suc 𝑏 → ( 𝑔 ‘ ∪ 𝑎 ) = ( 𝑔 ‘ ∪ suc 𝑏 ) )
364 361 363 ifbieq2d ⊢ ( 𝑎 = suc 𝑏 → if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) = if ( suc 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ suc 𝑏 ) ) )
365 nsuceq0 ⊢ suc 𝑏 ≠ ∅
366 365 neii ⊢ ¬ suc 𝑏 = ∅
367 366 iffalsei ⊢ if ( suc 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ suc 𝑏 ) ) = ( 𝑔 ‘ ∪ suc 𝑏 )
368 364 367 eqtrdi ⊢ ( 𝑎 = suc 𝑏 → if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) = ( 𝑔 ‘ ∪ suc 𝑏 ) )
369 fveq2 ⊢ ( 𝑎 = suc 𝑏 → ( 𝑔 ‘ 𝑎 ) = ( 𝑔 ‘ suc 𝑏 ) )
370 368 369 breq12d ⊢ ( 𝑎 = suc 𝑏 → ( if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ 𝑎 ) ↔ ( 𝑔 ‘ ∪ suc 𝑏 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑏 ) ) )
371 360 370 imbi12d ⊢ ( 𝑎 = suc 𝑏 → ( ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ 𝑎 ) ) ↔ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ suc 𝑏 ∈ suc suc 𝑛 ) → ( 𝑔 ‘ ∪ suc 𝑏 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑏 ) ) ) )
372 358 371 mpbiri ⊢ ( 𝑎 = suc 𝑏 → ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ 𝑎 ) ) )
373 372 com12 ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → ( 𝑎 = suc 𝑏 → if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ 𝑎 ) ) )
374 373 rexlimdvw ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → ( ∃ 𝑏 ∈ ω 𝑎 = suc 𝑏 → if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ 𝑎 ) ) )
375 elnn ⊢ ( ( 𝑎 ∈ suc suc 𝑛 ∧ suc suc 𝑛 ∈ ω ) → 𝑎 ∈ ω )
376 375 ancoms ⊢ ( ( suc suc 𝑛 ∈ ω ∧ 𝑎 ∈ suc suc 𝑛 ) → 𝑎 ∈ ω )
377 302 376 sylan ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → 𝑎 ∈ ω )
378 nn0suc ⊢ ( 𝑎 ∈ ω → ( 𝑎 = ∅ ∨ ∃ 𝑏 ∈ ω 𝑎 = suc 𝑏 ) )
379 377 378 syl ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → ( 𝑎 = ∅ ∨ ∃ 𝑏 ∈ ω 𝑎 = suc 𝑏 ) )
380 337 374 379 mpjaod ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ 𝑎 ) )
381 elelsuc ⊢ ( 𝑎 ∈ suc suc 𝑛 → 𝑎 ∈ suc suc suc 𝑛 )
382 eqeq1 ⊢ ( 𝑏 = 𝑎 → ( 𝑏 = ∅ ↔ 𝑎 = ∅ ) )
383 unieq ⊢ ( 𝑏 = 𝑎 → ∪ 𝑏 = ∪ 𝑎 )
384 383 fveq2d ⊢ ( 𝑏 = 𝑎 → ( 𝑔 ‘ ∪ 𝑏 ) = ( 𝑔 ‘ ∪ 𝑎 ) )
385 382 384 ifbieq2d ⊢ ( 𝑏 = 𝑎 → if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) = if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) )
386 fvex ⊢ ( 𝑔 ‘ ∪ 𝑎 ) ∈ V
387 101 386 ifex ⊢ if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) ∈ V
388 385 297 387 fvmpt ⊢ ( 𝑎 ∈ suc suc suc 𝑛 → ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ 𝑎 ) = if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) )
389 381 388 syl ⊢ ( 𝑎 ∈ suc suc 𝑛 → ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ 𝑎 ) = if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) )
390 389 adantl ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ 𝑎 ) = if ( 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑎 ) ) )
391 ordsucelsuc ⊢ ( Ord suc suc 𝑛 → ( 𝑎 ∈ suc suc 𝑛 ↔ suc 𝑎 ∈ suc suc suc 𝑛 ) )
392 304 391 syl ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ( 𝑎 ∈ suc suc 𝑛 ↔ suc 𝑎 ∈ suc suc suc 𝑛 ) )
393 392 biimpa ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → suc 𝑎 ∈ suc suc suc 𝑛 )
394 eqeq1 ⊢ ( 𝑏 = suc 𝑎 → ( 𝑏 = ∅ ↔ suc 𝑎 = ∅ ) )
395 unieq ⊢ ( 𝑏 = suc 𝑎 → ∪ 𝑏 = ∪ suc 𝑎 )
396 395 fveq2d ⊢ ( 𝑏 = suc 𝑎 → ( 𝑔 ‘ ∪ 𝑏 ) = ( 𝑔 ‘ ∪ suc 𝑎 ) )
397 394 396 ifbieq2d ⊢ ( 𝑏 = suc 𝑎 → if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) = if ( suc 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ suc 𝑎 ) ) )
398 nsuceq0 ⊢ suc 𝑎 ≠ ∅
399 398 neii ⊢ ¬ suc 𝑎 = ∅
400 399 iffalsei ⊢ if ( suc 𝑎 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ suc 𝑎 ) ) = ( 𝑔 ‘ ∪ suc 𝑎 )
401 397 400 eqtrdi ⊢ ( 𝑏 = suc 𝑎 → if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) = ( 𝑔 ‘ ∪ suc 𝑎 ) )
402 fvex ⊢ ( 𝑔 ‘ ∪ suc 𝑎 ) ∈ V
403 401 297 402 fvmpt ⊢ ( suc 𝑎 ∈ suc suc suc 𝑛 → ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc 𝑎 ) = ( 𝑔 ‘ ∪ suc 𝑎 ) )
404 393 403 syl ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc 𝑎 ) = ( 𝑔 ‘ ∪ suc 𝑎 ) )
405 nnord ⊢ ( 𝑎 ∈ ω → Ord 𝑎 )
406 377 405 syl ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → Ord 𝑎 )
407 ordunisuc ⊢ ( Ord 𝑎 → ∪ suc 𝑎 = 𝑎 )
408 406 407 syl ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → ∪ suc 𝑎 = 𝑎 )
409 408 fveq2d ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → ( 𝑔 ‘ ∪ suc 𝑎 ) = ( 𝑔 ‘ 𝑎 ) )
410 404 409 eqtrd ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc 𝑎 ) = ( 𝑔 ‘ 𝑎 ) )
411 380 390 410 3brtr4d ⊢ ( ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ∧ 𝑎 ∈ suc suc 𝑛 ) → ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc 𝑎 ) )
412 411 ralrimiva ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ∀ 𝑎 ∈ suc suc 𝑛 ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc 𝑎 ) )
413 264 sucex ⊢ suc suc suc 𝑛 ∈ V
414 413 mptex ⊢ ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ∈ V
415 fneq1 ⊢ ( 𝑓 = ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) → ( 𝑓 Fn suc suc suc 𝑛 ↔ ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) Fn suc suc suc 𝑛 ) )
416 fveq1 ⊢ ( 𝑓 = ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) → ( 𝑓 ‘ ∅ ) = ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ ∅ ) )
417 416 eqeq1d ⊢ ( 𝑓 = ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) → ( ( 𝑓 ‘ ∅ ) = 𝑦 ↔ ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ ∅ ) = 𝑦 ) )
418 fveq1 ⊢ ( 𝑓 = ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) → ( 𝑓 ‘ suc suc 𝑛 ) = ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc suc 𝑛 ) )
419 418 eqeq1d ⊢ ( 𝑓 = ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) → ( ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ↔ ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc suc 𝑛 ) = 𝑥 ) )
420 417 419 anbi12d ⊢ ( 𝑓 = ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) → ( ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ↔ ( ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ ∅ ) = 𝑦 ∧ ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc suc 𝑛 ) = 𝑥 ) ) )
421 fveq1 ⊢ ( 𝑓 = ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) → ( 𝑓 ‘ 𝑎 ) = ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ 𝑎 ) )
422 fveq1 ⊢ ( 𝑓 = ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) → ( 𝑓 ‘ suc 𝑎 ) = ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc 𝑎 ) )
423 421 422 breq12d ⊢ ( 𝑓 = ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) → ( ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ↔ ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc 𝑎 ) ) )
424 423 ralbidv ⊢ ( 𝑓 = ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) → ( ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ↔ ∀ 𝑎 ∈ suc suc 𝑛 ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( ( 𝑏 ∈ suc suc suc 𝑛 ↦ if ( 𝑏 = ∅ , 𝑦 , ( 𝑔 ‘ ∪ 𝑏 ) ) ) ‘ suc 𝑎 ) ) )
425 415 420 424 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 𝑎 ) ) ) )
426 414 425 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 𝑎 ) ) )
427 299 309 328 412 426 syl121anc ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) )
428 427 3exp ⊢ ( 𝑛 ∈ ω → ( ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) → ( 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 → ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) ) )
429 428 exlimdv ⊢ ( 𝑛 ∈ ω → ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) → ( 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 → ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) ) )
430 429 impd ⊢ ( 𝑛 ∈ ω → ( ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) )
431 430 exlimdv ⊢ ( 𝑛 ∈ ω → ( ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) → ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) )
432 294 431 impbid ⊢ ( 𝑛 ∈ ω → ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ) )
433 vex ⊢ 𝑧 ∈ V
434 433 brresi ⊢ ( 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) )
435 434 anbi2i ⊢ ( ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ↔ ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) )
436 435 exbii ⊢ ( ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑧 ) ↔ ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) )
437 432 436 bitrdi ⊢ ( 𝑛 ∈ ω → ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) ) )
438 215 437 vtoclg ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑛 ∈ ω → ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) ) ) )
439 438 impcom ⊢ ( ( 𝑛 ∈ ω ∧ 𝑋 ∈ 𝐴 ) → ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) ) )
440 439 adantrl ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) ) )
441 440 3adant3 ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) ) )
442 175 203 441 3bitr4rd ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ 𝑦 ∈ ( 𝐹 ‘ suc 𝑛 ) ) )
443 442 alrimiv ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ 𝑦 ∈ ( 𝐹 ‘ suc 𝑛 ) ) )
444 443 3exp ⊢ ( 𝑛 ∈ ω → ( ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ 𝑦 ∈ ( 𝐹 ‘ suc 𝑛 ) ) ) ) )
445 444 a2d ⊢ ( 𝑛 ∈ ω → ( ( ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑛 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑧 ∧ ( 𝑔 ‘ suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑐 ∈ suc 𝑛 ( 𝑔 ‘ 𝑐 ) ( 𝑅 ↾ 𝐴 ) ( 𝑔 ‘ suc 𝑐 ) ) ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ( ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc suc 𝑛 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ 𝑦 ∈ ( 𝐹 ‘ suc 𝑛 ) ) ) ) )
446 27 68 82 96 164 445 finds ⊢ ( 𝑁 ∈ ω → ( ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑁 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc 𝑁 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc 𝑁 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ 𝑦 ∈ ( 𝐹 ‘ 𝑁 ) ) ) )
447 446 3impib ⊢ ( ( 𝑁 ∈ ω ∧ 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑁 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc 𝑁 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc 𝑁 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ 𝑦 ∈ ( 𝐹 ‘ 𝑁 ) ) )
448 447 19.21bi ⊢ ( ( 𝑁 ∈ ω ∧ 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑁 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc 𝑁 ) = 𝑋 ) ∧ ∀ 𝑎 ∈ suc 𝑁 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ 𝑦 ∈ ( 𝐹 ‘ 𝑁 ) ) )