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

Theorem ttrclselem2 9723
Description: Lemma for ttrclse 9724. 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 6429 . . . . . . . . . . . 12 (𝑚 = ∅ → suc 𝑚 = suc ∅)
2 df-1o 8468 . . . . . . . . . . . 12 1o = suc ∅
31, 2eqtr4di 2788 . . . . . . . . . . 11 (𝑚 = ∅ → suc 𝑚 = 1o)
4 suceq 6429 . . . . . . . . . . 11 (suc 𝑚 = 1o → suc suc 𝑚 = suc 1o)
53, 4syl 17 . . . . . . . . . 10 (𝑚 = ∅ → suc suc 𝑚 = suc 1o)
65fneq2d 6642 . . . . . . . . 9 (𝑚 = ∅ → (𝑓 Fn suc suc 𝑚𝑓 Fn suc 1o))
73fveqeq2d 6898 . . . . . . . . . 10 (𝑚 = ∅ → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘1o) = 𝑋))
87anbi2d 627 . . . . . . . . 9 (𝑚 = ∅ → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
9 df1o2 8475 . . . . . . . . . . . 12 1o = {∅}
103, 9eqtrdi 2786 . . . . . . . . . . 11 (𝑚 = ∅ → suc 𝑚 = {∅})
1110raleqdv 3323 . . . . . . . . . 10 (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ {∅} (𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
12 0ex 5306 . . . . . . . . . . 11 ∅ ∈ V
13 fveq2 6890 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑓𝑎) = (𝑓‘∅))
14 suceq 6429 . . . . . . . . . . . . . 14 (𝑎 = ∅ → suc 𝑎 = suc ∅)
1514, 2eqtr4di 2788 . . . . . . . . . . . . 13 (𝑎 = ∅ → suc 𝑎 = 1o)
1615fveq2d 6894 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘1o))
1713, 16breq12d 5160 . . . . . . . . . . 11 (𝑎 = ∅ → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)))
1812, 17ralsn 4684 . . . . . . . . . 10 (∀𝑎 ∈ {∅} (𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o))
1911, 18bitrdi 286 . . . . . . . . 9 (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)))
206, 8, 193anbi123d 1434 . . . . . . . 8 (𝑚 = ∅ → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o))))
2120exbidv 1922 . . . . . . 7 (𝑚 = ∅ → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o))))
22 fveq2 6890 . . . . . . . 8 (𝑚 = ∅ → (𝐹𝑚) = (𝐹‘∅))
2322eleq2d 2817 . . . . . . 7 (𝑚 = ∅ → (𝑦 ∈ (𝐹𝑚) ↔ 𝑦 ∈ (𝐹‘∅)))
2421, 23bibi12d 344 . . . . . 6 (𝑚 = ∅ → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅))))
2524albidv 1921 . . . . 5 (𝑚 = ∅ → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅))))
2625imbi2d 339 . . . 4 (𝑚 = ∅ → (((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚))) ↔ ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅)))))
27 suceq 6429 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → suc 𝑚 = suc 𝑛)
28 suceq 6429 . . . . . . . . . . . . 13 (suc 𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc 𝑛)
2927, 28syl 17 . . . . . . . . . . . 12 (𝑚 = 𝑛 → suc suc 𝑚 = suc suc 𝑛)
3029fneq2d 6642 . . . . . . . . . . 11 (𝑚 = 𝑛 → (𝑓 Fn suc suc 𝑚𝑓 Fn suc suc 𝑛))
3127fveqeq2d 6898 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc 𝑛) = 𝑋))
3231anbi2d 627 . . . . . . . . . . 11 (𝑚 = 𝑛 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋)))
3327raleqdv 3323 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
34 fveq2 6890 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → (𝑓𝑎) = (𝑓𝑐))
35 suceq 6429 . . . . . . . . . . . . . . 15 (𝑎 = 𝑐 → suc 𝑎 = suc 𝑐)
3635fveq2d 6894 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑐))
3734, 36breq12d 5160 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐)))
3837cbvralvw 3232 . . . . . . . . . . . 12 (∀𝑎 ∈ suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐))
3933, 38bitrdi 286 . . . . . . . . . . 11 (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐)))
4030, 32, 393anbi123d 1434 . . . . . . . . . 10 (𝑚 = 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐))))
4140exbidv 1922 . . . . . . . . 9 (𝑚 = 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐))))
42 fneq1 6639 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑓 Fn suc suc 𝑛𝑔 Fn suc suc 𝑛))
43 fveq1 6889 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓‘∅) = (𝑔‘∅))
4443eqeq1d 2732 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓‘∅) = 𝑦 ↔ (𝑔‘∅) = 𝑦))
45 fveq1 6889 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓‘suc 𝑛) = (𝑔‘suc 𝑛))
4645eqeq1d 2732 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓‘suc 𝑛) = 𝑋 ↔ (𝑔‘suc 𝑛) = 𝑋))
4744, 46anbi12d 629 . . . . . . . . . . 11 (𝑓 = 𝑔 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ↔ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋)))
48 fveq1 6889 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓𝑐) = (𝑔𝑐))
49 fveq1 6889 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓‘suc 𝑐) = (𝑔‘suc 𝑐))
5048, 49breq12d 5160 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐) ↔ (𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)))
5150ralbidv 3175 . . . . . . . . . . 11 (𝑓 = 𝑔 → (∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐) ↔ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)))
5242, 47, 513anbi123d 1434 . . . . . . . . . 10 (𝑓 = 𝑔 → ((𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
5352cbvexvw 2038 . . . . . . . . 9 (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)))
5441, 53bitrdi 286 . . . . . . . 8 (𝑚 = 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
55 fveq2 6890 . . . . . . . . 9 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
5655eleq2d 2817 . . . . . . . 8 (𝑚 = 𝑛 → (𝑦 ∈ (𝐹𝑚) ↔ 𝑦 ∈ (𝐹𝑛)))
5754, 56bibi12d 344 . . . . . . 7 (𝑚 = 𝑛 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹𝑛))))
5857albidv 1921 . . . . . 6 (𝑚 = 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹𝑛))))
59 eqeq2 2742 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑔‘∅) = 𝑦 ↔ (𝑔‘∅) = 𝑧))
6059anbi1d 628 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ↔ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋)))
61603anbi2d 1439 . . . . . . . . 9 (𝑦 = 𝑧 → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
6261exbidv 1922 . . . . . . . 8 (𝑦 = 𝑧 → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
63 eleq1 2819 . . . . . . . 8 (𝑦 = 𝑧 → (𝑦 ∈ (𝐹𝑛) ↔ 𝑧 ∈ (𝐹𝑛)))
6462, 63bibi12d 344 . . . . . . 7 (𝑦 = 𝑧 → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹𝑛)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))))
6564cbvalvw 2037 . . . . . 6 (∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹𝑛)) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛)))
6658, 65bitrdi 286 . . . . 5 (𝑚 = 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))))
6766imbi2d 339 . . . 4 (𝑚 = 𝑛 → (((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚))) ↔ ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛)))))
68 suceq 6429 . . . . . . . . . . 11 (𝑚 = suc 𝑛 → suc 𝑚 = suc suc 𝑛)
69 suceq 6429 . . . . . . . . . . 11 (suc 𝑚 = suc suc 𝑛 → suc suc 𝑚 = suc suc suc 𝑛)
7068, 69syl 17 . . . . . . . . . 10 (𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc suc 𝑛)
7170fneq2d 6642 . . . . . . . . 9 (𝑚 = suc 𝑛 → (𝑓 Fn suc suc 𝑚𝑓 Fn suc suc suc 𝑛))
7268fveqeq2d 6898 . . . . . . . . . 10 (𝑚 = suc 𝑛 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc suc 𝑛) = 𝑋))
7372anbi2d 627 . . . . . . . . 9 (𝑚 = suc 𝑛 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋)))
7468raleqdv 3323 . . . . . . . . 9 (𝑚 = suc 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
7571, 73, 743anbi123d 1434 . . . . . . . 8 (𝑚 = suc 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
7675exbidv 1922 . . . . . . 7 (𝑚 = suc 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
77 fveq2 6890 . . . . . . . 8 (𝑚 = suc 𝑛 → (𝐹𝑚) = (𝐹‘suc 𝑛))
7877eleq2d 2817 . . . . . . 7 (𝑚 = suc 𝑛 → (𝑦 ∈ (𝐹𝑚) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
7976, 78bibi12d 344 . . . . . 6 (𝑚 = suc 𝑛 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛))))
8079albidv 1921 . . . . 5 (𝑚 = suc 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛))))
8180imbi2d 339 . . . 4 (𝑚 = suc 𝑛 → (((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚))) ↔ ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))))
82 suceq 6429 . . . . . . . . . . 11 (𝑚 = 𝑁 → suc 𝑚 = suc 𝑁)
83 suceq 6429 . . . . . . . . . . 11 (suc 𝑚 = suc 𝑁 → suc suc 𝑚 = suc suc 𝑁)
8482, 83syl 17 . . . . . . . . . 10 (𝑚 = 𝑁 → suc suc 𝑚 = suc suc 𝑁)
8584fneq2d 6642 . . . . . . . . 9 (𝑚 = 𝑁 → (𝑓 Fn suc suc 𝑚𝑓 Fn suc suc 𝑁))
8682fveqeq2d 6898 . . . . . . . . . 10 (𝑚 = 𝑁 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc 𝑁) = 𝑋))
8786anbi2d 627 . . . . . . . . 9 (𝑚 = 𝑁 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋)))
8882raleqdv 3323 . . . . . . . . 9 (𝑚 = 𝑁 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
8985, 87, 883anbi123d 1434 . . . . . . . 8 (𝑚 = 𝑁 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
9089exbidv 1922 . . . . . . 7 (𝑚 = 𝑁 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
91 fveq2 6890 . . . . . . . 8 (𝑚 = 𝑁 → (𝐹𝑚) = (𝐹𝑁))
9291eleq2d 2817 . . . . . . 7 (𝑚 = 𝑁 → (𝑦 ∈ (𝐹𝑚) ↔ 𝑦 ∈ (𝐹𝑁)))
9390, 92bibi12d 344 . . . . . 6 (𝑚 = 𝑁 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁))))
9493albidv 1921 . . . . 5 (𝑚 = 𝑁 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁))))
9594imbi2d 339 . . . 4 (𝑚 = 𝑁 → (((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚))) ↔ ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁)))))
96 eqeq2 2742 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((𝑓‘1o) = 𝑥 ↔ (𝑓‘1o) = 𝑋))
9796anbi2d 627 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
9897anbi2d 627 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)) ↔ (𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋))))
9998exbidv 1922 . . . . . . . . . 10 (𝑥 = 𝑋 → (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)) ↔ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋))))
100 vex 3476 . . . . . . . . . . . . 13 𝑦 ∈ V
101 vex 3476 . . . . . . . . . . . . 13 𝑥 ∈ V
102100, 101ifex 4577 . . . . . . . . . . . 12 if(𝑏 = ∅, 𝑦, 𝑥) ∈ V
103 eqid 2730 . . . . . . . . . . . 12 (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))
104102, 103fnmpti 6692 . . . . . . . . . . 11 (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o
105 equid 2013 . . . . . . . . . . . 12 𝑦 = 𝑦
106 equid 2013 . . . . . . . . . . . 12 𝑥 = 𝑥
107105, 106pm3.2i 469 . . . . . . . . . . 11 (𝑦 = 𝑦𝑥 = 𝑥)
108 1oex 8478 . . . . . . . . . . . . . 14 1o ∈ V
109108sucex 7796 . . . . . . . . . . . . 13 suc 1o ∈ V
110109mptex 7226 . . . . . . . . . . . 12 (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) ∈ V
111 fneq1 6639 . . . . . . . . . . . . 13 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓 Fn suc 1o ↔ (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o))
112 fveq1 6889 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘∅) = ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅))
113 1on 8480 . . . . . . . . . . . . . . . . . 18 1o ∈ On
114113onordi 6474 . . . . . . . . . . . . . . . . 17 Ord 1o
115 0elsuc 7825 . . . . . . . . . . . . . . . . 17 (Ord 1o → ∅ ∈ suc 1o)
116 iftrue 4533 . . . . . . . . . . . . . . . . . 18 (𝑏 = ∅ → if(𝑏 = ∅, 𝑦, 𝑥) = 𝑦)
117116, 103, 100fvmpt 6997 . . . . . . . . . . . . . . . . 17 (∅ ∈ suc 1o → ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅) = 𝑦)
118114, 115, 117mp2b 10 . . . . . . . . . . . . . . . 16 ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅) = 𝑦
119112, 118eqtrdi 2786 . . . . . . . . . . . . . . 15 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘∅) = 𝑦)
120119eqeq1d 2732 . . . . . . . . . . . . . 14 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓‘∅) = 𝑦𝑦 = 𝑦))
121 fveq1 6889 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘1o) = ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1o))
122108sucid 6445 . . . . . . . . . . . . . . . . 17 1o ∈ suc 1o
123 eqeq1 2734 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 1o → (𝑏 = ∅ ↔ 1o = ∅))
124123ifbid 4550 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1o → if(𝑏 = ∅, 𝑦, 𝑥) = if(1o = ∅, 𝑦, 𝑥))
125 1n0 8490 . . . . . . . . . . . . . . . . . . . . 21 1o ≠ ∅
126125neii 2940 . . . . . . . . . . . . . . . . . . . 20 ¬ 1o = ∅
127126iffalsei 4537 . . . . . . . . . . . . . . . . . . 19 if(1o = ∅, 𝑦, 𝑥) = 𝑥
128124, 127eqtrdi 2786 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1o → if(𝑏 = ∅, 𝑦, 𝑥) = 𝑥)
129128, 103, 101fvmpt 6997 . . . . . . . . . . . . . . . . 17 (1o ∈ suc 1o → ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1o) = 𝑥)
130122, 129ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1o) = 𝑥
131121, 130eqtrdi 2786 . . . . . . . . . . . . . . 15 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘1o) = 𝑥)
132131eqeq1d 2732 . . . . . . . . . . . . . 14 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓‘1o) = 𝑥𝑥 = 𝑥))
133120, 132anbi12d 629 . . . . . . . . . . . . 13 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥) ↔ (𝑦 = 𝑦𝑥 = 𝑥)))
134111, 133anbi12d 629 . . . . . . . . . . . 12 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)) ↔ ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o ∧ (𝑦 = 𝑦𝑥 = 𝑥))))
135110, 134spcev 3595 . . . . . . . . . . 11 (((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o ∧ (𝑦 = 𝑦𝑥 = 𝑥)) → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)))
136104, 107, 135mp2an 688 . . . . . . . . . 10 𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥))
13799, 136vtoclg 3541 . . . . . . . . 9 (𝑋𝐴 → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
138137adantl 480 . . . . . . . 8 ((𝑅 Se 𝐴𝑋𝐴) → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
139138biantrurd 531 . . . . . . 7 ((𝑅 Se 𝐴𝑋𝐴) → ((𝑦𝐴𝑦𝑅𝑋) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑦𝐴𝑦𝑅𝑋))))
140100elpred 6316 . . . . . . . 8 (𝑋𝐴 → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑦𝐴𝑦𝑅𝑋)))
141140adantl 480 . . . . . . 7 ((𝑅 Se 𝐴𝑋𝐴) → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑦𝐴𝑦𝑅𝑋)))
142 brres 5987 . . . . . . . . 9 (𝑋𝐴 → (𝑦(𝑅𝐴)𝑋 ↔ (𝑦𝐴𝑦𝑅𝑋)))
143142adantl 480 . . . . . . . 8 ((𝑅 Se 𝐴𝑋𝐴) → (𝑦(𝑅𝐴)𝑋 ↔ (𝑦𝐴𝑦𝑅𝑋)))
144143anbi2d 627 . . . . . . 7 ((𝑅 Se 𝐴𝑋𝐴) → ((∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑦𝐴𝑦𝑅𝑋))))
145139, 141, 1443bitr4rd 311 . . . . . 6 ((𝑅 Se 𝐴𝑋𝐴) → ((∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋) ↔ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑋)))
146 df-3an 1087 . . . . . . . . . 10 ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)))
147 breq12 5152 . . . . . . . . . . . 12 (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) → ((𝑓‘∅)(𝑅𝐴)(𝑓‘1o) ↔ 𝑦(𝑅𝐴)𝑋))
148147adantl 480 . . . . . . . . . . 11 ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) → ((𝑓‘∅)(𝑅𝐴)(𝑓‘1o) ↔ 𝑦(𝑅𝐴)𝑋))
149148pm5.32i 573 . . . . . . . . . 10 (((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋))
150146, 149bitri 274 . . . . . . . . 9 ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋))
151150exbii 1848 . . . . . . . 8 (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ ∃𝑓((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋))
152 19.41v 1951 . . . . . . . 8 (∃𝑓((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋))
153151, 152bitri 274 . . . . . . 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 6891 . . . . . . . 8 (𝐹‘∅) = (rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅)
157 setlikespec 6325 . . . . . . . . . 10 ((𝑋𝐴𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
158157ancoms 457 . . . . . . . . 9 ((𝑅 Se 𝐴𝑋𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
159 rdg0g 8429 . . . . . . . . 9 (Pred(𝑅, 𝐴, 𝑋) ∈ V → (rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅) = Pred(𝑅, 𝐴, 𝑋))
160158, 159syl 17 . . . . . . . 8 ((𝑅 Se 𝐴𝑋𝐴) → (rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅) = Pred(𝑅, 𝐴, 𝑋))
161156, 160eqtrid 2782 . . . . . . 7 ((𝑅 Se 𝐴𝑋𝐴) → (𝐹‘∅) = Pred(𝑅, 𝐴, 𝑋))
162161eleq2d 2817 . . . . . 6 ((𝑅 Se 𝐴𝑋𝐴) → (𝑦 ∈ (𝐹‘∅) ↔ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑋)))
163145, 154, 1623bitr4d 310 . . . . 5 ((𝑅 Se 𝐴𝑋𝐴) → (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅)))
164163alrimiv 1928 . . . 4 ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅)))
165 eliun 5000 . . . . . . . . . 10 (𝑦 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧 ∈ (𝐹𝑛)𝑦 ∈ Pred(𝑅, 𝐴, 𝑧))
166 df-rex 3069 . . . . . . . . . 10 (∃𝑧 ∈ (𝐹𝑛)𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)))
167165, 166bitri 274 . . . . . . . . 9 (𝑦 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)))
168100elpred 6316 . . . . . . . . . . . . . 14 (𝑧 ∈ V → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ (𝑦𝐴𝑦𝑅𝑧)))
169168elv 3478 . . . . . . . . . . . . 13 (𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ (𝑦𝐴𝑦𝑅𝑧))
170169anbi2i 621 . . . . . . . . . . . 12 ((𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ (𝑧 ∈ (𝐹𝑛) ∧ (𝑦𝐴𝑦𝑅𝑧)))
171 anbi1 630 . . . . . . . . . . . 12 ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛)) → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)) ↔ (𝑧 ∈ (𝐹𝑛) ∧ (𝑦𝐴𝑦𝑅𝑧))))
172170, 171bitr4id 289 . . . . . . . . . . 11 ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛)) → ((𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
173172alexbii 1833 . . . . . . . . . 10 (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛)) → (∃𝑧(𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
1741733ad2ant3 1133 . . . . . . . . 9 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → (∃𝑧(𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
175167, 174bitrid 282 . . . . . . . 8 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → (𝑦 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
176 nnon 7863 . . . . . . . . . . 11 (𝑛 ∈ ω → 𝑛 ∈ On)
177 fvex 6903 . . . . . . . . . . . 12 (𝐹𝑛) ∈ V
178155ttrclselem1 9722 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (𝐹𝑛) ⊆ 𝐴)
179178adantr 479 . . . . . . . . . . . . . 14 ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → (𝐹𝑛) ⊆ 𝐴)
180 dfse3 6336 . . . . . . . . . . . . . . . 16 (𝑅 Se 𝐴 ↔ ∀𝑧𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
181180biimpi 215 . . . . . . . . . . . . . . 15 (𝑅 Se 𝐴 → ∀𝑧𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
182181adantl 480 . . . . . . . . . . . . . 14 ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → ∀𝑧𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
183 ssralv 4049 . . . . . . . . . . . . . 14 ((𝐹𝑛) ⊆ 𝐴 → (∀𝑧𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V → ∀𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V))
184179, 182, 183sylc 65 . . . . . . . . . . . . 13 ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → ∀𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
185184adantrr 713 . . . . . . . . . . . 12 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴)) → ∀𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
186 iunexg 7952 . . . . . . . . . . . 12 (((𝐹𝑛) ∈ V ∧ ∀𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V) → 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
187177, 185, 186sylancr 585 . . . . . . . . . . 11 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴)) → 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
188 nfcv 2901 . . . . . . . . . . . 12 𝑏Pred(𝑅, 𝐴, 𝑋)
189 nfcv 2901 . . . . . . . . . . . 12 𝑏𝑛
190 nfmpt1 5255 . . . . . . . . . . . . . . . 16 𝑏(𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤))
191190, 188nfrdg 8416 . . . . . . . . . . . . . . 15 𝑏rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))
192155, 191nfcxfr 2899 . . . . . . . . . . . . . 14 𝑏𝐹
193192, 189nffv 6900 . . . . . . . . . . . . 13 𝑏(𝐹𝑛)
194 nfcv 2901 . . . . . . . . . . . . 13 𝑏Pred(𝑅, 𝐴, 𝑧)
195193, 194nfiun 5026 . . . . . . . . . . . 12 𝑏 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧)
196 predeq3 6303 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
197196cbviunv 5042 . . . . . . . . . . . . 13 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤) = 𝑧𝑏 Pred(𝑅, 𝐴, 𝑧)
198 iuneq1 5012 . . . . . . . . . . . . 13 (𝑏 = (𝐹𝑛) → 𝑧𝑏 Pred(𝑅, 𝐴, 𝑧) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
199197, 198eqtrid 2782 . . . . . . . . . . . 12 (𝑏 = (𝐹𝑛) → 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
200188, 189, 195, 155, 199rdgsucmptf 8430 . . . . . . . . . . 11 ((𝑛 ∈ On ∧ 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V) → (𝐹‘suc 𝑛) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
201176, 187, 200syl2an2r 681 . . . . . . . . . 10 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴)) → (𝐹‘suc 𝑛) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
2022013adant3 1130 . . . . . . . . 9 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → (𝐹‘suc 𝑛) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
203202eleq2d 2817 . . . . . . . 8 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → (𝑦 ∈ (𝐹‘suc 𝑛) ↔ 𝑦 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧)))
204 eqeq2 2742 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → ((𝑓‘suc suc 𝑛) = 𝑥 ↔ (𝑓‘suc suc 𝑛) = 𝑋))
205204anbi2d 627 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋)))
2062053anbi2d 1439 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
207206exbidv 1922 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
208 eqeq2 2742 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → ((𝑔‘suc 𝑛) = 𝑥 ↔ (𝑔‘suc 𝑛) = 𝑋))
209208anbi2d 627 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → (((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋)))
2102093anbi2d 1439 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
211210exbidv 1922 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
212211anbi1d 628 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
213212exbidv 1922 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
214207, 213bibi12d 344 . . . . . . . . . . . . 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 339 . . . . . . . . . . . 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 6903 . . . . . . . . . . . . . . . . . . . 20 (𝑓‘suc 𝑏) ∈ V
217 eqid 2730 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))
218216, 217fnmpti 6692 . . . . . . . . . . . . . . . . . . 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 7883 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
221220adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → suc 𝑛 ∈ ω)
222 nnord 7865 . . . . . . . . . . . . . . . . . . . . 21 (suc 𝑛 ∈ ω → Ord suc 𝑛)
223221, 222syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → Ord suc 𝑛)
224 0elsuc 7825 . . . . . . . . . . . . . . . . . . . 20 (Ord suc 𝑛 → ∅ ∈ suc suc 𝑛)
225223, 224syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∅ ∈ suc suc 𝑛)
226 suceq 6429 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = ∅ → suc 𝑏 = suc ∅)
227226fveq2d 6894 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = ∅ → (𝑓‘suc 𝑏) = (𝑓‘suc ∅))
228 fvex 6903 . . . . . . . . . . . . . . . . . . . 20 (𝑓‘suc ∅) ∈ V
229227, 217, 228fvmpt 6997 . . . . . . . . . . . . . . . . . . 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 3476 . . . . . . . . . . . . . . . . . . . . . 22 𝑛 ∈ V
232231sucex 7796 . . . . . . . . . . . . . . . . . . . . 21 suc 𝑛 ∈ V
233232sucid 6445 . . . . . . . . . . . . . . . . . . . 20 suc 𝑛 ∈ suc suc 𝑛
234 suceq 6429 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = suc 𝑛 → suc 𝑏 = suc suc 𝑛)
235234fveq2d 6894 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = suc 𝑛 → (𝑓‘suc 𝑏) = (𝑓‘suc suc 𝑛))
236 fvex 6903 . . . . . . . . . . . . . . . . . . . . 21 (𝑓‘suc suc 𝑛) ∈ V
237235, 217, 236fvmpt 6997 . . . . . . . . . . . . . . . . . . . 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 1231 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → (𝑓‘suc suc 𝑛) = 𝑥)
240238, 239eqtrd 2770 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥)
241 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = suc 𝑐 → (𝑓𝑎) = (𝑓‘suc 𝑐))
242 suceq 6429 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = suc 𝑐 → suc 𝑎 = suc suc 𝑐)
243242fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = suc 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc suc 𝑐))
244241, 243breq12d 5160 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = suc 𝑐 → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘suc 𝑐)(𝑅𝐴)(𝑓‘suc suc 𝑐)))
245 simplr3 1215 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))
246 ordsucelsuc 7812 . . . . . . . . . . . . . . . . . . . . . . 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 475 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → suc 𝑐 ∈ suc suc 𝑛)
249244, 245, 248rspcdva 3612 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → (𝑓‘suc 𝑐)(𝑅𝐴)(𝑓‘suc suc 𝑐))
250 elelsuc 6436 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ suc 𝑛𝑐 ∈ suc suc 𝑛)
251 suceq 6429 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = 𝑐 → suc 𝑏 = suc 𝑐)
252251fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = 𝑐 → (𝑓‘suc 𝑏) = (𝑓‘suc 𝑐))
253 fvex 6903 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓‘suc 𝑐) ∈ V
254252, 217, 253fvmpt 6997 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
255250, 254syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 ∈ suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
256255adantl 480 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
257 suceq 6429 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = suc 𝑐 → suc 𝑏 = suc suc 𝑐)
258257fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = suc 𝑐 → (𝑓‘suc 𝑏) = (𝑓‘suc suc 𝑐))
259 fvex 6903 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓‘suc suc 𝑐) ∈ V
260258, 217, 259fvmpt 6997 . . . . . . . . . . . . . . . . . . . . 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 5179 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
263262ralrimiva 3144 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∀𝑐 ∈ suc 𝑛((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
264232sucex 7796 . . . . . . . . . . . . . . . . . . . 20 suc suc 𝑛 ∈ V
265264mptex 7226 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) ∈ V
266 fneq1 6639 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔 Fn suc suc 𝑛 ↔ (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) Fn suc suc 𝑛))
267 fveq1 6889 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘∅) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅))
268267eqeq1d 2732 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔‘∅) = (𝑓‘suc ∅) ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅)))
269 fveq1 6889 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘suc 𝑛) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛))
270269eqeq1d 2732 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔‘suc 𝑛) = 𝑥 ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥))
271268, 270anbi12d 629 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ (((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅) ∧ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥)))
272 fveq1 6889 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔𝑐) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐))
273 fveq1 6889 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘suc 𝑐) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
274272, 273breq12d 5160 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐) ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐)))
275274ralbidv 3175 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐) ↔ ∀𝑐 ∈ suc 𝑛((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐)))
276266, 271, 2753anbi123d 1434 . . . . . . . . . . . . . . . . . . 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 3595 . . . . . . . . . . . . . . . . . 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 1373 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)))
279 simpr2l 1230 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → (𝑓‘∅) = 𝑦)
28014fveq2d 6894 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘suc ∅))
28113, 280breq12d 5160 . . . . . . . . . . . . . . . . . . 19 (𝑎 = ∅ → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅𝐴)(𝑓‘suc ∅)))
282 simpr3 1194 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))
283281, 282, 225rspcdva 3612 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → (𝑓‘∅)(𝑅𝐴)(𝑓‘suc ∅))
284279, 283eqbrtrrd 5171 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → 𝑦(𝑅𝐴)(𝑓‘suc ∅))
285 eqeq2 2742 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (𝑓‘suc ∅) → ((𝑔‘∅) = 𝑧 ↔ (𝑔‘∅) = (𝑓‘suc ∅)))
286285anbi1d 628 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = (𝑓‘suc ∅) → (((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥)))
2872863anbi2d 1439 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑓‘suc ∅) → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
288287exbidv 1922 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑓‘suc ∅) → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
289 breq2 5151 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑓‘suc ∅) → (𝑦(𝑅𝐴)𝑧𝑦(𝑅𝐴)(𝑓‘suc ∅)))
290288, 289anbi12d 629 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑓‘suc ∅) → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)(𝑓‘suc ∅))))
291228, 290spcev 3595 . . . . . . . . . . . . . . . . 17 ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)(𝑓‘suc ∅)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧))
292278, 284, 291syl2anc 582 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧))
293292ex 411 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → ((𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧)))
294293exlimdv 1934 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧)))
295 fvex 6903 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 𝑏) ∈ V
296100, 295ifex 4577 . . . . . . . . . . . . . . . . . . . . 21 if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) ∈ V
297 eqid 2730 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))
298296, 297fnmpti 6692 . . . . . . . . . . . . . . . . . . . 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 7883 . . . . . . . . . . . . . . . . . . . . . . . 24 (suc 𝑛 ∈ ω → suc suc 𝑛 ∈ ω)
301220, 300syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ω → suc suc 𝑛 ∈ ω)
3023013ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → suc suc 𝑛 ∈ ω)
303 nnord 7865 . . . . . . . . . . . . . . . . . . . . . 22 (suc suc 𝑛 ∈ ω → Ord suc suc 𝑛)
304302, 303syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → Ord suc suc 𝑛)
305 0elsuc 7825 . . . . . . . . . . . . . . . . . . . . 21 (Ord suc suc 𝑛 → ∅ ∈ suc suc suc 𝑛)
306304, 305syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∅ ∈ suc suc suc 𝑛)
307 iftrue 4533 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = ∅ → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = 𝑦)
308307, 297, 100fvmpt 6997 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅) = 𝑦)
309306, 308syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅) = 𝑦)
310264sucid 6445 . . . . . . . . . . . . . . . . . . . . 21 suc suc 𝑛 ∈ suc suc suc 𝑛
311 eqeq1 2734 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = suc suc 𝑛 → (𝑏 = ∅ ↔ suc suc 𝑛 = ∅))
312 unieq 4918 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = suc suc 𝑛 𝑏 = suc suc 𝑛)
313312fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = suc suc 𝑛 → (𝑔 𝑏) = (𝑔 suc suc 𝑛))
314311, 313ifbieq2d 4553 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = suc suc 𝑛 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = if(suc suc 𝑛 = ∅, 𝑦, (𝑔 suc suc 𝑛)))
315 nsuceq0 6446 . . . . . . . . . . . . . . . . . . . . . . . . 25 suc suc 𝑛 ≠ ∅
316315neii 2940 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ suc suc 𝑛 = ∅
317316iffalsei 4537 . . . . . . . . . . . . . . . . . . . . . . 23 if(suc suc 𝑛 = ∅, 𝑦, (𝑔 suc suc 𝑛)) = (𝑔 suc suc 𝑛)
318314, 317eqtrdi 2786 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = suc suc 𝑛 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = (𝑔 suc suc 𝑛))
319 fvex 6903 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 suc suc 𝑛) ∈ V
320318, 297, 319fvmpt 6997 . . . . . . . . . . . . . . . . . . . . 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 1131 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → suc 𝑛 ∈ ω)
323322, 222syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → Ord suc 𝑛)
324 ordunisuc 7822 . . . . . . . . . . . . . . . . . . . . . 22 (Ord suc 𝑛 suc suc 𝑛 = suc 𝑛)
325323, 324syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → suc suc 𝑛 = suc 𝑛)
326325fveq2d 6894 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑔 suc suc 𝑛) = (𝑔‘suc 𝑛))
327 simp22r 1291 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑔‘suc 𝑛) = 𝑥)
328321, 326, 3273eqtrd 2774 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛) = 𝑥)
329 simpl3 1191 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 = ∅) → 𝑦(𝑅𝐴)𝑧)
330 iftrue 4533 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) = 𝑦)
331330adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 = ∅) → if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) = 𝑦)
332 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = ∅ → (𝑔𝑎) = (𝑔‘∅))
333 simp22l 1290 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑔‘∅) = 𝑧)
334332, 333sylan9eqr 2792 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 = ∅) → (𝑔𝑎) = 𝑧)
335329, 331, 3343brtr4d 5179 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 = ∅) → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎))
336335ex 411 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎)))
337336adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎)))
338 ordsucelsuc 7812 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Ord suc 𝑛 → (𝑏 ∈ suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
339323, 338syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑏 ∈ suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
340 elnn 7868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑏 ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → 𝑏 ∈ ω)
341322, 340sylan2 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑏 ∈ suc 𝑛 ∧ (𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧)) → 𝑏 ∈ ω)
342341ancoms 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → 𝑏 ∈ ω)
343 nnord 7865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑏 ∈ ω → Ord 𝑏)
344342, 343syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → Ord 𝑏)
345 ordunisuc 7822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Ord 𝑏 suc 𝑏 = 𝑏)
346344, 345syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → suc 𝑏 = 𝑏)
347346fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔 suc 𝑏) = (𝑔𝑏))
348 simp23 1206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))
349 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = 𝑏 → (𝑔𝑐) = (𝑔𝑏))
350 suceq 6429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑏 → suc 𝑐 = suc 𝑏)
351350fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = 𝑏 → (𝑔‘suc 𝑐) = (𝑔‘suc 𝑏))
352349, 351breq12d 5160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑏 → ((𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐) ↔ (𝑔𝑏)(𝑅𝐴)(𝑔‘suc 𝑏)))
353352rspcv 3607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 ∈ suc 𝑛 → (∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐) → (𝑔𝑏)(𝑅𝐴)(𝑔‘suc 𝑏)))
354348, 353mpan9 505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔𝑏)(𝑅𝐴)(𝑔‘suc 𝑏))
355347, 354eqbrtrd 5169 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏))
356355ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑏 ∈ suc 𝑛 → (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏)))
357339, 356sylbird 259 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (suc 𝑏 ∈ suc suc 𝑛 → (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏)))
358357imp 405 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛) → (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏))
359 eleq1 2819 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = suc 𝑏 → (𝑎 ∈ suc suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
360359anbi2d 627 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = suc 𝑏 → (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) ↔ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛)))
361 eqeq1 2734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = suc 𝑏 → (𝑎 = ∅ ↔ suc 𝑏 = ∅))
362 unieq 4918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = suc 𝑏 𝑎 = suc 𝑏)
363362fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = suc 𝑏 → (𝑔 𝑎) = (𝑔 suc 𝑏))
364361, 363ifbieq2d 4553 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) = if(suc 𝑏 = ∅, 𝑦, (𝑔 suc 𝑏)))
365 nsuceq0 6446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 suc 𝑏 ≠ ∅
366365neii 2940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ¬ suc 𝑏 = ∅
367366iffalsei 4537 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 if(suc 𝑏 = ∅, 𝑦, (𝑔 suc 𝑏)) = (𝑔 suc 𝑏)
368364, 367eqtrdi 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) = (𝑔 suc 𝑏))
369 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = suc 𝑏 → (𝑔𝑎) = (𝑔‘suc 𝑏))
370368, 369breq12d 5160 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = suc 𝑏 → (if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎) ↔ (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏)))
371360, 370imbi12d 343 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = suc 𝑏 → ((((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎)) ↔ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛) → (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏))))
372358, 371mpbiri 257 . . . . . . . . . . . . . . . . . . . . . . . 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 3158 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (∃𝑏 ∈ ω 𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎)))
375 elnn 7868 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ suc suc 𝑛 ∧ suc suc 𝑛 ∈ ω) → 𝑎 ∈ ω)
376375ancoms 457 . . . . . . . . . . . . . . . . . . . . . . . 24 ((suc suc 𝑛 ∈ ω ∧ 𝑎 ∈ suc suc 𝑛) → 𝑎 ∈ ω)
377302, 376sylan 578 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → 𝑎 ∈ ω)
378 nn0suc 7888 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ ω → (𝑎 = ∅ ∨ ∃𝑏 ∈ ω 𝑎 = suc 𝑏))
379377, 378syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑎 = ∅ ∨ ∃𝑏 ∈ ω 𝑎 = suc 𝑏))
380337, 374, 379mpjaod 856 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎))
381 elelsuc 6436 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ suc suc 𝑛𝑎 ∈ suc suc suc 𝑛)
382 eqeq1 2734 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = 𝑎 → (𝑏 = ∅ ↔ 𝑎 = ∅))
383 unieq 4918 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 = 𝑎 𝑏 = 𝑎)
384383fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = 𝑎 → (𝑔 𝑏) = (𝑔 𝑎))
385382, 384ifbieq2d 4553 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = if(𝑎 = ∅, 𝑦, (𝑔 𝑎)))
386 fvex 6903 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔 𝑎) ∈ V
387100, 386ifex 4577 . . . . . . . . . . . . . . . . . . . . . . . 24 if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) ∈ V
388385, 297, 387fvmpt 6997 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔 𝑎)))
389381, 388syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔 𝑎)))
390389adantl 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔 𝑎)))
391 ordsucelsuc 7812 . . . . . . . . . . . . . . . . . . . . . . . . 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 475 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → suc 𝑎 ∈ suc suc suc 𝑛)
394 eqeq1 2734 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 = suc 𝑎 → (𝑏 = ∅ ↔ suc 𝑎 = ∅))
395 unieq 4918 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = suc 𝑎 𝑏 = suc 𝑎)
396395fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 = suc 𝑎 → (𝑔 𝑏) = (𝑔 suc 𝑎))
397394, 396ifbieq2d 4553 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = suc 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = if(suc 𝑎 = ∅, 𝑦, (𝑔 suc 𝑎)))
398 nsuceq0 6446 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 suc 𝑎 ≠ ∅
399398neii 2940 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ¬ suc 𝑎 = ∅
400399iffalsei 4537 . . . . . . . . . . . . . . . . . . . . . . . . 25 if(suc 𝑎 = ∅, 𝑦, (𝑔 suc 𝑎)) = (𝑔 suc 𝑎)
401397, 400eqtrdi 2786 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = suc 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = (𝑔 suc 𝑎))
402 fvex 6903 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 suc 𝑎) ∈ V
403401, 297, 402fvmpt 6997 . . . . . . . . . . . . . . . . . . . . . . 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 7865 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ ω → Ord 𝑎)
406377, 405syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → Ord 𝑎)
407 ordunisuc 7822 . . . . . . . . . . . . . . . . . . . . . . . 24 (Ord 𝑎 suc 𝑎 = 𝑎)
408406, 407syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → suc 𝑎 = 𝑎)
409408fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑔 suc 𝑎) = (𝑔𝑎))
410404, 409eqtrd 2770 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎) = (𝑔𝑎))
411380, 390, 4103brtr4d 5179 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎)(𝑅𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎))
412411ralrimiva 3144 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∀𝑎 ∈ suc suc 𝑛((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎)(𝑅𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎))
413264sucex 7796 . . . . . . . . . . . . . . . . . . . . 21 suc suc suc 𝑛 ∈ V
414413mptex 7226 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) ∈ V
415 fneq1 6639 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓 Fn suc suc suc 𝑛 ↔ (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) Fn suc suc suc 𝑛))
416 fveq1 6889 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓‘∅) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅))
417416eqeq1d 2732 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → ((𝑓‘∅) = 𝑦 ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅) = 𝑦))
418 fveq1 6889 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓‘suc suc 𝑛) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛))
419418eqeq1d 2732 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → ((𝑓‘suc suc 𝑛) = 𝑥 ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛) = 𝑥))
420417, 419anbi12d 629 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ↔ (((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅) = 𝑦 ∧ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛) = 𝑥)))
421 fveq1 6889 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓𝑎) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎))
422 fveq1 6889 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓‘suc 𝑎) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎))
423421, 422breq12d 5160 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎)(𝑅𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎)))
424423ralbidv 3175 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑛((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎)(𝑅𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎)))
425415, 420, 4243anbi123d 1434 . . . . . . . . . . . . . . . . . . . 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 3595 . . . . . . . . . . . . . . . . . . 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 1373 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
4284273exp 1117 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) → (𝑦(𝑅𝐴)𝑧 → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))))
429428exlimdv 1934 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) → (𝑦(𝑅𝐴)𝑧 → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))))
430429impd 409 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
431430exlimdv 1934 . . . . . . . . . . . . . 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 3476 . . . . . . . . . . . . . . . 16 𝑧 ∈ V
434433brresi 5989 . . . . . . . . . . . . . . 15 (𝑦(𝑅𝐴)𝑧 ↔ (𝑦𝐴𝑦𝑅𝑧))
435434anbi2i 621 . . . . . . . . . . . . . 14 ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)))
436435exbii 1848 . . . . . . . . . . . . 13 (∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)))
437432, 436bitrdi 286 . . . . . . . . . . . 12 (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
438215, 437vtoclg 3541 . . . . . . . . . . 11 (𝑋𝐴 → (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)))))
439438impcom 406 . . . . . . . . . 10 ((𝑛 ∈ ω ∧ 𝑋𝐴) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
440439adantrl 712 . . . . . . . . 9 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴)) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
4414403adant3 1130 . . . . . . . 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 311 . . . . . . 7 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
443442alrimiv 1928 . . . . . 6 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
4444433exp 1117 . . . . 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 7891 . . 3 (𝑁 ∈ ω → ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁))))
4474463impib 1114 . 2 ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁)))
44844719.21bi 2180 1 ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴𝑋𝐴) → (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wo 843  w3a 1085  wal 1537   = wceq 1539  wex 1779  wcel 2104  wral 3059  wrex 3068  Vcvv 3472  wss 3947  c0 4321  ifcif 4527  {csn 4627   cuni 4907   ciun 4996   class class class wbr 5147  cmpt 5230   Se wse 5628  cres 5677  Predcpred 6298  Ord word 6362  Oncon0 6363  suc csuc 6365   Fn wfn 6537  cfv 6542  ωcom 7857  reccrdg 8411  1oc1o 8461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468
This theorem is referenced by:  ttrclse  9724
  Copyright terms: Public domain W3C validator