MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ttrclselem2 Structured version   Visualization version   GIF version

Theorem ttrclselem2 9721
Description: Lemma for ttrclse 9722. Show that a suc 𝑁 element long chain gives membership in the 𝑁-th predecessor class and vice-versa. (Contributed by Scott Fenton, 31-Oct-2024.)
Hypothesis
Ref Expression
ttrclselem.1 𝐹 = rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))
Assertion
Ref Expression
ttrclselem2 ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴𝑋𝐴) → (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁)))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑓,𝑤,𝑦   𝑦,𝐹   𝑁,𝑎,𝑓,𝑦   𝑅,𝑎,𝑏,𝑓,𝑤,𝑦   𝑋,𝑏,𝑓,𝑦
Allowed substitution hints:   𝐹(𝑤,𝑓,𝑎,𝑏)   𝑁(𝑤,𝑏)   𝑋(𝑤,𝑎)

Proof of Theorem ttrclselem2
Dummy variables 𝑐 𝑔 𝑚 𝑛 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 suceq 6431 . . . . . . . . . . . 12 (𝑚 = ∅ → suc 𝑚 = suc ∅)
2 df-1o 8466 . . . . . . . . . . . 12 1o = suc ∅
31, 2eqtr4di 2791 . . . . . . . . . . 11 (𝑚 = ∅ → suc 𝑚 = 1o)
4 suceq 6431 . . . . . . . . . . 11 (suc 𝑚 = 1o → suc suc 𝑚 = suc 1o)
53, 4syl 17 . . . . . . . . . 10 (𝑚 = ∅ → suc suc 𝑚 = suc 1o)
65fneq2d 6644 . . . . . . . . 9 (𝑚 = ∅ → (𝑓 Fn suc suc 𝑚𝑓 Fn suc 1o))
73fveqeq2d 6900 . . . . . . . . . 10 (𝑚 = ∅ → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘1o) = 𝑋))
87anbi2d 630 . . . . . . . . 9 (𝑚 = ∅ → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
9 df1o2 8473 . . . . . . . . . . . 12 1o = {∅}
103, 9eqtrdi 2789 . . . . . . . . . . 11 (𝑚 = ∅ → suc 𝑚 = {∅})
1110raleqdv 3326 . . . . . . . . . 10 (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ {∅} (𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
12 0ex 5308 . . . . . . . . . . 11 ∅ ∈ V
13 fveq2 6892 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑓𝑎) = (𝑓‘∅))
14 suceq 6431 . . . . . . . . . . . . . 14 (𝑎 = ∅ → suc 𝑎 = suc ∅)
1514, 2eqtr4di 2791 . . . . . . . . . . . . 13 (𝑎 = ∅ → suc 𝑎 = 1o)
1615fveq2d 6896 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘1o))
1713, 16breq12d 5162 . . . . . . . . . . 11 (𝑎 = ∅ → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)))
1812, 17ralsn 4686 . . . . . . . . . 10 (∀𝑎 ∈ {∅} (𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o))
1911, 18bitrdi 287 . . . . . . . . 9 (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)))
206, 8, 193anbi123d 1437 . . . . . . . 8 (𝑚 = ∅ → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o))))
2120exbidv 1925 . . . . . . 7 (𝑚 = ∅ → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o))))
22 fveq2 6892 . . . . . . . 8 (𝑚 = ∅ → (𝐹𝑚) = (𝐹‘∅))
2322eleq2d 2820 . . . . . . 7 (𝑚 = ∅ → (𝑦 ∈ (𝐹𝑚) ↔ 𝑦 ∈ (𝐹‘∅)))
2421, 23bibi12d 346 . . . . . 6 (𝑚 = ∅ → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅))))
2524albidv 1924 . . . . 5 (𝑚 = ∅ → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅))))
2625imbi2d 341 . . . 4 (𝑚 = ∅ → (((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚))) ↔ ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅)))))
27 suceq 6431 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → suc 𝑚 = suc 𝑛)
28 suceq 6431 . . . . . . . . . . . . 13 (suc 𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc 𝑛)
2927, 28syl 17 . . . . . . . . . . . 12 (𝑚 = 𝑛 → suc suc 𝑚 = suc suc 𝑛)
3029fneq2d 6644 . . . . . . . . . . 11 (𝑚 = 𝑛 → (𝑓 Fn suc suc 𝑚𝑓 Fn suc suc 𝑛))
3127fveqeq2d 6900 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc 𝑛) = 𝑋))
3231anbi2d 630 . . . . . . . . . . 11 (𝑚 = 𝑛 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋)))
3327raleqdv 3326 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
34 fveq2 6892 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → (𝑓𝑎) = (𝑓𝑐))
35 suceq 6431 . . . . . . . . . . . . . . 15 (𝑎 = 𝑐 → suc 𝑎 = suc 𝑐)
3635fveq2d 6896 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑐))
3734, 36breq12d 5162 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐)))
3837cbvralvw 3235 . . . . . . . . . . . 12 (∀𝑎 ∈ suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐))
3933, 38bitrdi 287 . . . . . . . . . . 11 (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐)))
4030, 32, 393anbi123d 1437 . . . . . . . . . 10 (𝑚 = 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐))))
4140exbidv 1925 . . . . . . . . 9 (𝑚 = 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐))))
42 fneq1 6641 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑓 Fn suc suc 𝑛𝑔 Fn suc suc 𝑛))
43 fveq1 6891 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓‘∅) = (𝑔‘∅))
4443eqeq1d 2735 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓‘∅) = 𝑦 ↔ (𝑔‘∅) = 𝑦))
45 fveq1 6891 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓‘suc 𝑛) = (𝑔‘suc 𝑛))
4645eqeq1d 2735 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓‘suc 𝑛) = 𝑋 ↔ (𝑔‘suc 𝑛) = 𝑋))
4744, 46anbi12d 632 . . . . . . . . . . 11 (𝑓 = 𝑔 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ↔ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋)))
48 fveq1 6891 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓𝑐) = (𝑔𝑐))
49 fveq1 6891 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓‘suc 𝑐) = (𝑔‘suc 𝑐))
5048, 49breq12d 5162 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐) ↔ (𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)))
5150ralbidv 3178 . . . . . . . . . . 11 (𝑓 = 𝑔 → (∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐) ↔ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)))
5242, 47, 513anbi123d 1437 . . . . . . . . . 10 (𝑓 = 𝑔 → ((𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
5352cbvexvw 2041 . . . . . . . . 9 (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)))
5441, 53bitrdi 287 . . . . . . . 8 (𝑚 = 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
55 fveq2 6892 . . . . . . . . 9 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
5655eleq2d 2820 . . . . . . . 8 (𝑚 = 𝑛 → (𝑦 ∈ (𝐹𝑚) ↔ 𝑦 ∈ (𝐹𝑛)))
5754, 56bibi12d 346 . . . . . . 7 (𝑚 = 𝑛 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹𝑛))))
5857albidv 1924 . . . . . 6 (𝑚 = 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹𝑛))))
59 eqeq2 2745 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑔‘∅) = 𝑦 ↔ (𝑔‘∅) = 𝑧))
6059anbi1d 631 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ↔ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋)))
61603anbi2d 1442 . . . . . . . . 9 (𝑦 = 𝑧 → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
6261exbidv 1925 . . . . . . . 8 (𝑦 = 𝑧 → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
63 eleq1 2822 . . . . . . . 8 (𝑦 = 𝑧 → (𝑦 ∈ (𝐹𝑛) ↔ 𝑧 ∈ (𝐹𝑛)))
6462, 63bibi12d 346 . . . . . . 7 (𝑦 = 𝑧 → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹𝑛)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))))
6564cbvalvw 2040 . . . . . 6 (∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹𝑛)) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛)))
6658, 65bitrdi 287 . . . . 5 (𝑚 = 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))))
6766imbi2d 341 . . . 4 (𝑚 = 𝑛 → (((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚))) ↔ ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛)))))
68 suceq 6431 . . . . . . . . . . 11 (𝑚 = suc 𝑛 → suc 𝑚 = suc suc 𝑛)
69 suceq 6431 . . . . . . . . . . 11 (suc 𝑚 = suc suc 𝑛 → suc suc 𝑚 = suc suc suc 𝑛)
7068, 69syl 17 . . . . . . . . . 10 (𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc suc 𝑛)
7170fneq2d 6644 . . . . . . . . 9 (𝑚 = suc 𝑛 → (𝑓 Fn suc suc 𝑚𝑓 Fn suc suc suc 𝑛))
7268fveqeq2d 6900 . . . . . . . . . 10 (𝑚 = suc 𝑛 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc suc 𝑛) = 𝑋))
7372anbi2d 630 . . . . . . . . 9 (𝑚 = suc 𝑛 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋)))
7468raleqdv 3326 . . . . . . . . 9 (𝑚 = suc 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
7571, 73, 743anbi123d 1437 . . . . . . . 8 (𝑚 = suc 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
7675exbidv 1925 . . . . . . 7 (𝑚 = suc 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
77 fveq2 6892 . . . . . . . 8 (𝑚 = suc 𝑛 → (𝐹𝑚) = (𝐹‘suc 𝑛))
7877eleq2d 2820 . . . . . . 7 (𝑚 = suc 𝑛 → (𝑦 ∈ (𝐹𝑚) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
7976, 78bibi12d 346 . . . . . 6 (𝑚 = suc 𝑛 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛))))
8079albidv 1924 . . . . 5 (𝑚 = suc 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛))))
8180imbi2d 341 . . . 4 (𝑚 = suc 𝑛 → (((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚))) ↔ ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))))
82 suceq 6431 . . . . . . . . . . 11 (𝑚 = 𝑁 → suc 𝑚 = suc 𝑁)
83 suceq 6431 . . . . . . . . . . 11 (suc 𝑚 = suc 𝑁 → suc suc 𝑚 = suc suc 𝑁)
8482, 83syl 17 . . . . . . . . . 10 (𝑚 = 𝑁 → suc suc 𝑚 = suc suc 𝑁)
8584fneq2d 6644 . . . . . . . . 9 (𝑚 = 𝑁 → (𝑓 Fn suc suc 𝑚𝑓 Fn suc suc 𝑁))
8682fveqeq2d 6900 . . . . . . . . . 10 (𝑚 = 𝑁 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc 𝑁) = 𝑋))
8786anbi2d 630 . . . . . . . . 9 (𝑚 = 𝑁 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋)))
8882raleqdv 3326 . . . . . . . . 9 (𝑚 = 𝑁 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
8985, 87, 883anbi123d 1437 . . . . . . . 8 (𝑚 = 𝑁 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
9089exbidv 1925 . . . . . . 7 (𝑚 = 𝑁 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
91 fveq2 6892 . . . . . . . 8 (𝑚 = 𝑁 → (𝐹𝑚) = (𝐹𝑁))
9291eleq2d 2820 . . . . . . 7 (𝑚 = 𝑁 → (𝑦 ∈ (𝐹𝑚) ↔ 𝑦 ∈ (𝐹𝑁)))
9390, 92bibi12d 346 . . . . . 6 (𝑚 = 𝑁 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁))))
9493albidv 1924 . . . . 5 (𝑚 = 𝑁 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁))))
9594imbi2d 341 . . . 4 (𝑚 = 𝑁 → (((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚))) ↔ ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁)))))
96 eqeq2 2745 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((𝑓‘1o) = 𝑥 ↔ (𝑓‘1o) = 𝑋))
9796anbi2d 630 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
9897anbi2d 630 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)) ↔ (𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋))))
9998exbidv 1925 . . . . . . . . . 10 (𝑥 = 𝑋 → (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)) ↔ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋))))
100 vex 3479 . . . . . . . . . . . . 13 𝑦 ∈ V
101 vex 3479 . . . . . . . . . . . . 13 𝑥 ∈ V
102100, 101ifex 4579 . . . . . . . . . . . 12 if(𝑏 = ∅, 𝑦, 𝑥) ∈ V
103 eqid 2733 . . . . . . . . . . . 12 (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))
104102, 103fnmpti 6694 . . . . . . . . . . 11 (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o
105 equid 2016 . . . . . . . . . . . 12 𝑦 = 𝑦
106 equid 2016 . . . . . . . . . . . 12 𝑥 = 𝑥
107105, 106pm3.2i 472 . . . . . . . . . . 11 (𝑦 = 𝑦𝑥 = 𝑥)
108 1oex 8476 . . . . . . . . . . . . . 14 1o ∈ V
109108sucex 7794 . . . . . . . . . . . . 13 suc 1o ∈ V
110109mptex 7225 . . . . . . . . . . . 12 (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) ∈ V
111 fneq1 6641 . . . . . . . . . . . . 13 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓 Fn suc 1o ↔ (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o))
112 fveq1 6891 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘∅) = ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅))
113 1on 8478 . . . . . . . . . . . . . . . . . 18 1o ∈ On
114113onordi 6476 . . . . . . . . . . . . . . . . 17 Ord 1o
115 0elsuc 7823 . . . . . . . . . . . . . . . . 17 (Ord 1o → ∅ ∈ suc 1o)
116 iftrue 4535 . . . . . . . . . . . . . . . . . 18 (𝑏 = ∅ → if(𝑏 = ∅, 𝑦, 𝑥) = 𝑦)
117116, 103, 100fvmpt 6999 . . . . . . . . . . . . . . . . 17 (∅ ∈ suc 1o → ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅) = 𝑦)
118114, 115, 117mp2b 10 . . . . . . . . . . . . . . . 16 ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅) = 𝑦
119112, 118eqtrdi 2789 . . . . . . . . . . . . . . 15 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘∅) = 𝑦)
120119eqeq1d 2735 . . . . . . . . . . . . . 14 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓‘∅) = 𝑦𝑦 = 𝑦))
121 fveq1 6891 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘1o) = ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1o))
122108sucid 6447 . . . . . . . . . . . . . . . . 17 1o ∈ suc 1o
123 eqeq1 2737 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 1o → (𝑏 = ∅ ↔ 1o = ∅))
124123ifbid 4552 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1o → if(𝑏 = ∅, 𝑦, 𝑥) = if(1o = ∅, 𝑦, 𝑥))
125 1n0 8488 . . . . . . . . . . . . . . . . . . . . 21 1o ≠ ∅
126125neii 2943 . . . . . . . . . . . . . . . . . . . 20 ¬ 1o = ∅
127126iffalsei 4539 . . . . . . . . . . . . . . . . . . 19 if(1o = ∅, 𝑦, 𝑥) = 𝑥
128124, 127eqtrdi 2789 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1o → if(𝑏 = ∅, 𝑦, 𝑥) = 𝑥)
129128, 103, 101fvmpt 6999 . . . . . . . . . . . . . . . . 17 (1o ∈ suc 1o → ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1o) = 𝑥)
130122, 129ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1o) = 𝑥
131121, 130eqtrdi 2789 . . . . . . . . . . . . . . 15 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘1o) = 𝑥)
132131eqeq1d 2735 . . . . . . . . . . . . . 14 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓‘1o) = 𝑥𝑥 = 𝑥))
133120, 132anbi12d 632 . . . . . . . . . . . . 13 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥) ↔ (𝑦 = 𝑦𝑥 = 𝑥)))
134111, 133anbi12d 632 . . . . . . . . . . . 12 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)) ↔ ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o ∧ (𝑦 = 𝑦𝑥 = 𝑥))))
135110, 134spcev 3597 . . . . . . . . . . 11 (((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o ∧ (𝑦 = 𝑦𝑥 = 𝑥)) → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)))
136104, 107, 135mp2an 691 . . . . . . . . . 10 𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥))
13799, 136vtoclg 3557 . . . . . . . . 9 (𝑋𝐴 → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
138137adantl 483 . . . . . . . 8 ((𝑅 Se 𝐴𝑋𝐴) → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
139138biantrurd 534 . . . . . . 7 ((𝑅 Se 𝐴𝑋𝐴) → ((𝑦𝐴𝑦𝑅𝑋) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑦𝐴𝑦𝑅𝑋))))
140100elpred 6318 . . . . . . . 8 (𝑋𝐴 → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑦𝐴𝑦𝑅𝑋)))
141140adantl 483 . . . . . . 7 ((𝑅 Se 𝐴𝑋𝐴) → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑦𝐴𝑦𝑅𝑋)))
142 brres 5989 . . . . . . . . 9 (𝑋𝐴 → (𝑦(𝑅𝐴)𝑋 ↔ (𝑦𝐴𝑦𝑅𝑋)))
143142adantl 483 . . . . . . . 8 ((𝑅 Se 𝐴𝑋𝐴) → (𝑦(𝑅𝐴)𝑋 ↔ (𝑦𝐴𝑦𝑅𝑋)))
144143anbi2d 630 . . . . . . 7 ((𝑅 Se 𝐴𝑋𝐴) → ((∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑦𝐴𝑦𝑅𝑋))))
145139, 141, 1443bitr4rd 312 . . . . . 6 ((𝑅 Se 𝐴𝑋𝐴) → ((∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋) ↔ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑋)))
146 df-3an 1090 . . . . . . . . . 10 ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)))
147 breq12 5154 . . . . . . . . . . . 12 (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) → ((𝑓‘∅)(𝑅𝐴)(𝑓‘1o) ↔ 𝑦(𝑅𝐴)𝑋))
148147adantl 483 . . . . . . . . . . 11 ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) → ((𝑓‘∅)(𝑅𝐴)(𝑓‘1o) ↔ 𝑦(𝑅𝐴)𝑋))
149148pm5.32i 576 . . . . . . . . . 10 (((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋))
150146, 149bitri 275 . . . . . . . . 9 ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋))
151150exbii 1851 . . . . . . . 8 (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ ∃𝑓((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋))
152 19.41v 1954 . . . . . . . 8 (∃𝑓((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋))
153151, 152bitri 275 . . . . . . 7 (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋))
154153a1i 11 . . . . . 6 ((𝑅 Se 𝐴𝑋𝐴) → (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋)))
155 ttrclselem.1 . . . . . . . . 9 𝐹 = rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))
156155fveq1i 6893 . . . . . . . 8 (𝐹‘∅) = (rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅)
157 setlikespec 6327 . . . . . . . . . 10 ((𝑋𝐴𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
158157ancoms 460 . . . . . . . . 9 ((𝑅 Se 𝐴𝑋𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
159 rdg0g 8427 . . . . . . . . 9 (Pred(𝑅, 𝐴, 𝑋) ∈ V → (rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅) = Pred(𝑅, 𝐴, 𝑋))
160158, 159syl 17 . . . . . . . 8 ((𝑅 Se 𝐴𝑋𝐴) → (rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅) = Pred(𝑅, 𝐴, 𝑋))
161156, 160eqtrid 2785 . . . . . . 7 ((𝑅 Se 𝐴𝑋𝐴) → (𝐹‘∅) = Pred(𝑅, 𝐴, 𝑋))
162161eleq2d 2820 . . . . . 6 ((𝑅 Se 𝐴𝑋𝐴) → (𝑦 ∈ (𝐹‘∅) ↔ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑋)))
163145, 154, 1623bitr4d 311 . . . . 5 ((𝑅 Se 𝐴𝑋𝐴) → (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅)))
164163alrimiv 1931 . . . 4 ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅)))
165 eliun 5002 . . . . . . . . . 10 (𝑦 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧 ∈ (𝐹𝑛)𝑦 ∈ Pred(𝑅, 𝐴, 𝑧))
166 df-rex 3072 . . . . . . . . . 10 (∃𝑧 ∈ (𝐹𝑛)𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)))
167165, 166bitri 275 . . . . . . . . 9 (𝑦 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)))
168100elpred 6318 . . . . . . . . . . . . . 14 (𝑧 ∈ V → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ (𝑦𝐴𝑦𝑅𝑧)))
169168elv 3481 . . . . . . . . . . . . 13 (𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ (𝑦𝐴𝑦𝑅𝑧))
170169anbi2i 624 . . . . . . . . . . . 12 ((𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ (𝑧 ∈ (𝐹𝑛) ∧ (𝑦𝐴𝑦𝑅𝑧)))
171 anbi1 633 . . . . . . . . . . . 12 ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛)) → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)) ↔ (𝑧 ∈ (𝐹𝑛) ∧ (𝑦𝐴𝑦𝑅𝑧))))
172170, 171bitr4id 290 . . . . . . . . . . 11 ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛)) → ((𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
173172alexbii 1836 . . . . . . . . . 10 (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛)) → (∃𝑧(𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
1741733ad2ant3 1136 . . . . . . . . 9 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → (∃𝑧(𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
175167, 174bitrid 283 . . . . . . . 8 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → (𝑦 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
176 nnon 7861 . . . . . . . . . . 11 (𝑛 ∈ ω → 𝑛 ∈ On)
177 fvex 6905 . . . . . . . . . . . 12 (𝐹𝑛) ∈ V
178155ttrclselem1 9720 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (𝐹𝑛) ⊆ 𝐴)
179178adantr 482 . . . . . . . . . . . . . 14 ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → (𝐹𝑛) ⊆ 𝐴)
180 dfse3 6338 . . . . . . . . . . . . . . . 16 (𝑅 Se 𝐴 ↔ ∀𝑧𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
181180biimpi 215 . . . . . . . . . . . . . . 15 (𝑅 Se 𝐴 → ∀𝑧𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
182181adantl 483 . . . . . . . . . . . . . 14 ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → ∀𝑧𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
183 ssralv 4051 . . . . . . . . . . . . . 14 ((𝐹𝑛) ⊆ 𝐴 → (∀𝑧𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V → ∀𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V))
184179, 182, 183sylc 65 . . . . . . . . . . . . 13 ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → ∀𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
185184adantrr 716 . . . . . . . . . . . 12 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴)) → ∀𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
186 iunexg 7950 . . . . . . . . . . . 12 (((𝐹𝑛) ∈ V ∧ ∀𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V) → 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
187177, 185, 186sylancr 588 . . . . . . . . . . 11 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴)) → 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
188 nfcv 2904 . . . . . . . . . . . 12 𝑏Pred(𝑅, 𝐴, 𝑋)
189 nfcv 2904 . . . . . . . . . . . 12 𝑏𝑛
190 nfmpt1 5257 . . . . . . . . . . . . . . . 16 𝑏(𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤))
191190, 188nfrdg 8414 . . . . . . . . . . . . . . 15 𝑏rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))
192155, 191nfcxfr 2902 . . . . . . . . . . . . . 14 𝑏𝐹
193192, 189nffv 6902 . . . . . . . . . . . . 13 𝑏(𝐹𝑛)
194 nfcv 2904 . . . . . . . . . . . . 13 𝑏Pred(𝑅, 𝐴, 𝑧)
195193, 194nfiun 5028 . . . . . . . . . . . 12 𝑏 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧)
196 predeq3 6305 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
197196cbviunv 5044 . . . . . . . . . . . . 13 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤) = 𝑧𝑏 Pred(𝑅, 𝐴, 𝑧)
198 iuneq1 5014 . . . . . . . . . . . . 13 (𝑏 = (𝐹𝑛) → 𝑧𝑏 Pred(𝑅, 𝐴, 𝑧) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
199197, 198eqtrid 2785 . . . . . . . . . . . 12 (𝑏 = (𝐹𝑛) → 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
200188, 189, 195, 155, 199rdgsucmptf 8428 . . . . . . . . . . 11 ((𝑛 ∈ On ∧ 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V) → (𝐹‘suc 𝑛) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
201176, 187, 200syl2an2r 684 . . . . . . . . . 10 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴)) → (𝐹‘suc 𝑛) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
2022013adant3 1133 . . . . . . . . 9 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → (𝐹‘suc 𝑛) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
203202eleq2d 2820 . . . . . . . 8 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → (𝑦 ∈ (𝐹‘suc 𝑛) ↔ 𝑦 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧)))
204 eqeq2 2745 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → ((𝑓‘suc suc 𝑛) = 𝑥 ↔ (𝑓‘suc suc 𝑛) = 𝑋))
205204anbi2d 630 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋)))
2062053anbi2d 1442 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
207206exbidv 1925 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
208 eqeq2 2745 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → ((𝑔‘suc 𝑛) = 𝑥 ↔ (𝑔‘suc 𝑛) = 𝑋))
209208anbi2d 630 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → (((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋)))
2102093anbi2d 1442 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
211210exbidv 1925 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
212211anbi1d 631 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
213212exbidv 1925 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
214207, 213bibi12d 346 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((∃𝑓(𝑓 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 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)))))
215214imbi2d 341 . . . . . . . . . . . 12 (𝑥 = 𝑋 → ((𝑛 ∈ ω → (∃𝑓(𝑓 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 6905 . . . . . . . . . . . . . . . . . . . 20 (𝑓‘suc 𝑏) ∈ V
217 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))
218216, 217fnmpti 6694 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) Fn suc suc 𝑛
219218a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) Fn suc suc 𝑛)
220 peano2 7881 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
221220adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → suc 𝑛 ∈ ω)
222 nnord 7863 . . . . . . . . . . . . . . . . . . . . 21 (suc 𝑛 ∈ ω → Ord suc 𝑛)
223221, 222syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → Ord suc 𝑛)
224 0elsuc 7823 . . . . . . . . . . . . . . . . . . . 20 (Ord suc 𝑛 → ∅ ∈ suc suc 𝑛)
225223, 224syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∅ ∈ suc suc 𝑛)
226 suceq 6431 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = ∅ → suc 𝑏 = suc ∅)
227226fveq2d 6896 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = ∅ → (𝑓‘suc 𝑏) = (𝑓‘suc ∅))
228 fvex 6905 . . . . . . . . . . . . . . . . . . . 20 (𝑓‘suc ∅) ∈ V
229227, 217, 228fvmpt 6999 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅))
230225, 229syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅))
231 vex 3479 . . . . . . . . . . . . . . . . . . . . . 22 𝑛 ∈ V
232231sucex 7794 . . . . . . . . . . . . . . . . . . . . 21 suc 𝑛 ∈ V
233232sucid 6447 . . . . . . . . . . . . . . . . . . . 20 suc 𝑛 ∈ suc suc 𝑛
234 suceq 6431 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = suc 𝑛 → suc 𝑏 = suc suc 𝑛)
235234fveq2d 6896 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = suc 𝑛 → (𝑓‘suc 𝑏) = (𝑓‘suc suc 𝑛))
236 fvex 6905 . . . . . . . . . . . . . . . . . . . . 21 (𝑓‘suc suc 𝑛) ∈ V
237235, 217, 236fvmpt 6999 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑛 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = (𝑓‘suc suc 𝑛))
238233, 237mp1i 13 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = (𝑓‘suc suc 𝑛))
239 simpr2r 1234 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → (𝑓‘suc suc 𝑛) = 𝑥)
240238, 239eqtrd 2773 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥)
241 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = suc 𝑐 → (𝑓𝑎) = (𝑓‘suc 𝑐))
242 suceq 6431 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = suc 𝑐 → suc 𝑎 = suc suc 𝑐)
243242fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = suc 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc suc 𝑐))
244241, 243breq12d 5162 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = suc 𝑐 → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘suc 𝑐)(𝑅𝐴)(𝑓‘suc suc 𝑐)))
245 simplr3 1218 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))
246 ordsucelsuc 7810 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord suc 𝑛 → (𝑐 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc suc 𝑛))
247223, 246syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → (𝑐 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc suc 𝑛))
248247biimpa 478 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → suc 𝑐 ∈ suc suc 𝑛)
249244, 245, 248rspcdva 3614 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → (𝑓‘suc 𝑐)(𝑅𝐴)(𝑓‘suc suc 𝑐))
250 elelsuc 6438 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ suc 𝑛𝑐 ∈ suc suc 𝑛)
251 suceq 6431 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = 𝑐 → suc 𝑏 = suc 𝑐)
252251fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = 𝑐 → (𝑓‘suc 𝑏) = (𝑓‘suc 𝑐))
253 fvex 6905 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓‘suc 𝑐) ∈ V
254252, 217, 253fvmpt 6999 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
255250, 254syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 ∈ suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
256255adantl 483 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
257 suceq 6431 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = suc 𝑐 → suc 𝑏 = suc suc 𝑐)
258257fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = suc 𝑐 → (𝑓‘suc 𝑏) = (𝑓‘suc suc 𝑐))
259 fvex 6905 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓‘suc suc 𝑐) ∈ V
260258, 217, 259fvmpt 6999 . . . . . . . . . . . . . . . . . . . . 21 (suc 𝑐 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐) = (𝑓‘suc suc 𝑐))
261248, 260syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐) = (𝑓‘suc suc 𝑐))
262249, 256, 2613brtr4d 5181 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
263262ralrimiva 3147 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∀𝑐 ∈ suc 𝑛((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
264232sucex 7794 . . . . . . . . . . . . . . . . . . . 20 suc suc 𝑛 ∈ V
265264mptex 7225 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) ∈ V
266 fneq1 6641 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔 Fn suc suc 𝑛 ↔ (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) Fn suc suc 𝑛))
267 fveq1 6891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘∅) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅))
268267eqeq1d 2735 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔‘∅) = (𝑓‘suc ∅) ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅)))
269 fveq1 6891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘suc 𝑛) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛))
270269eqeq1d 2735 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔‘suc 𝑛) = 𝑥 ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥))
271268, 270anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ (((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅) ∧ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥)))
272 fveq1 6891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔𝑐) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐))
273 fveq1 6891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘suc 𝑐) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
274272, 273breq12d 5162 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐) ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐)))
275274ralbidv 3178 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐) ↔ ∀𝑐 ∈ suc 𝑛((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐)))
276266, 271, 2753anbi123d 1437 . . . . . . . . . . . . . . . . . . 19 (𝑔 = (𝑏 ∈ 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 𝑐))))
277265, 276spcev 3597 . . . . . . . . . . . . . . . . . 18 (((𝑏 ∈ 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 𝑐)))
278219, 230, 240, 263, 277syl121anc 1376 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)))
279 simpr2l 1233 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → (𝑓‘∅) = 𝑦)
28014fveq2d 6896 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘suc ∅))
28113, 280breq12d 5162 . . . . . . . . . . . . . . . . . . 19 (𝑎 = ∅ → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅𝐴)(𝑓‘suc ∅)))
282 simpr3 1197 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))
283281, 282, 225rspcdva 3614 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → (𝑓‘∅)(𝑅𝐴)(𝑓‘suc ∅))
284279, 283eqbrtrrd 5173 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → 𝑦(𝑅𝐴)(𝑓‘suc ∅))
285 eqeq2 2745 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (𝑓‘suc ∅) → ((𝑔‘∅) = 𝑧 ↔ (𝑔‘∅) = (𝑓‘suc ∅)))
286285anbi1d 631 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = (𝑓‘suc ∅) → (((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥)))
2872863anbi2d 1442 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑓‘suc ∅) → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
288287exbidv 1925 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑓‘suc ∅) → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
289 breq2 5153 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑓‘suc ∅) → (𝑦(𝑅𝐴)𝑧𝑦(𝑅𝐴)(𝑓‘suc ∅)))
290288, 289anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑓‘suc ∅) → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)(𝑓‘suc ∅))))
291228, 290spcev 3597 . . . . . . . . . . . . . . . . 17 ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)(𝑓‘suc ∅)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧))
292278, 284, 291syl2anc 585 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧))
293292ex 414 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → ((𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧)))
294293exlimdv 1937 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧)))
295 fvex 6905 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 𝑏) ∈ V
296100, 295ifex 4579 . . . . . . . . . . . . . . . . . . . . 21 if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) ∈ V
297 eqid 2733 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))
298296, 297fnmpti 6694 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) Fn suc suc suc 𝑛
299298a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) Fn suc suc suc 𝑛)
300 peano2 7881 . . . . . . . . . . . . . . . . . . . . . . . 24 (suc 𝑛 ∈ ω → suc suc 𝑛 ∈ ω)
301220, 300syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ω → suc suc 𝑛 ∈ ω)
3023013ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → suc suc 𝑛 ∈ ω)
303 nnord 7863 . . . . . . . . . . . . . . . . . . . . . 22 (suc suc 𝑛 ∈ ω → Ord suc suc 𝑛)
304302, 303syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → Ord suc suc 𝑛)
305 0elsuc 7823 . . . . . . . . . . . . . . . . . . . . 21 (Ord suc suc 𝑛 → ∅ ∈ suc suc suc 𝑛)
306304, 305syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∅ ∈ suc suc suc 𝑛)
307 iftrue 4535 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = ∅ → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = 𝑦)
308307, 297, 100fvmpt 6999 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅) = 𝑦)
309306, 308syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅) = 𝑦)
310264sucid 6447 . . . . . . . . . . . . . . . . . . . . 21 suc suc 𝑛 ∈ suc suc suc 𝑛
311 eqeq1 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = suc suc 𝑛 → (𝑏 = ∅ ↔ suc suc 𝑛 = ∅))
312 unieq 4920 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = suc suc 𝑛 𝑏 = suc suc 𝑛)
313312fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = suc suc 𝑛 → (𝑔 𝑏) = (𝑔 suc suc 𝑛))
314311, 313ifbieq2d 4555 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = suc suc 𝑛 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = if(suc suc 𝑛 = ∅, 𝑦, (𝑔 suc suc 𝑛)))
315 nsuceq0 6448 . . . . . . . . . . . . . . . . . . . . . . . . 25 suc suc 𝑛 ≠ ∅
316315neii 2943 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ suc suc 𝑛 = ∅
317316iffalsei 4539 . . . . . . . . . . . . . . . . . . . . . . 23 if(suc suc 𝑛 = ∅, 𝑦, (𝑔 suc suc 𝑛)) = (𝑔 suc suc 𝑛)
318314, 317eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = suc suc 𝑛 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = (𝑔 suc suc 𝑛))
319 fvex 6905 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 suc suc 𝑛) ∈ V
320318, 297, 319fvmpt 6999 . . . . . . . . . . . . . . . . . . . . 21 (suc suc 𝑛 ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛) = (𝑔 suc suc 𝑛))
321310, 320mp1i 13 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛) = (𝑔 suc suc 𝑛))
3222203ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → suc 𝑛 ∈ ω)
323322, 222syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → Ord suc 𝑛)
324 ordunisuc 7820 . . . . . . . . . . . . . . . . . . . . . 22 (Ord suc 𝑛 suc suc 𝑛 = suc 𝑛)
325323, 324syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → suc suc 𝑛 = suc 𝑛)
326325fveq2d 6896 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑔 suc suc 𝑛) = (𝑔‘suc 𝑛))
327 simp22r 1294 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑔‘suc 𝑛) = 𝑥)
328321, 326, 3273eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛) = 𝑥)
329 simpl3 1194 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 = ∅) → 𝑦(𝑅𝐴)𝑧)
330 iftrue 4535 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) = 𝑦)
331330adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 = ∅) → if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) = 𝑦)
332 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = ∅ → (𝑔𝑎) = (𝑔‘∅))
333 simp22l 1293 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑔‘∅) = 𝑧)
334332, 333sylan9eqr 2795 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 = ∅) → (𝑔𝑎) = 𝑧)
335329, 331, 3343brtr4d 5181 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 = ∅) → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎))
336335ex 414 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎)))
337336adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎)))
338 ordsucelsuc 7810 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Ord suc 𝑛 → (𝑏 ∈ suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
339323, 338syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑏 ∈ suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
340 elnn 7866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑏 ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → 𝑏 ∈ ω)
341322, 340sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑏 ∈ suc 𝑛 ∧ (𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧)) → 𝑏 ∈ ω)
342341ancoms 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → 𝑏 ∈ ω)
343 nnord 7863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑏 ∈ ω → Ord 𝑏)
344342, 343syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → Ord 𝑏)
345 ordunisuc 7820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Ord 𝑏 suc 𝑏 = 𝑏)
346344, 345syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → suc 𝑏 = 𝑏)
347346fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔 suc 𝑏) = (𝑔𝑏))
348 simp23 1209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))
349 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = 𝑏 → (𝑔𝑐) = (𝑔𝑏))
350 suceq 6431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑏 → suc 𝑐 = suc 𝑏)
351350fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = 𝑏 → (𝑔‘suc 𝑐) = (𝑔‘suc 𝑏))
352349, 351breq12d 5162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑏 → ((𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐) ↔ (𝑔𝑏)(𝑅𝐴)(𝑔‘suc 𝑏)))
353352rspcv 3609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 ∈ suc 𝑛 → (∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐) → (𝑔𝑏)(𝑅𝐴)(𝑔‘suc 𝑏)))
354348, 353mpan9 508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔𝑏)(𝑅𝐴)(𝑔‘suc 𝑏))
355347, 354eqbrtrd 5171 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏))
356355ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑏 ∈ suc 𝑛 → (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏)))
357339, 356sylbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (suc 𝑏 ∈ suc suc 𝑛 → (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏)))
358357imp 408 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛) → (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏))
359 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = suc 𝑏 → (𝑎 ∈ suc suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
360359anbi2d 630 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = suc 𝑏 → (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) ↔ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛)))
361 eqeq1 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = suc 𝑏 → (𝑎 = ∅ ↔ suc 𝑏 = ∅))
362 unieq 4920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = suc 𝑏 𝑎 = suc 𝑏)
363362fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = suc 𝑏 → (𝑔 𝑎) = (𝑔 suc 𝑏))
364361, 363ifbieq2d 4555 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) = if(suc 𝑏 = ∅, 𝑦, (𝑔 suc 𝑏)))
365 nsuceq0 6448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 suc 𝑏 ≠ ∅
366365neii 2943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ¬ suc 𝑏 = ∅
367366iffalsei 4539 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 if(suc 𝑏 = ∅, 𝑦, (𝑔 suc 𝑏)) = (𝑔 suc 𝑏)
368364, 367eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) = (𝑔 suc 𝑏))
369 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = suc 𝑏 → (𝑔𝑎) = (𝑔‘suc 𝑏))
370368, 369breq12d 5162 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = suc 𝑏 → (if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎) ↔ (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏)))
371360, 370imbi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = suc 𝑏 → ((((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎)) ↔ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛) → (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏))))
372358, 371mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = suc 𝑏 → (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎)))
373372com12 32 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎)))
374373rexlimdvw 3161 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (∃𝑏 ∈ ω 𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎)))
375 elnn 7866 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ suc suc 𝑛 ∧ suc suc 𝑛 ∈ ω) → 𝑎 ∈ ω)
376375ancoms 460 . . . . . . . . . . . . . . . . . . . . . . . 24 ((suc suc 𝑛 ∈ ω ∧ 𝑎 ∈ suc suc 𝑛) → 𝑎 ∈ ω)
377302, 376sylan 581 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → 𝑎 ∈ ω)
378 nn0suc 7886 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ ω → (𝑎 = ∅ ∨ ∃𝑏 ∈ ω 𝑎 = suc 𝑏))
379377, 378syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑎 = ∅ ∨ ∃𝑏 ∈ ω 𝑎 = suc 𝑏))
380337, 374, 379mpjaod 859 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎))
381 elelsuc 6438 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ suc suc 𝑛𝑎 ∈ suc suc suc 𝑛)
382 eqeq1 2737 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = 𝑎 → (𝑏 = ∅ ↔ 𝑎 = ∅))
383 unieq 4920 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 = 𝑎 𝑏 = 𝑎)
384383fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = 𝑎 → (𝑔 𝑏) = (𝑔 𝑎))
385382, 384ifbieq2d 4555 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = if(𝑎 = ∅, 𝑦, (𝑔 𝑎)))
386 fvex 6905 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔 𝑎) ∈ V
387100, 386ifex 4579 . . . . . . . . . . . . . . . . . . . . . . . 24 if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) ∈ V
388385, 297, 387fvmpt 6999 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔 𝑎)))
389381, 388syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔 𝑎)))
390389adantl 483 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔 𝑎)))
391 ordsucelsuc 7810 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord suc suc 𝑛 → (𝑎 ∈ suc suc 𝑛 ↔ suc 𝑎 ∈ suc suc suc 𝑛))
392304, 391syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑎 ∈ suc suc 𝑛 ↔ suc 𝑎 ∈ suc suc suc 𝑛))
393392biimpa 478 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → suc 𝑎 ∈ suc suc suc 𝑛)
394 eqeq1 2737 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 = suc 𝑎 → (𝑏 = ∅ ↔ suc 𝑎 = ∅))
395 unieq 4920 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = suc 𝑎 𝑏 = suc 𝑎)
396395fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 = suc 𝑎 → (𝑔 𝑏) = (𝑔 suc 𝑎))
397394, 396ifbieq2d 4555 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = suc 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = if(suc 𝑎 = ∅, 𝑦, (𝑔 suc 𝑎)))
398 nsuceq0 6448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 suc 𝑎 ≠ ∅
399398neii 2943 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ¬ suc 𝑎 = ∅
400399iffalsei 4539 . . . . . . . . . . . . . . . . . . . . . . . . 25 if(suc 𝑎 = ∅, 𝑦, (𝑔 suc 𝑎)) = (𝑔 suc 𝑎)
401397, 400eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = suc 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = (𝑔 suc 𝑎))
402 fvex 6905 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 suc 𝑎) ∈ V
403401, 297, 402fvmpt 6999 . . . . . . . . . . . . . . . . . . . . . . 23 (suc 𝑎 ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎) = (𝑔 suc 𝑎))
404393, 403syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎) = (𝑔 suc 𝑎))
405 nnord 7863 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ ω → Ord 𝑎)
406377, 405syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → Ord 𝑎)
407 ordunisuc 7820 . . . . . . . . . . . . . . . . . . . . . . . 24 (Ord 𝑎 suc 𝑎 = 𝑎)
408406, 407syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → suc 𝑎 = 𝑎)
409408fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑔 suc 𝑎) = (𝑔𝑎))
410404, 409eqtrd 2773 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎) = (𝑔𝑎))
411380, 390, 4103brtr4d 5181 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎)(𝑅𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎))
412411ralrimiva 3147 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∀𝑎 ∈ suc suc 𝑛((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎)(𝑅𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎))
413264sucex 7794 . . . . . . . . . . . . . . . . . . . . 21 suc suc suc 𝑛 ∈ V
414413mptex 7225 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) ∈ V
415 fneq1 6641 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓 Fn suc suc suc 𝑛 ↔ (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) Fn suc suc suc 𝑛))
416 fveq1 6891 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓‘∅) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅))
417416eqeq1d 2735 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → ((𝑓‘∅) = 𝑦 ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅) = 𝑦))
418 fveq1 6891 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓‘suc suc 𝑛) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛))
419418eqeq1d 2735 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → ((𝑓‘suc suc 𝑛) = 𝑥 ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛) = 𝑥))
420417, 419anbi12d 632 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ↔ (((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅) = 𝑦 ∧ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛) = 𝑥)))
421 fveq1 6891 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓𝑎) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎))
422 fveq1 6891 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓‘suc 𝑎) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎))
423421, 422breq12d 5162 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎)(𝑅𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎)))
424423ralbidv 3178 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑛((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎)(𝑅𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎)))
425415, 420, 4243anbi123d 1437 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑏 ∈ 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 𝑎))))
426414, 425spcev 3597 . . . . . . . . . . . . . . . . . . 19 (((𝑏 ∈ 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 𝑎)))
427299, 309, 328, 412, 426syl121anc 1376 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
4284273exp 1120 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) → (𝑦(𝑅𝐴)𝑧 → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))))
429428exlimdv 1937 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) → (𝑦(𝑅𝐴)𝑧 → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))))
430429impd 412 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
431430exlimdv 1937 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
432294, 431impbid 211 . . . . . . . . . . . . 13 (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧)))
433 vex 3479 . . . . . . . . . . . . . . . 16 𝑧 ∈ V
434433brresi 5991 . . . . . . . . . . . . . . 15 (𝑦(𝑅𝐴)𝑧 ↔ (𝑦𝐴𝑦𝑅𝑧))
435434anbi2i 624 . . . . . . . . . . . . . 14 ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)))
436435exbii 1851 . . . . . . . . . . . . 13 (∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)))
437432, 436bitrdi 287 . . . . . . . . . . . 12 (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
438215, 437vtoclg 3557 . . . . . . . . . . 11 (𝑋𝐴 → (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)))))
439438impcom 409 . . . . . . . . . 10 ((𝑛 ∈ ω ∧ 𝑋𝐴) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
440439adantrl 715 . . . . . . . . 9 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴)) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
4414403adant3 1133 . . . . . . . 8 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
442175, 203, 4413bitr4rd 312 . . . . . . 7 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
443442alrimiv 1931 . . . . . 6 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
4444433exp 1120 . . . . 5 (𝑛 ∈ ω → ((𝑅 Se 𝐴𝑋𝐴) → (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛)) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))))
445444a2d 29 . . . 4 (𝑛 ∈ ω → (((𝑅 Se 𝐴𝑋𝐴) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))))
44626, 67, 81, 95, 164, 445finds 7889 . . 3 (𝑁 ∈ ω → ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁))))
4474463impib 1117 . 2 ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁)))
44844719.21bi 2183 1 ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴𝑋𝐴) → (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wo 846  w3a 1088  wal 1540   = wceq 1542  wex 1782  wcel 2107  wral 3062  wrex 3071  Vcvv 3475  wss 3949  c0 4323  ifcif 4529  {csn 4629   cuni 4909   ciun 4998   class class class wbr 5149  cmpt 5232   Se wse 5630  cres 5679  Predcpred 6300  Ord word 6364  Oncon0 6365  suc csuc 6367   Fn wfn 6539  cfv 6544  ωcom 7855  reccrdg 8409  1oc1o 8459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466
This theorem is referenced by:  ttrclse  9722
  Copyright terms: Public domain W3C validator