Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ttrclss Structured version   Visualization version   GIF version

Theorem ttrclss 33542
Description: If 𝑅 is a subclass of 𝑆 and 𝑆 is transitive, then the transitive closure of 𝑅 is a subclass of 𝑆. (Contributed by Scott Fenton, 20-Oct-2024.)
Assertion
Ref Expression
ttrclss ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → t++𝑅𝑆)

Proof of Theorem ttrclss
Dummy variables 𝑥 𝑦 𝑧 𝑓 𝑔 𝑛 𝑚 𝑎 𝑏 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 suceq 6296 . . . . . . . . . . . . . . 15 (𝑚 = ∅ → suc 𝑚 = suc ∅)
2 suceq 6296 . . . . . . . . . . . . . . 15 (suc 𝑚 = suc ∅ → suc suc 𝑚 = suc suc ∅)
31, 2syl 17 . . . . . . . . . . . . . 14 (𝑚 = ∅ → suc suc 𝑚 = suc suc ∅)
43fneq2d 6491 . . . . . . . . . . . . 13 (𝑚 = ∅ → (𝑓 Fn suc suc 𝑚𝑓 Fn suc suc ∅))
5 df-1o 8223 . . . . . . . . . . . . . . . 16 1o = suc ∅
61, 5eqtr4di 2797 . . . . . . . . . . . . . . 15 (𝑚 = ∅ → suc 𝑚 = 1o)
76fveqeq2d 6744 . . . . . . . . . . . . . 14 (𝑚 = ∅ → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘1o) = 𝑦))
87anbi2d 632 . . . . . . . . . . . . 13 (𝑚 = ∅ → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦)))
9 df1o2 8235 . . . . . . . . . . . . . . . 16 1o = {∅}
106, 9eqtrdi 2795 . . . . . . . . . . . . . . 15 (𝑚 = ∅ → suc 𝑚 = {∅})
1110raleqdv 3338 . . . . . . . . . . . . . 14 (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ {∅} (𝑓𝑎)𝑅(𝑓‘suc 𝑎)))
12 0ex 5215 . . . . . . . . . . . . . . 15 ∅ ∈ V
13 fveq2 6736 . . . . . . . . . . . . . . . 16 (𝑎 = ∅ → (𝑓𝑎) = (𝑓‘∅))
14 suceq 6296 . . . . . . . . . . . . . . . . . 18 (𝑎 = ∅ → suc 𝑎 = suc ∅)
1514, 5eqtr4di 2797 . . . . . . . . . . . . . . . . 17 (𝑎 = ∅ → suc 𝑎 = 1o)
1615fveq2d 6740 . . . . . . . . . . . . . . . 16 (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘1o))
1713, 16breq12d 5081 . . . . . . . . . . . . . . 15 (𝑎 = ∅ → ((𝑓𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1o)))
1812, 17ralsn 4612 . . . . . . . . . . . . . 14 (∀𝑎 ∈ {∅} (𝑓𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1o))
1911, 18bitrdi 290 . . . . . . . . . . . . 13 (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1o)))
204, 8, 193anbi123d 1438 . . . . . . . . . . . 12 (𝑚 = ∅ → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o))))
2120exbidv 1929 . . . . . . . . . . 11 (𝑚 = ∅ → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o))))
2221imbi1d 345 . . . . . . . . . 10 (𝑚 = ∅ → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)) → 𝑥𝑆𝑦)))
2322albidv 1928 . . . . . . . . 9 (𝑚 = ∅ → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)) → 𝑥𝑆𝑦)))
2423imbi2d 344 . . . . . . . 8 (𝑚 = ∅ → (((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)) → 𝑥𝑆𝑦))))
25 suceq 6296 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
26 suceq 6296 . . . . . . . . . . . . . . . . 17 (suc 𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc 𝑖)
2725, 26syl 17 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑖 → suc suc 𝑚 = suc suc 𝑖)
2827fneq2d 6491 . . . . . . . . . . . . . . 15 (𝑚 = 𝑖 → (𝑓 Fn suc suc 𝑚𝑓 Fn suc suc 𝑖))
2925fveqeq2d 6744 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑖 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc 𝑖) = 𝑦))
3029anbi2d 632 . . . . . . . . . . . . . . 15 (𝑚 = 𝑖 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦)))
3125raleqdv 3338 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎)))
32 fveq2 6736 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑏 → (𝑓𝑎) = (𝑓𝑏))
33 suceq 6296 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑏 → suc 𝑎 = suc 𝑏)
3433fveq2d 6740 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑏 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑏))
3532, 34breq12d 5081 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑏 → ((𝑓𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓𝑏)𝑅(𝑓‘suc 𝑏)))
3635cbvralvw 3371 . . . . . . . . . . . . . . . 16 (∀𝑎 ∈ suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑏 ∈ suc 𝑖(𝑓𝑏)𝑅(𝑓‘suc 𝑏))
3731, 36bitrdi 290 . . . . . . . . . . . . . . 15 (𝑚 = 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑏 ∈ suc 𝑖(𝑓𝑏)𝑅(𝑓‘suc 𝑏)))
3828, 30, 373anbi123d 1438 . . . . . . . . . . . . . 14 (𝑚 = 𝑖 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓𝑏)𝑅(𝑓‘suc 𝑏))))
3938exbidv 1929 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓𝑏)𝑅(𝑓‘suc 𝑏))))
40 fneq1 6488 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑓 Fn suc suc 𝑖𝑔 Fn suc suc 𝑖))
41 fveq1 6735 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → (𝑓‘∅) = (𝑔‘∅))
4241eqeq1d 2740 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → ((𝑓‘∅) = 𝑥 ↔ (𝑔‘∅) = 𝑥))
43 fveq1 6735 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → (𝑓‘suc 𝑖) = (𝑔‘suc 𝑖))
4443eqeq1d 2740 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → ((𝑓‘suc 𝑖) = 𝑦 ↔ (𝑔‘suc 𝑖) = 𝑦))
4542, 44anbi12d 634 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦)))
46 fveq1 6735 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → (𝑓𝑏) = (𝑔𝑏))
47 fveq1 6735 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → (𝑓‘suc 𝑏) = (𝑔‘suc 𝑏))
4846, 47breq12d 5081 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → ((𝑓𝑏)𝑅(𝑓‘suc 𝑏) ↔ (𝑔𝑏)𝑅(𝑔‘suc 𝑏)))
4948ralbidv 3119 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (∀𝑏 ∈ suc 𝑖(𝑓𝑏)𝑅(𝑓‘suc 𝑏) ↔ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)))
5040, 45, 493anbi123d 1438 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → ((𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓𝑏)𝑅(𝑓‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
5150cbvexvw 2045 . . . . . . . . . . . . 13 (∃𝑓(𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓𝑏)𝑅(𝑓‘suc 𝑏)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)))
5239, 51bitrdi 290 . . . . . . . . . . . 12 (𝑚 = 𝑖 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
5352imbi1d 345 . . . . . . . . . . 11 (𝑚 = 𝑖 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦)))
5453albidv 1928 . . . . . . . . . 10 (𝑚 = 𝑖 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦)))
55 eqeq2 2750 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → ((𝑔‘suc 𝑖) = 𝑦 ↔ (𝑔‘suc 𝑖) = 𝑧))
5655anbi2d 632 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧)))
57563anbi2d 1443 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → ((𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
5857exbidv 1929 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
59 breq2 5072 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑥𝑆𝑦𝑥𝑆𝑧))
6058, 59imbi12d 348 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦) ↔ (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)))
6160cbvalvw 2044 . . . . . . . . . 10 (∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧))
6254, 61bitrdi 290 . . . . . . . . 9 (𝑚 = 𝑖 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)))
6362imbi2d 344 . . . . . . . 8 (𝑚 = 𝑖 → (((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧))))
64 suceq 6296 . . . . . . . . . . . . . . 15 (𝑚 = suc 𝑖 → suc 𝑚 = suc suc 𝑖)
65 suceq 6296 . . . . . . . . . . . . . . 15 (suc 𝑚 = suc suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖)
6664, 65syl 17 . . . . . . . . . . . . . 14 (𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖)
6766fneq2d 6491 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → (𝑓 Fn suc suc 𝑚𝑓 Fn suc suc suc 𝑖))
6864fveqeq2d 6744 . . . . . . . . . . . . . 14 (𝑚 = suc 𝑖 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc suc 𝑖) = 𝑦))
6968anbi2d 632 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦)))
7064raleqdv 3338 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎)))
7167, 69, 703anbi123d 1438 . . . . . . . . . . . 12 (𝑚 = suc 𝑖 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))))
7271exbidv 1929 . . . . . . . . . . 11 (𝑚 = suc 𝑖 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))))
7372imbi1d 345 . . . . . . . . . 10 (𝑚 = suc 𝑖 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
7473albidv 1928 . . . . . . . . 9 (𝑚 = suc 𝑖 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
7574imbi2d 344 . . . . . . . 8 (𝑚 = suc 𝑖 → (((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
76 suceq 6296 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → suc 𝑚 = suc 𝑛)
77 suceq 6296 . . . . . . . . . . . . . . 15 (suc 𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc 𝑛)
7876, 77syl 17 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → suc suc 𝑚 = suc suc 𝑛)
7978fneq2d 6491 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (𝑓 Fn suc suc 𝑚𝑓 Fn suc suc 𝑛))
8076fveqeq2d 6744 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc 𝑛) = 𝑦))
8180anbi2d 632 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦)))
8276raleqdv 3338 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)))
8379, 81, 823anbi123d 1438 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎))))
8483exbidv 1929 . . . . . . . . . . 11 (𝑚 = 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎))))
8584imbi1d 345 . . . . . . . . . 10 (𝑚 = 𝑛 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
8685albidv 1928 . . . . . . . . 9 (𝑚 = 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
8786imbi2d 344 . . . . . . . 8 (𝑚 = 𝑛 → (((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
88 breq12 5073 . . . . . . . . . . . . 13 (((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) → ((𝑓‘∅)𝑅(𝑓‘1o) ↔ 𝑥𝑅𝑦))
8988biimpa 480 . . . . . . . . . . . 12 ((((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)) → 𝑥𝑅𝑦)
90893adant1 1132 . . . . . . . . . . 11 ((𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)) → 𝑥𝑅𝑦)
91 ssbr 5112 . . . . . . . . . . . 12 (𝑅𝑆 → (𝑥𝑅𝑦𝑥𝑆𝑦))
9291adantr 484 . . . . . . . . . . 11 ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → (𝑥𝑅𝑦𝑥𝑆𝑦))
9390, 92syl5 34 . . . . . . . . . 10 ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ((𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)) → 𝑥𝑆𝑦))
9493exlimdv 1941 . . . . . . . . 9 ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → (∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)) → 𝑥𝑆𝑦))
9594alrimiv 1935 . . . . . . . 8 ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)) → 𝑥𝑆𝑦))
96 fvex 6749 . . . . . . . . . . . . . . 15 (𝑓‘suc 𝑖) ∈ V
97 eqeq2 2750 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑓‘suc 𝑖) → ((𝑔‘suc 𝑖) = 𝑧 ↔ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)))
9897anbi2d 632 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑓‘suc 𝑖) → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖))))
99983anbi2d 1443 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑓‘suc 𝑖) → ((𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
10099exbidv 1929 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑓‘suc 𝑖) → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏))))
101 breq2 5072 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑓‘suc 𝑖) → (𝑥𝑆𝑧𝑥𝑆(𝑓‘suc 𝑖)))
102100, 101imbi12d 348 . . . . . . . . . . . . . . 15 (𝑧 = (𝑓‘suc 𝑖) → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖))))
10396, 102spcv 3533 . . . . . . . . . . . . . 14 (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)))
104 simpr1 1196 . . . . . . . . . . . . . . . . . . 19 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑓 Fn suc suc suc 𝑖)
105 sssucid 6308 . . . . . . . . . . . . . . . . . . 19 suc suc 𝑖 ⊆ suc suc suc 𝑖
106 fnssres 6519 . . . . . . . . . . . . . . . . . . 19 ((𝑓 Fn suc suc suc 𝑖 ∧ suc suc 𝑖 ⊆ suc suc suc 𝑖) → (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖)
107104, 105, 106sylancl 589 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖)
108 peano2 7687 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ ω → suc 𝑖 ∈ ω)
109108ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → suc 𝑖 ∈ ω)
110 nnord 7671 . . . . . . . . . . . . . . . . . . . . . 22 (suc 𝑖 ∈ ω → Ord suc 𝑖)
111109, 110syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → Ord suc 𝑖)
112 0elsuc 7633 . . . . . . . . . . . . . . . . . . . . 21 (Ord suc 𝑖 → ∅ ∈ suc suc 𝑖)
113111, 112syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → ∅ ∈ suc suc 𝑖)
114113fvresd 6756 . . . . . . . . . . . . . . . . . . 19 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘∅) = (𝑓‘∅))
115 simpr2l 1234 . . . . . . . . . . . . . . . . . . 19 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∅) = 𝑥)
116114, 115eqtrd 2778 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥)
117 vex 3425 . . . . . . . . . . . . . . . . . . . . 21 𝑖 ∈ V
118117sucex 7609 . . . . . . . . . . . . . . . . . . . 20 suc 𝑖 ∈ V
119118sucid 6310 . . . . . . . . . . . . . . . . . . 19 suc 𝑖 ∈ suc suc 𝑖
120 fvres 6755 . . . . . . . . . . . . . . . . . . 19 (suc 𝑖 ∈ suc suc 𝑖 → ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖))
121119, 120mp1i 13 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖))
122 simplr3 1219 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))
123 elelsuc 6303 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 ∈ suc 𝑖𝑏 ∈ suc suc 𝑖)
124123adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → 𝑏 ∈ suc suc 𝑖)
12535, 122, 124rspcdva 3552 . . . . . . . . . . . . . . . . . . . 20 ((((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → (𝑓𝑏)𝑅(𝑓‘suc 𝑏))
126124fvresd 6756 . . . . . . . . . . . . . . . . . . . 20 ((((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘𝑏) = (𝑓𝑏))
127 ordsucelsuc 7620 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord suc 𝑖 → (𝑏 ∈ suc 𝑖 ↔ suc 𝑏 ∈ suc suc 𝑖))
128111, 127syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑏 ∈ suc 𝑖 ↔ suc 𝑏 ∈ suc suc 𝑖))
129128biimpa 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → suc 𝑏 ∈ suc suc 𝑖)
130129fvresd 6756 . . . . . . . . . . . . . . . . . . . 20 ((((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘suc 𝑏) = (𝑓‘suc 𝑏))
131125, 126, 1303brtr4d 5100 . . . . . . . . . . . . . . . . . . 19 ((((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
132131ralrimiva 3106 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
133 vex 3425 . . . . . . . . . . . . . . . . . . . 20 𝑓 ∈ V
134133resex 5914 . . . . . . . . . . . . . . . . . . 19 (𝑓 ↾ suc suc 𝑖) ∈ V
135 fneq1 6488 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔 Fn suc suc 𝑖 ↔ (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖))
136 fveq1 6735 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘∅) = ((𝑓 ↾ suc suc 𝑖)‘∅))
137136eqeq1d 2740 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘∅) = 𝑥 ↔ ((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥))
138 fveq1 6735 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘suc 𝑖) = ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖))
139138eqeq1d 2740 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘suc 𝑖) = (𝑓‘suc 𝑖) ↔ ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖)))
140137, 139anbi12d 634 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑓 ↾ suc suc 𝑖) → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ↔ (((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥 ∧ ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖))))
141 fveq1 6735 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔𝑏) = ((𝑓 ↾ suc suc 𝑖)‘𝑏))
142 fveq1 6735 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘suc 𝑏) = ((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
143141, 142breq12d 5081 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔𝑏)𝑅(𝑔‘suc 𝑏) ↔ ((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)))
144143ralbidv 3119 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑓 ↾ suc suc 𝑖) → (∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏) ↔ ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)))
145135, 140, 1443anbi123d 1438 . . . . . . . . . . . . . . . . . . 19 (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) ↔ ((𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖 ∧ (((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥 ∧ ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))))
146134, 145spcev 3534 . . . . . . . . . . . . . . . . . 18 (((𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖 ∧ (((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥 ∧ ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)) → ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)))
147107, 116, 121, 132, 146syl121anc 1377 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)))
148 simplrl 777 . . . . . . . . . . . . . . . . . . . . 21 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑅𝑆)
149 simpr3 1198 . . . . . . . . . . . . . . . . . . . . 21 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))
150 ssbr 5112 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅𝑆 → ((𝑓𝑎)𝑅(𝑓‘suc 𝑎) → (𝑓𝑎)𝑆(𝑓‘suc 𝑎)))
151150ralimdv 3102 . . . . . . . . . . . . . . . . . . . . 21 (𝑅𝑆 → (∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎) → ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑆(𝑓‘suc 𝑎)))
152148, 149, 151sylc 65 . . . . . . . . . . . . . . . . . . . 20 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑆(𝑓‘suc 𝑎))
153 fveq2 6736 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = suc 𝑖 → (𝑓𝑎) = (𝑓‘suc 𝑖))
154 suceq 6296 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = suc 𝑖 → suc 𝑎 = suc suc 𝑖)
155154fveq2d 6740 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = suc 𝑖 → (𝑓‘suc 𝑎) = (𝑓‘suc suc 𝑖))
156153, 155breq12d 5081 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = suc 𝑖 → ((𝑓𝑎)𝑆(𝑓‘suc 𝑎) ↔ (𝑓‘suc 𝑖)𝑆(𝑓‘suc suc 𝑖)))
157156rspcv 3545 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑖 ∈ suc suc 𝑖 → (∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑆(𝑓‘suc 𝑎) → (𝑓‘suc 𝑖)𝑆(𝑓‘suc suc 𝑖)))
158119, 152, 157mpsyl 68 . . . . . . . . . . . . . . . . . . 19 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc 𝑖)𝑆(𝑓‘suc suc 𝑖))
159 simpr2r 1235 . . . . . . . . . . . . . . . . . . 19 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc suc 𝑖) = 𝑦)
160158, 159breqtrd 5094 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc 𝑖)𝑆𝑦)
161 breq1 5071 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (𝑓‘suc 𝑖) → (𝑧𝑆𝑦 ↔ (𝑓‘suc 𝑖)𝑆𝑦))
162101, 161anbi12d 634 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = (𝑓‘suc 𝑖) → ((𝑥𝑆𝑧𝑧𝑆𝑦) ↔ (𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦)))
16396, 162spcev 3534 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → ∃𝑧(𝑥𝑆𝑧𝑧𝑆𝑦))
164 vex 3425 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
165 vex 3425 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
166164, 165brco 5754 . . . . . . . . . . . . . . . . . . . 20 (𝑥(𝑆𝑆)𝑦 ↔ ∃𝑧(𝑥𝑆𝑧𝑧𝑆𝑦))
167163, 166sylibr 237 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → 𝑥(𝑆𝑆)𝑦)
168 simplrr 778 . . . . . . . . . . . . . . . . . . . 20 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑆𝑆) ⊆ 𝑆)
169168ssbrd 5111 . . . . . . . . . . . . . . . . . . 19 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑥(𝑆𝑆)𝑦𝑥𝑆𝑦))
170167, 169syl5 34 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → 𝑥𝑆𝑦))
171160, 170mpan2d 694 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑥𝑆(𝑓‘suc 𝑖) → 𝑥𝑆𝑦))
172147, 171embantd 59 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎))) → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)) → 𝑥𝑆𝑦))
173172ex 416 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)) → 𝑥𝑆𝑦)))
174173com23 86 . . . . . . . . . . . . . 14 ((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
175103, 174syl5 34 . . . . . . . . . . . . 13 ((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆)) → (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
1761753impia 1119 . . . . . . . . . . . 12 ((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
177176exlimdv 1941 . . . . . . . . . . 11 ((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → (∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
178177alrimiv 1935 . . . . . . . . . 10 ((𝑖 ∈ ω ∧ (𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
1791783exp 1121 . . . . . . . . 9 (𝑖 ∈ ω → ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
180179a2d 29 . . . . . . . 8 (𝑖 ∈ ω → (((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
18124, 63, 75, 87, 95, 180finds 7695 . . . . . . 7 (𝑛 ∈ ω → ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
182181com12 32 . . . . . 6 ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → (𝑛 ∈ ω → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
183182ralrimiv 3105 . . . . 5 ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
184 ralcom4 3160 . . . . . 6 (∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
185 r19.23v 3206 . . . . . . 7 (∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
186185albii 1827 . . . . . 6 (∀𝑦𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
187184, 186bitri 278 . . . . 5 (∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
188183, 187sylib 221 . . . 4 ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
189 brttrcl2 33536 . . . . . . 7 (𝑥t++𝑅𝑦 ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)))
190 df-br 5069 . . . . . . 7 (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
191189, 190bitr3i 280 . . . . . 6 (∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
192 df-br 5069 . . . . . 6 (𝑥𝑆𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
193191, 192imbi12i 354 . . . . 5 ((∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
194193albii 1827 . . . 4 (∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
195188, 194sylib 221 . . 3 ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
196195alrimiv 1935 . 2 ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
197 relttrcl 33534 . . 3 Rel t++𝑅
198 ssrel 5669 . . 3 (Rel t++𝑅 → (t++𝑅𝑆 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆)))
199197, 198ax-mp 5 . 2 (t++𝑅𝑆 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
200196, 199sylibr 237 1 ((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → t++𝑅𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089  wal 1541   = wceq 1543  wex 1787  wcel 2111  wral 3062  wrex 3063  wss 3881  c0 4252  {csn 4556  cop 4562   class class class wbr 5068  cres 5568  ccom 5570  Rel wrel 5571  Ord word 6230  suc csuc 6233   Fn wfn 6393  cfv 6398  ωcom 7663  1oc1o 8216  t++cttrcl 33529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5207  ax-nul 5214  ax-pr 5337  ax-un 7542
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3423  df-sbc 3710  df-csb 3827  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4253  df-if 4455  df-pw 4530  df-sn 4557  df-pr 4559  df-tp 4561  df-op 4563  df-uni 4835  df-int 4875  df-iun 4921  df-br 5069  df-opab 5131  df-mpt 5151  df-tr 5177  df-id 5470  df-eprel 5475  df-po 5483  df-so 5484  df-fr 5524  df-we 5526  df-xp 5572  df-rel 5573  df-cnv 5574  df-co 5575  df-dm 5576  df-rn 5577  df-res 5578  df-ima 5579  df-pred 6176  df-ord 6234  df-on 6235  df-lim 6236  df-suc 6237  df-iota 6356  df-fun 6400  df-fn 6401  df-f 6402  df-f1 6403  df-fo 6404  df-f1o 6405  df-fv 6406  df-ov 7235  df-oprab 7236  df-mpo 7237  df-om 7664  df-wrecs 8068  df-recs 8129  df-rdg 8167  df-1o 8223  df-oadd 8227  df-ttrcl 33530
This theorem is referenced by:  dfttrcl2  33546
  Copyright terms: Public domain W3C validator