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

Theorem ttrclselem2 9662
Description: Lemma for ttrclse 9663. 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 6383 . . . . . . . . . . . 12 (𝑚 = ∅ → suc 𝑚 = suc ∅)
2 df-1o 8412 . . . . . . . . . . . 12 1o = suc ∅
31, 2eqtr4di 2794 . . . . . . . . . . 11 (𝑚 = ∅ → suc 𝑚 = 1o)
4 suceq 6383 . . . . . . . . . . 11 (suc 𝑚 = 1o → suc suc 𝑚 = suc 1o)
53, 4syl 17 . . . . . . . . . 10 (𝑚 = ∅ → suc suc 𝑚 = suc 1o)
65fneq2d 6596 . . . . . . . . 9 (𝑚 = ∅ → (𝑓 Fn suc suc 𝑚𝑓 Fn suc 1o))
73fveqeq2d 6850 . . . . . . . . . 10 (𝑚 = ∅ → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘1o) = 𝑋))
87anbi2d 629 . . . . . . . . 9 (𝑚 = ∅ → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
9 df1o2 8419 . . . . . . . . . . . 12 1o = {∅}
103, 9eqtrdi 2792 . . . . . . . . . . 11 (𝑚 = ∅ → suc 𝑚 = {∅})
1110raleqdv 3313 . . . . . . . . . 10 (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ {∅} (𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
12 0ex 5264 . . . . . . . . . . 11 ∅ ∈ V
13 fveq2 6842 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑓𝑎) = (𝑓‘∅))
14 suceq 6383 . . . . . . . . . . . . . 14 (𝑎 = ∅ → suc 𝑎 = suc ∅)
1514, 2eqtr4di 2794 . . . . . . . . . . . . 13 (𝑎 = ∅ → suc 𝑎 = 1o)
1615fveq2d 6846 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘1o))
1713, 16breq12d 5118 . . . . . . . . . . 11 (𝑎 = ∅ → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)))
1812, 17ralsn 4642 . . . . . . . . . 10 (∀𝑎 ∈ {∅} (𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o))
1911, 18bitrdi 286 . . . . . . . . 9 (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)))
206, 8, 193anbi123d 1436 . . . . . . . 8 (𝑚 = ∅ → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o))))
2120exbidv 1924 . . . . . . 7 (𝑚 = ∅ → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o))))
22 fveq2 6842 . . . . . . . 8 (𝑚 = ∅ → (𝐹𝑚) = (𝐹‘∅))
2322eleq2d 2823 . . . . . . 7 (𝑚 = ∅ → (𝑦 ∈ (𝐹𝑚) ↔ 𝑦 ∈ (𝐹‘∅)))
2421, 23bibi12d 345 . . . . . 6 (𝑚 = ∅ → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅))))
2524albidv 1923 . . . . 5 (𝑚 = ∅ → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅))))
2625imbi2d 340 . . . 4 (𝑚 = ∅ → (((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚))) ↔ ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅)))))
27 suceq 6383 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → suc 𝑚 = suc 𝑛)
28 suceq 6383 . . . . . . . . . . . . 13 (suc 𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc 𝑛)
2927, 28syl 17 . . . . . . . . . . . 12 (𝑚 = 𝑛 → suc suc 𝑚 = suc suc 𝑛)
3029fneq2d 6596 . . . . . . . . . . 11 (𝑚 = 𝑛 → (𝑓 Fn suc suc 𝑚𝑓 Fn suc suc 𝑛))
3127fveqeq2d 6850 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc 𝑛) = 𝑋))
3231anbi2d 629 . . . . . . . . . . 11 (𝑚 = 𝑛 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋)))
3327raleqdv 3313 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
34 fveq2 6842 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → (𝑓𝑎) = (𝑓𝑐))
35 suceq 6383 . . . . . . . . . . . . . . 15 (𝑎 = 𝑐 → suc 𝑎 = suc 𝑐)
3635fveq2d 6846 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑐))
3734, 36breq12d 5118 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐)))
3837cbvralvw 3225 . . . . . . . . . . . 12 (∀𝑎 ∈ suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐))
3933, 38bitrdi 286 . . . . . . . . . . 11 (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐)))
4030, 32, 393anbi123d 1436 . . . . . . . . . 10 (𝑚 = 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐))))
4140exbidv 1924 . . . . . . . . 9 (𝑚 = 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐))))
42 fneq1 6593 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑓 Fn suc suc 𝑛𝑔 Fn suc suc 𝑛))
43 fveq1 6841 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓‘∅) = (𝑔‘∅))
4443eqeq1d 2738 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓‘∅) = 𝑦 ↔ (𝑔‘∅) = 𝑦))
45 fveq1 6841 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓‘suc 𝑛) = (𝑔‘suc 𝑛))
4645eqeq1d 2738 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓‘suc 𝑛) = 𝑋 ↔ (𝑔‘suc 𝑛) = 𝑋))
4744, 46anbi12d 631 . . . . . . . . . . 11 (𝑓 = 𝑔 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ↔ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋)))
48 fveq1 6841 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓𝑐) = (𝑔𝑐))
49 fveq1 6841 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓‘suc 𝑐) = (𝑔‘suc 𝑐))
5048, 49breq12d 5118 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐) ↔ (𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)))
5150ralbidv 3174 . . . . . . . . . . 11 (𝑓 = 𝑔 → (∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐) ↔ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)))
5242, 47, 513anbi123d 1436 . . . . . . . . . 10 (𝑓 = 𝑔 → ((𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓𝑐)(𝑅𝐴)(𝑓‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
5352cbvexvw 2040 . . . . . . . . 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 6842 . . . . . . . . 9 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
5655eleq2d 2823 . . . . . . . 8 (𝑚 = 𝑛 → (𝑦 ∈ (𝐹𝑚) ↔ 𝑦 ∈ (𝐹𝑛)))
5754, 56bibi12d 345 . . . . . . 7 (𝑚 = 𝑛 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹𝑛))))
5857albidv 1923 . . . . . 6 (𝑚 = 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹𝑛))))
59 eqeq2 2748 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑔‘∅) = 𝑦 ↔ (𝑔‘∅) = 𝑧))
6059anbi1d 630 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ↔ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋)))
61603anbi2d 1441 . . . . . . . . 9 (𝑦 = 𝑧 → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
6261exbidv 1924 . . . . . . . 8 (𝑦 = 𝑧 → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
63 eleq1 2825 . . . . . . . 8 (𝑦 = 𝑧 → (𝑦 ∈ (𝐹𝑛) ↔ 𝑧 ∈ (𝐹𝑛)))
6462, 63bibi12d 345 . . . . . . 7 (𝑦 = 𝑧 → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹𝑛)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))))
6564cbvalvw 2039 . . . . . 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 340 . . . 4 (𝑚 = 𝑛 → (((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚))) ↔ ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛)))))
68 suceq 6383 . . . . . . . . . . 11 (𝑚 = suc 𝑛 → suc 𝑚 = suc suc 𝑛)
69 suceq 6383 . . . . . . . . . . 11 (suc 𝑚 = suc suc 𝑛 → suc suc 𝑚 = suc suc suc 𝑛)
7068, 69syl 17 . . . . . . . . . 10 (𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc suc 𝑛)
7170fneq2d 6596 . . . . . . . . 9 (𝑚 = suc 𝑛 → (𝑓 Fn suc suc 𝑚𝑓 Fn suc suc suc 𝑛))
7268fveqeq2d 6850 . . . . . . . . . 10 (𝑚 = suc 𝑛 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc suc 𝑛) = 𝑋))
7372anbi2d 629 . . . . . . . . 9 (𝑚 = suc 𝑛 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋)))
7468raleqdv 3313 . . . . . . . . 9 (𝑚 = suc 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
7571, 73, 743anbi123d 1436 . . . . . . . 8 (𝑚 = suc 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
7675exbidv 1924 . . . . . . 7 (𝑚 = suc 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
77 fveq2 6842 . . . . . . . 8 (𝑚 = suc 𝑛 → (𝐹𝑚) = (𝐹‘suc 𝑛))
7877eleq2d 2823 . . . . . . 7 (𝑚 = suc 𝑛 → (𝑦 ∈ (𝐹𝑚) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
7976, 78bibi12d 345 . . . . . 6 (𝑚 = suc 𝑛 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛))))
8079albidv 1923 . . . . 5 (𝑚 = suc 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛))))
8180imbi2d 340 . . . 4 (𝑚 = suc 𝑛 → (((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚))) ↔ ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))))
82 suceq 6383 . . . . . . . . . . 11 (𝑚 = 𝑁 → suc 𝑚 = suc 𝑁)
83 suceq 6383 . . . . . . . . . . 11 (suc 𝑚 = suc 𝑁 → suc suc 𝑚 = suc suc 𝑁)
8482, 83syl 17 . . . . . . . . . 10 (𝑚 = 𝑁 → suc suc 𝑚 = suc suc 𝑁)
8584fneq2d 6596 . . . . . . . . 9 (𝑚 = 𝑁 → (𝑓 Fn suc suc 𝑚𝑓 Fn suc suc 𝑁))
8682fveqeq2d 6850 . . . . . . . . . 10 (𝑚 = 𝑁 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc 𝑁) = 𝑋))
8786anbi2d 629 . . . . . . . . 9 (𝑚 = 𝑁 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋)))
8882raleqdv 3313 . . . . . . . . 9 (𝑚 = 𝑁 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
8985, 87, 883anbi123d 1436 . . . . . . . 8 (𝑚 = 𝑁 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
9089exbidv 1924 . . . . . . 7 (𝑚 = 𝑁 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
91 fveq2 6842 . . . . . . . 8 (𝑚 = 𝑁 → (𝐹𝑚) = (𝐹𝑁))
9291eleq2d 2823 . . . . . . 7 (𝑚 = 𝑁 → (𝑦 ∈ (𝐹𝑚) ↔ 𝑦 ∈ (𝐹𝑁)))
9390, 92bibi12d 345 . . . . . 6 (𝑚 = 𝑁 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁))))
9493albidv 1923 . . . . 5 (𝑚 = 𝑁 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁))))
9594imbi2d 340 . . . 4 (𝑚 = 𝑁 → (((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑚))) ↔ ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁)))))
96 eqeq2 2748 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((𝑓‘1o) = 𝑥 ↔ (𝑓‘1o) = 𝑋))
9796anbi2d 629 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
9897anbi2d 629 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)) ↔ (𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋))))
9998exbidv 1924 . . . . . . . . . 10 (𝑥 = 𝑋 → (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)) ↔ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋))))
100 vex 3449 . . . . . . . . . . . . 13 𝑦 ∈ V
101 vex 3449 . . . . . . . . . . . . 13 𝑥 ∈ V
102100, 101ifex 4536 . . . . . . . . . . . 12 if(𝑏 = ∅, 𝑦, 𝑥) ∈ V
103 eqid 2736 . . . . . . . . . . . 12 (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))
104102, 103fnmpti 6644 . . . . . . . . . . 11 (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o
105 equid 2015 . . . . . . . . . . . 12 𝑦 = 𝑦
106 equid 2015 . . . . . . . . . . . 12 𝑥 = 𝑥
107105, 106pm3.2i 471 . . . . . . . . . . 11 (𝑦 = 𝑦𝑥 = 𝑥)
108 1oex 8422 . . . . . . . . . . . . . 14 1o ∈ V
109108sucex 7741 . . . . . . . . . . . . 13 suc 1o ∈ V
110109mptex 7173 . . . . . . . . . . . 12 (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) ∈ V
111 fneq1 6593 . . . . . . . . . . . . 13 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓 Fn suc 1o ↔ (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o))
112 fveq1 6841 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘∅) = ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅))
113 1on 8424 . . . . . . . . . . . . . . . . . 18 1o ∈ On
114113onordi 6428 . . . . . . . . . . . . . . . . 17 Ord 1o
115 0elsuc 7770 . . . . . . . . . . . . . . . . 17 (Ord 1o → ∅ ∈ suc 1o)
116 iftrue 4492 . . . . . . . . . . . . . . . . . 18 (𝑏 = ∅ → if(𝑏 = ∅, 𝑦, 𝑥) = 𝑦)
117116, 103, 100fvmpt 6948 . . . . . . . . . . . . . . . . 17 (∅ ∈ suc 1o → ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅) = 𝑦)
118114, 115, 117mp2b 10 . . . . . . . . . . . . . . . 16 ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅) = 𝑦
119112, 118eqtrdi 2792 . . . . . . . . . . . . . . 15 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘∅) = 𝑦)
120119eqeq1d 2738 . . . . . . . . . . . . . 14 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓‘∅) = 𝑦𝑦 = 𝑦))
121 fveq1 6841 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘1o) = ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1o))
122108sucid 6399 . . . . . . . . . . . . . . . . 17 1o ∈ suc 1o
123 eqeq1 2740 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 1o → (𝑏 = ∅ ↔ 1o = ∅))
124123ifbid 4509 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1o → if(𝑏 = ∅, 𝑦, 𝑥) = if(1o = ∅, 𝑦, 𝑥))
125 1n0 8434 . . . . . . . . . . . . . . . . . . . . 21 1o ≠ ∅
126125neii 2945 . . . . . . . . . . . . . . . . . . . 20 ¬ 1o = ∅
127126iffalsei 4496 . . . . . . . . . . . . . . . . . . 19 if(1o = ∅, 𝑦, 𝑥) = 𝑥
128124, 127eqtrdi 2792 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1o → if(𝑏 = ∅, 𝑦, 𝑥) = 𝑥)
129128, 103, 101fvmpt 6948 . . . . . . . . . . . . . . . . 17 (1o ∈ suc 1o → ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1o) = 𝑥)
130122, 129ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1o) = 𝑥
131121, 130eqtrdi 2792 . . . . . . . . . . . . . . 15 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘1o) = 𝑥)
132131eqeq1d 2738 . . . . . . . . . . . . . 14 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓‘1o) = 𝑥𝑥 = 𝑥))
133120, 132anbi12d 631 . . . . . . . . . . . . 13 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥) ↔ (𝑦 = 𝑦𝑥 = 𝑥)))
134111, 133anbi12d 631 . . . . . . . . . . . 12 (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)) ↔ ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o ∧ (𝑦 = 𝑦𝑥 = 𝑥))))
135110, 134spcev 3565 . . . . . . . . . . 11 (((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o ∧ (𝑦 = 𝑦𝑥 = 𝑥)) → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)))
136104, 107, 135mp2an 690 . . . . . . . . . 10 𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥))
13799, 136vtoclg 3525 . . . . . . . . 9 (𝑋𝐴 → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
138137adantl 482 . . . . . . . 8 ((𝑅 Se 𝐴𝑋𝐴) → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
139138biantrurd 533 . . . . . . 7 ((𝑅 Se 𝐴𝑋𝐴) → ((𝑦𝐴𝑦𝑅𝑋) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑦𝐴𝑦𝑅𝑋))))
140100elpred 6270 . . . . . . . 8 (𝑋𝐴 → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑦𝐴𝑦𝑅𝑋)))
141140adantl 482 . . . . . . 7 ((𝑅 Se 𝐴𝑋𝐴) → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑦𝐴𝑦𝑅𝑋)))
142 brres 5944 . . . . . . . . 9 (𝑋𝐴 → (𝑦(𝑅𝐴)𝑋 ↔ (𝑦𝐴𝑦𝑅𝑋)))
143142adantl 482 . . . . . . . 8 ((𝑅 Se 𝐴𝑋𝐴) → (𝑦(𝑅𝐴)𝑋 ↔ (𝑦𝐴𝑦𝑅𝑋)))
144143anbi2d 629 . . . . . . 7 ((𝑅 Se 𝐴𝑋𝐴) → ((∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑦𝐴𝑦𝑅𝑋))))
145139, 141, 1443bitr4rd 311 . . . . . 6 ((𝑅 Se 𝐴𝑋𝐴) → ((∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋) ↔ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑋)))
146 df-3an 1089 . . . . . . . . . 10 ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)))
147 breq12 5110 . . . . . . . . . . . 12 (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) → ((𝑓‘∅)(𝑅𝐴)(𝑓‘1o) ↔ 𝑦(𝑅𝐴)𝑋))
148147adantl 482 . . . . . . . . . . 11 ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) → ((𝑓‘∅)(𝑅𝐴)(𝑓‘1o) ↔ 𝑦(𝑅𝐴)𝑋))
149148pm5.32i 575 . . . . . . . . . 10 (((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋))
150146, 149bitri 274 . . . . . . . . 9 ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋))
151150exbii 1850 . . . . . . . 8 (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ ∃𝑓((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅𝐴)𝑋))
152 19.41v 1953 . . . . . . . 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 6843 . . . . . . . 8 (𝐹‘∅) = (rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅)
157 setlikespec 6279 . . . . . . . . . 10 ((𝑋𝐴𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
158157ancoms 459 . . . . . . . . 9 ((𝑅 Se 𝐴𝑋𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
159 rdg0g 8373 . . . . . . . . 9 (Pred(𝑅, 𝐴, 𝑋) ∈ V → (rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅) = Pred(𝑅, 𝐴, 𝑋))
160158, 159syl 17 . . . . . . . 8 ((𝑅 Se 𝐴𝑋𝐴) → (rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅) = Pred(𝑅, 𝐴, 𝑋))
161156, 160eqtrid 2788 . . . . . . 7 ((𝑅 Se 𝐴𝑋𝐴) → (𝐹‘∅) = Pred(𝑅, 𝐴, 𝑋))
162161eleq2d 2823 . . . . . 6 ((𝑅 Se 𝐴𝑋𝐴) → (𝑦 ∈ (𝐹‘∅) ↔ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑋)))
163145, 154, 1623bitr4d 310 . . . . 5 ((𝑅 Se 𝐴𝑋𝐴) → (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅)))
164163alrimiv 1930 . . . 4 ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅)))
165 eliun 4958 . . . . . . . . . 10 (𝑦 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧 ∈ (𝐹𝑛)𝑦 ∈ Pred(𝑅, 𝐴, 𝑧))
166 df-rex 3074 . . . . . . . . . 10 (∃𝑧 ∈ (𝐹𝑛)𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)))
167165, 166bitri 274 . . . . . . . . 9 (𝑦 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)))
168100elpred 6270 . . . . . . . . . . . . . 14 (𝑧 ∈ V → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ (𝑦𝐴𝑦𝑅𝑧)))
169168elv 3451 . . . . . . . . . . . . 13 (𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ (𝑦𝐴𝑦𝑅𝑧))
170169anbi2i 623 . . . . . . . . . . . 12 ((𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ (𝑧 ∈ (𝐹𝑛) ∧ (𝑦𝐴𝑦𝑅𝑧)))
171 anbi1 632 . . . . . . . . . . . 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 1835 . . . . . . . . . 10 (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛)) → (∃𝑧(𝑧 ∈ (𝐹𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
1741733ad2ant3 1135 . . . . . . . . 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 7808 . . . . . . . . . . 11 (𝑛 ∈ ω → 𝑛 ∈ On)
177 fvex 6855 . . . . . . . . . . . 12 (𝐹𝑛) ∈ V
178155ttrclselem1 9661 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (𝐹𝑛) ⊆ 𝐴)
179178adantr 481 . . . . . . . . . . . . . 14 ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → (𝐹𝑛) ⊆ 𝐴)
180 dfse3 6290 . . . . . . . . . . . . . . . 16 (𝑅 Se 𝐴 ↔ ∀𝑧𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
181180biimpi 215 . . . . . . . . . . . . . . 15 (𝑅 Se 𝐴 → ∀𝑧𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
182181adantl 482 . . . . . . . . . . . . . 14 ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → ∀𝑧𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
183 ssralv 4010 . . . . . . . . . . . . . 14 ((𝐹𝑛) ⊆ 𝐴 → (∀𝑧𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V → ∀𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V))
184179, 182, 183sylc 65 . . . . . . . . . . . . 13 ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → ∀𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
185184adantrr 715 . . . . . . . . . . . 12 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴)) → ∀𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
186 iunexg 7896 . . . . . . . . . . . 12 (((𝐹𝑛) ∈ V ∧ ∀𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V) → 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
187177, 185, 186sylancr 587 . . . . . . . . . . 11 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴)) → 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
188 nfcv 2907 . . . . . . . . . . . 12 𝑏Pred(𝑅, 𝐴, 𝑋)
189 nfcv 2907 . . . . . . . . . . . 12 𝑏𝑛
190 nfmpt1 5213 . . . . . . . . . . . . . . . 16 𝑏(𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤))
191190, 188nfrdg 8360 . . . . . . . . . . . . . . 15 𝑏rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))
192155, 191nfcxfr 2905 . . . . . . . . . . . . . 14 𝑏𝐹
193192, 189nffv 6852 . . . . . . . . . . . . 13 𝑏(𝐹𝑛)
194 nfcv 2907 . . . . . . . . . . . . 13 𝑏Pred(𝑅, 𝐴, 𝑧)
195193, 194nfiun 4984 . . . . . . . . . . . 12 𝑏 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧)
196 predeq3 6257 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
197196cbviunv 5000 . . . . . . . . . . . . 13 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤) = 𝑧𝑏 Pred(𝑅, 𝐴, 𝑧)
198 iuneq1 4970 . . . . . . . . . . . . 13 (𝑏 = (𝐹𝑛) → 𝑧𝑏 Pred(𝑅, 𝐴, 𝑧) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
199197, 198eqtrid 2788 . . . . . . . . . . . 12 (𝑏 = (𝐹𝑛) → 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
200188, 189, 195, 155, 199rdgsucmptf 8374 . . . . . . . . . . 11 ((𝑛 ∈ On ∧ 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V) → (𝐹‘suc 𝑛) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
201176, 187, 200syl2an2r 683 . . . . . . . . . 10 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴)) → (𝐹‘suc 𝑛) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
2022013adant3 1132 . . . . . . . . 9 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → (𝐹‘suc 𝑛) = 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧))
203202eleq2d 2823 . . . . . . . 8 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → (𝑦 ∈ (𝐹‘suc 𝑛) ↔ 𝑦 𝑧 ∈ (𝐹𝑛)Pred(𝑅, 𝐴, 𝑧)))
204 eqeq2 2748 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → ((𝑓‘suc suc 𝑛) = 𝑥 ↔ (𝑓‘suc suc 𝑛) = 𝑋))
205204anbi2d 629 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋)))
2062053anbi2d 1441 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
207206exbidv 1924 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
208 eqeq2 2748 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → ((𝑔‘suc 𝑛) = 𝑥 ↔ (𝑔‘suc 𝑛) = 𝑋))
209208anbi2d 629 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → (((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋)))
2102093anbi2d 1441 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
211210exbidv 1924 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
212211anbi1d 630 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
213212exbidv 1924 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
214207, 213bibi12d 345 . . . . . . . . . . . . 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 340 . . . . . . . . . . . 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 6855 . . . . . . . . . . . . . . . . . . . 20 (𝑓‘suc 𝑏) ∈ V
217 eqid 2736 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))
218216, 217fnmpti 6644 . . . . . . . . . . . . . . . . . . 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 7827 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
221220adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → suc 𝑛 ∈ ω)
222 nnord 7810 . . . . . . . . . . . . . . . . . . . . 21 (suc 𝑛 ∈ ω → Ord suc 𝑛)
223221, 222syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → Ord suc 𝑛)
224 0elsuc 7770 . . . . . . . . . . . . . . . . . . . 20 (Ord suc 𝑛 → ∅ ∈ suc suc 𝑛)
225223, 224syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∅ ∈ suc suc 𝑛)
226 suceq 6383 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = ∅ → suc 𝑏 = suc ∅)
227226fveq2d 6846 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = ∅ → (𝑓‘suc 𝑏) = (𝑓‘suc ∅))
228 fvex 6855 . . . . . . . . . . . . . . . . . . . 20 (𝑓‘suc ∅) ∈ V
229227, 217, 228fvmpt 6948 . . . . . . . . . . . . . . . . . . 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 3449 . . . . . . . . . . . . . . . . . . . . . 22 𝑛 ∈ V
232231sucex 7741 . . . . . . . . . . . . . . . . . . . . 21 suc 𝑛 ∈ V
233232sucid 6399 . . . . . . . . . . . . . . . . . . . 20 suc 𝑛 ∈ suc suc 𝑛
234 suceq 6383 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = suc 𝑛 → suc 𝑏 = suc suc 𝑛)
235234fveq2d 6846 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = suc 𝑛 → (𝑓‘suc 𝑏) = (𝑓‘suc suc 𝑛))
236 fvex 6855 . . . . . . . . . . . . . . . . . . . . 21 (𝑓‘suc suc 𝑛) ∈ V
237235, 217, 236fvmpt 6948 . . . . . . . . . . . . . . . . . . . 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 1233 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → (𝑓‘suc suc 𝑛) = 𝑥)
240238, 239eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥)
241 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = suc 𝑐 → (𝑓𝑎) = (𝑓‘suc 𝑐))
242 suceq 6383 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = suc 𝑐 → suc 𝑎 = suc suc 𝑐)
243242fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = suc 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc suc 𝑐))
244241, 243breq12d 5118 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = suc 𝑐 → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘suc 𝑐)(𝑅𝐴)(𝑓‘suc suc 𝑐)))
245 simplr3 1217 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))
246 ordsucelsuc 7757 . . . . . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → suc 𝑐 ∈ suc suc 𝑛)
249244, 245, 248rspcdva 3582 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → (𝑓‘suc 𝑐)(𝑅𝐴)(𝑓‘suc suc 𝑐))
250 elelsuc 6390 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ suc 𝑛𝑐 ∈ suc suc 𝑛)
251 suceq 6383 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = 𝑐 → suc 𝑏 = suc 𝑐)
252251fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = 𝑐 → (𝑓‘suc 𝑏) = (𝑓‘suc 𝑐))
253 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓‘suc 𝑐) ∈ V
254252, 217, 253fvmpt 6948 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
255250, 254syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 ∈ suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
256255adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
257 suceq 6383 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = suc 𝑐 → suc 𝑏 = suc suc 𝑐)
258257fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = suc 𝑐 → (𝑓‘suc 𝑏) = (𝑓‘suc suc 𝑐))
259 fvex 6855 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓‘suc suc 𝑐) ∈ V
260258, 217, 259fvmpt 6948 . . . . . . . . . . . . . . . . . . . . 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 5137 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
263262ralrimiva 3143 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∀𝑐 ∈ suc 𝑛((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
264232sucex 7741 . . . . . . . . . . . . . . . . . . . 20 suc suc 𝑛 ∈ V
265264mptex 7173 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) ∈ V
266 fneq1 6593 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔 Fn suc suc 𝑛 ↔ (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) Fn suc suc 𝑛))
267 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘∅) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅))
268267eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔‘∅) = (𝑓‘suc ∅) ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅)))
269 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘suc 𝑛) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛))
270269eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔‘suc 𝑛) = 𝑥 ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥))
271268, 270anbi12d 631 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ (((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅) ∧ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥)))
272 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔𝑐) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐))
273 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘suc 𝑐) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
274272, 273breq12d 5118 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐) ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐)))
275274ralbidv 3174 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐) ↔ ∀𝑐 ∈ suc 𝑛((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐)))
276266, 271, 2753anbi123d 1436 . . . . . . . . . . . . . . . . . . 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 3565 . . . . . . . . . . . . . . . . . 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 1375 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)))
279 simpr2l 1232 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → (𝑓‘∅) = 𝑦)
28014fveq2d 6846 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘suc ∅))
28113, 280breq12d 5118 . . . . . . . . . . . . . . . . . . 19 (𝑎 = ∅ → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅𝐴)(𝑓‘suc ∅)))
282 simpr3 1196 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))
283281, 282, 225rspcdva 3582 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → (𝑓‘∅)(𝑅𝐴)(𝑓‘suc ∅))
284279, 283eqbrtrrd 5129 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → 𝑦(𝑅𝐴)(𝑓‘suc ∅))
285 eqeq2 2748 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (𝑓‘suc ∅) → ((𝑔‘∅) = 𝑧 ↔ (𝑔‘∅) = (𝑓‘suc ∅)))
286285anbi1d 630 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = (𝑓‘suc ∅) → (((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥)))
2872863anbi2d 1441 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑓‘suc ∅) → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
288287exbidv 1924 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑓‘suc ∅) → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))))
289 breq2 5109 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑓‘suc ∅) → (𝑦(𝑅𝐴)𝑧𝑦(𝑅𝐴)(𝑓‘suc ∅)))
290288, 289anbi12d 631 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑓‘suc ∅) → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)(𝑓‘suc ∅))))
291228, 290spcev 3565 . . . . . . . . . . . . . . . . 17 ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)(𝑓‘suc ∅)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧))
292278, 284, 291syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧))
293292ex 413 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → ((𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧)))
294293exlimdv 1936 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧)))
295 fvex 6855 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 𝑏) ∈ V
296100, 295ifex 4536 . . . . . . . . . . . . . . . . . . . . 21 if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) ∈ V
297 eqid 2736 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))
298296, 297fnmpti 6644 . . . . . . . . . . . . . . . . . . . 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 7827 . . . . . . . . . . . . . . . . . . . . . . . 24 (suc 𝑛 ∈ ω → suc suc 𝑛 ∈ ω)
301220, 300syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ω → suc suc 𝑛 ∈ ω)
3023013ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → suc suc 𝑛 ∈ ω)
303 nnord 7810 . . . . . . . . . . . . . . . . . . . . . 22 (suc suc 𝑛 ∈ ω → Ord suc suc 𝑛)
304302, 303syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → Ord suc suc 𝑛)
305 0elsuc 7770 . . . . . . . . . . . . . . . . . . . . 21 (Ord suc suc 𝑛 → ∅ ∈ suc suc suc 𝑛)
306304, 305syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∅ ∈ suc suc suc 𝑛)
307 iftrue 4492 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = ∅ → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = 𝑦)
308307, 297, 100fvmpt 6948 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅) = 𝑦)
309306, 308syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅) = 𝑦)
310264sucid 6399 . . . . . . . . . . . . . . . . . . . . 21 suc suc 𝑛 ∈ suc suc suc 𝑛
311 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = suc suc 𝑛 → (𝑏 = ∅ ↔ suc suc 𝑛 = ∅))
312 unieq 4876 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = suc suc 𝑛 𝑏 = suc suc 𝑛)
313312fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = suc suc 𝑛 → (𝑔 𝑏) = (𝑔 suc suc 𝑛))
314311, 313ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = suc suc 𝑛 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = if(suc suc 𝑛 = ∅, 𝑦, (𝑔 suc suc 𝑛)))
315 nsuceq0 6400 . . . . . . . . . . . . . . . . . . . . . . . . 25 suc suc 𝑛 ≠ ∅
316315neii 2945 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ suc suc 𝑛 = ∅
317316iffalsei 4496 . . . . . . . . . . . . . . . . . . . . . . 23 if(suc suc 𝑛 = ∅, 𝑦, (𝑔 suc suc 𝑛)) = (𝑔 suc suc 𝑛)
318314, 317eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = suc suc 𝑛 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = (𝑔 suc suc 𝑛))
319 fvex 6855 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 suc suc 𝑛) ∈ V
320318, 297, 319fvmpt 6948 . . . . . . . . . . . . . . . . . . . . 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 1133 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → suc 𝑛 ∈ ω)
323322, 222syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → Ord suc 𝑛)
324 ordunisuc 7767 . . . . . . . . . . . . . . . . . . . . . 22 (Ord suc 𝑛 suc suc 𝑛 = suc 𝑛)
325323, 324syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → suc suc 𝑛 = suc 𝑛)
326325fveq2d 6846 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑔 suc suc 𝑛) = (𝑔‘suc 𝑛))
327 simp22r 1293 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑔‘suc 𝑛) = 𝑥)
328321, 326, 3273eqtrd 2780 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛) = 𝑥)
329 simpl3 1193 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 = ∅) → 𝑦(𝑅𝐴)𝑧)
330 iftrue 4492 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) = 𝑦)
331330adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 = ∅) → if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) = 𝑦)
332 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = ∅ → (𝑔𝑎) = (𝑔‘∅))
333 simp22l 1292 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑔‘∅) = 𝑧)
334332, 333sylan9eqr 2798 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 = ∅) → (𝑔𝑎) = 𝑧)
335329, 331, 3343brtr4d 5137 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 = ∅) → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎))
336335ex 413 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎)))
337336adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎)))
338 ordsucelsuc 7757 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Ord suc 𝑛 → (𝑏 ∈ suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
339323, 338syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → (𝑏 ∈ suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
340 elnn 7813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑏 ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → 𝑏 ∈ ω)
341322, 340sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑏 ∈ suc 𝑛 ∧ (𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧)) → 𝑏 ∈ ω)
342341ancoms 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → 𝑏 ∈ ω)
343 nnord 7810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑏 ∈ ω → Ord 𝑏)
344342, 343syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → Ord 𝑏)
345 ordunisuc 7767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Ord 𝑏 suc 𝑏 = 𝑏)
346344, 345syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → suc 𝑏 = 𝑏)
347346fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔 suc 𝑏) = (𝑔𝑏))
348 simp23 1208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐))
349 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = 𝑏 → (𝑔𝑐) = (𝑔𝑏))
350 suceq 6383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑏 → suc 𝑐 = suc 𝑏)
351350fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = 𝑏 → (𝑔‘suc 𝑐) = (𝑔‘suc 𝑏))
352349, 351breq12d 5118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑏 → ((𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐) ↔ (𝑔𝑏)(𝑅𝐴)(𝑔‘suc 𝑏)))
353352rspcv 3577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 ∈ suc 𝑛 → (∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐) → (𝑔𝑏)(𝑅𝐴)(𝑔‘suc 𝑏)))
354348, 353mpan9 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔𝑏)(𝑅𝐴)(𝑔‘suc 𝑏))
355347, 354eqbrtrd 5127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏))
356355ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 407 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛) → (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏))
359 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = suc 𝑏 → (𝑎 ∈ suc suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
360359anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = suc 𝑏 → (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) ↔ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛)))
361 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = suc 𝑏 → (𝑎 = ∅ ↔ suc 𝑏 = ∅))
362 unieq 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = suc 𝑏 𝑎 = suc 𝑏)
363362fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = suc 𝑏 → (𝑔 𝑎) = (𝑔 suc 𝑏))
364361, 363ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) = if(suc 𝑏 = ∅, 𝑦, (𝑔 suc 𝑏)))
365 nsuceq0 6400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 suc 𝑏 ≠ ∅
366365neii 2945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ¬ suc 𝑏 = ∅
367366iffalsei 4496 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 if(suc 𝑏 = ∅, 𝑦, (𝑔 suc 𝑏)) = (𝑔 suc 𝑏)
368364, 367eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) = (𝑔 suc 𝑏))
369 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = suc 𝑏 → (𝑔𝑎) = (𝑔‘suc 𝑏))
370368, 369breq12d 5118 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = suc 𝑏 → (if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎) ↔ (𝑔 suc 𝑏)(𝑅𝐴)(𝑔‘suc 𝑏)))
371360, 370imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . 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 3157 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (∃𝑏 ∈ ω 𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎)))
375 elnn 7813 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ suc suc 𝑛 ∧ suc suc 𝑛 ∈ ω) → 𝑎 ∈ ω)
376375ancoms 459 . . . . . . . . . . . . . . . . . . . . . . . 24 ((suc suc 𝑛 ∈ ω ∧ 𝑎 ∈ suc suc 𝑛) → 𝑎 ∈ ω)
377302, 376sylan 580 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → 𝑎 ∈ ω)
378 nn0suc 7832 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ ω → (𝑎 = ∅ ∨ ∃𝑏 ∈ ω 𝑎 = suc 𝑏))
379377, 378syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑎 = ∅ ∨ ∃𝑏 ∈ ω 𝑎 = suc 𝑏))
380337, 374, 379mpjaod 858 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → if(𝑎 = ∅, 𝑦, (𝑔 𝑎))(𝑅𝐴)(𝑔𝑎))
381 elelsuc 6390 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ suc suc 𝑛𝑎 ∈ suc suc suc 𝑛)
382 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = 𝑎 → (𝑏 = ∅ ↔ 𝑎 = ∅))
383 unieq 4876 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 = 𝑎 𝑏 = 𝑎)
384383fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = 𝑎 → (𝑔 𝑏) = (𝑔 𝑎))
385382, 384ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = if(𝑎 = ∅, 𝑦, (𝑔 𝑎)))
386 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔 𝑎) ∈ V
387100, 386ifex 4536 . . . . . . . . . . . . . . . . . . . . . . . 24 if(𝑎 = ∅, 𝑦, (𝑔 𝑎)) ∈ V
388385, 297, 387fvmpt 6948 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔 𝑎)))
389381, 388syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔 𝑎)))
390389adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔 𝑎)))
391 ordsucelsuc 7757 . . . . . . . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → suc 𝑎 ∈ suc suc suc 𝑛)
394 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 = suc 𝑎 → (𝑏 = ∅ ↔ suc 𝑎 = ∅))
395 unieq 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = suc 𝑎 𝑏 = suc 𝑎)
396395fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 = suc 𝑎 → (𝑔 𝑏) = (𝑔 suc 𝑎))
397394, 396ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = suc 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = if(suc 𝑎 = ∅, 𝑦, (𝑔 suc 𝑎)))
398 nsuceq0 6400 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 suc 𝑎 ≠ ∅
399398neii 2945 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ¬ suc 𝑎 = ∅
400399iffalsei 4496 . . . . . . . . . . . . . . . . . . . . . . . . 25 if(suc 𝑎 = ∅, 𝑦, (𝑔 suc 𝑎)) = (𝑔 suc 𝑎)
401397, 400eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = suc 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔 𝑏)) = (𝑔 suc 𝑎))
402 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 suc 𝑎) ∈ V
403401, 297, 402fvmpt 6948 . . . . . . . . . . . . . . . . . . . . . . 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 7810 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ ω → Ord 𝑎)
406377, 405syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → Ord 𝑎)
407 ordunisuc 7767 . . . . . . . . . . . . . . . . . . . . . . . 24 (Ord 𝑎 suc 𝑎 = 𝑎)
408406, 407syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → suc 𝑎 = 𝑎)
409408fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑔 suc 𝑎) = (𝑔𝑎))
410404, 409eqtrd 2776 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎) = (𝑔𝑎))
411380, 390, 4103brtr4d 5137 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎)(𝑅𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎))
412411ralrimiva 3143 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∀𝑎 ∈ suc suc 𝑛((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎)(𝑅𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎))
413264sucex 7741 . . . . . . . . . . . . . . . . . . . . 21 suc suc suc 𝑛 ∈ V
414413mptex 7173 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) ∈ V
415 fneq1 6593 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓 Fn suc suc suc 𝑛 ↔ (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) Fn suc suc suc 𝑛))
416 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓‘∅) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅))
417416eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → ((𝑓‘∅) = 𝑦 ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅) = 𝑦))
418 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓‘suc suc 𝑛) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛))
419418eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → ((𝑓‘suc suc 𝑛) = 𝑥 ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛) = 𝑥))
420417, 419anbi12d 631 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ↔ (((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘∅) = 𝑦 ∧ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc suc 𝑛) = 𝑥)))
421 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓𝑎) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎))
422 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (𝑓‘suc 𝑎) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎))
423421, 422breq12d 5118 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → ((𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎)(𝑅𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎)))
424423ralbidv 3174 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏))) → (∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑛((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘𝑎)(𝑅𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔 𝑏)))‘suc 𝑎)))
425415, 420, 4243anbi123d 1436 . . . . . . . . . . . . . . . . . . . 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 3565 . . . . . . . . . . . . . . . . . . 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 1375 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))
4284273exp 1119 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) → (𝑦(𝑅𝐴)𝑧 → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))))
429428exlimdv 1936 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) → (𝑦(𝑅𝐴)𝑧 → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)))))
430429impd 411 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎))))
431430exlimdv 1936 . . . . . . . . . . . . . 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 3449 . . . . . . . . . . . . . . . 16 𝑧 ∈ V
434433brresi 5946 . . . . . . . . . . . . . . 15 (𝑦(𝑅𝐴)𝑧 ↔ (𝑦𝐴𝑦𝑅𝑧))
435434anbi2i 623 . . . . . . . . . . . . . 14 ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅𝐴)𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)))
436435exbii 1850 . . . . . . . . . . . . 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 3525 . . . . . . . . . . 11 (𝑋𝐴 → (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧)))))
439438impcom 408 . . . . . . . . . 10 ((𝑛 ∈ ω ∧ 𝑋𝐴) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
440439adantrl 714 . . . . . . . . 9 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴)) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦𝐴𝑦𝑅𝑧))))
4414403adant3 1132 . . . . . . . 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 1930 . . . . . 6 ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴𝑋𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔𝑐)(𝑅𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹𝑛))) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
4444433exp 1119 . . . . 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 7835 . . 3 (𝑁 ∈ ω → ((𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁))))
4474463impib 1116 . 2 ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴𝑋𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁)))
44844719.21bi 2182 1 ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴𝑋𝐴) → (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  w3a 1087  wal 1539   = wceq 1541  wex 1781  wcel 2106  wral 3064  wrex 3073  Vcvv 3445  wss 3910  c0 4282  ifcif 4486  {csn 4586   cuni 4865   ciun 4954   class class class wbr 5105  cmpt 5188   Se wse 5586  cres 5635  Predcpred 6252  Ord word 6316  Oncon0 6317  suc csuc 6319   Fn wfn 6491  cfv 6496  ωcom 7802  reccrdg 8355  1oc1o 8405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412
This theorem is referenced by:  ttrclse  9663
  Copyright terms: Public domain W3C validator