Metamath Proof Explorer

Theorem ttrclss

Description: If R is a subclass of S and S is transitive, then the transitive closure of R is a subclass of S . (Contributed by Scott Fenton, 20-Oct-2024)

Ref Expression
Assertion ttrclss ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → t++ 𝑅 ⊆ 𝑆 )

Proof

Step Hyp Ref Expression
1 suceq ⊢ ( 𝑚 = ∅ → suc 𝑚 = suc ∅ )
2 suceq ⊢ ( suc 𝑚 = suc ∅ → suc suc 𝑚 = suc suc ∅ )
3 1 2 syl ⊢ ( 𝑚 = ∅ → suc suc 𝑚 = suc suc ∅ )
4 3 fneq2d ⊢ ( 𝑚 = ∅ → ( 𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc ∅ ) )
5 df-1o ⊢ 1o = suc ∅
6 1 5 eqtr4di ⊢ ( 𝑚 = ∅ → suc 𝑚 = 1o )
7 6 fveqeq2d ⊢ ( 𝑚 = ∅ → ( ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ↔ ( 𝑓 ‘ 1o ) = 𝑦 ) )
8 7 anbi2d ⊢ ( 𝑚 = ∅ → ( ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ↔ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ) )
9 df1o2 ⊢ 1o = { ∅ }
10 6 9 eqtrdi ⊢ ( 𝑚 = ∅ → suc 𝑚 = { ∅ } )
11 10 raleqdv ⊢ ( 𝑚 = ∅ → ( ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ∀ 𝑎 ∈ { ∅ } ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
12 0ex ⊢ ∅ ∈ V
13 fveq2 ⊢ ( 𝑎 = ∅ → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ ∅ ) )
14 suceq ⊢ ( 𝑎 = ∅ → suc 𝑎 = suc ∅ )
15 14 5 eqtr4di ⊢ ( 𝑎 = ∅ → suc 𝑎 = 1o )
16 15 fveq2d ⊢ ( 𝑎 = ∅ → ( 𝑓 ‘ suc 𝑎 ) = ( 𝑓 ‘ 1o ) )
17 13 16 breq12d ⊢ ( 𝑎 = ∅ → ( ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) )
18 12 17 ralsn ⊢ ( ∀ 𝑎 ∈ { ∅ } ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) )
19 11 18 bitrdi ⊢ ( 𝑚 = ∅ → ( ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) )
20 4 8 19 3anbi123d ⊢ ( 𝑚 = ∅ → ( ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ( 𝑓 Fn suc suc ∅ ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) ) )
21 20 exbidv ⊢ ( 𝑚 = ∅ → ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn suc suc ∅ ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) ) )
22 21 imbi1d ⊢ ( 𝑚 = ∅ → ( ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ( ∃ 𝑓 ( 𝑓 Fn suc suc ∅ ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) → 𝑥 𝑆 𝑦 ) ) )
23 22 albidv ⊢ ( 𝑚 = ∅ → ( ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc ∅ ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) → 𝑥 𝑆 𝑦 ) ) )
24 23 imbi2d ⊢ ( 𝑚 = ∅ → ( ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) ↔ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc ∅ ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) → 𝑥 𝑆 𝑦 ) ) ) )
25 suceq ⊢ ( 𝑚 = 𝑖 → suc 𝑚 = suc 𝑖 )
26 suceq ⊢ ( suc 𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc 𝑖 )
27 25 26 syl ⊢ ( 𝑚 = 𝑖 → suc suc 𝑚 = suc suc 𝑖 )
28 27 fneq2d ⊢ ( 𝑚 = 𝑖 → ( 𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑖 ) )
29 25 fveqeq2d ⊢ ( 𝑚 = 𝑖 → ( ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ↔ ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ) )
30 29 anbi2d ⊢ ( 𝑚 = 𝑖 → ( ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ↔ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ) ) )
31 25 raleqdv ⊢ ( 𝑚 = 𝑖 → ( ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ∀ 𝑎 ∈ suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
32 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) )
33 suceq ⊢ ( 𝑎 = 𝑏 → suc 𝑎 = suc 𝑏 )
34 33 fveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑓 ‘ suc 𝑎 ) = ( 𝑓 ‘ suc 𝑏 ) )
35 32 34 breq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ( 𝑓 ‘ 𝑏 ) 𝑅 ( 𝑓 ‘ suc 𝑏 ) ) )
36 35 cbvralvw ⊢ ( ∀ 𝑎 ∈ suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ∀ 𝑏 ∈ suc 𝑖 ( 𝑓 ‘ 𝑏 ) 𝑅 ( 𝑓 ‘ suc 𝑏 ) )
37 31 36 bitrdi ⊢ ( 𝑚 = 𝑖 → ( ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ∀ 𝑏 ∈ suc 𝑖 ( 𝑓 ‘ 𝑏 ) 𝑅 ( 𝑓 ‘ suc 𝑏 ) ) )
38 28 30 37 3anbi123d ⊢ ( 𝑚 = 𝑖 → ( ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ( 𝑓 Fn suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑓 ‘ 𝑏 ) 𝑅 ( 𝑓 ‘ suc 𝑏 ) ) ) )
39 38 exbidv ⊢ ( 𝑚 = 𝑖 → ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑓 ‘ 𝑏 ) 𝑅 ( 𝑓 ‘ suc 𝑏 ) ) ) )
40 fneq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 Fn suc suc 𝑖 ↔ 𝑔 Fn suc suc 𝑖 ) )
41 fveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ ∅ ) = ( 𝑔 ‘ ∅ ) )
42 41 eqeq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ‘ ∅ ) = 𝑥 ↔ ( 𝑔 ‘ ∅ ) = 𝑥 ) )
43 fveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ suc 𝑖 ) = ( 𝑔 ‘ suc 𝑖 ) )
44 43 eqeq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ↔ ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ) )
45 42 44 anbi12d ⊢ ( 𝑓 = 𝑔 → ( ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ) ↔ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ) ) )
46 fveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 𝑏 ) = ( 𝑔 ‘ 𝑏 ) )
47 fveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ suc 𝑏 ) = ( 𝑔 ‘ suc 𝑏 ) )
48 46 47 breq12d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ‘ 𝑏 ) 𝑅 ( 𝑓 ‘ suc 𝑏 ) ↔ ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) )
49 48 ralbidv ⊢ ( 𝑓 = 𝑔 → ( ∀ 𝑏 ∈ suc 𝑖 ( 𝑓 ‘ 𝑏 ) 𝑅 ( 𝑓 ‘ suc 𝑏 ) ↔ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) )
50 40 45 49 3anbi123d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 Fn suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑓 ‘ 𝑏 ) 𝑅 ( 𝑓 ‘ suc 𝑏 ) ) ↔ ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) ) )
51 50 cbvexvw ⊢ ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑓 ‘ 𝑏 ) 𝑅 ( 𝑓 ‘ suc 𝑏 ) ) ↔ ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) )
52 39 51 bitrdi ⊢ ( 𝑚 = 𝑖 → ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) ) )
53 52 imbi1d ⊢ ( 𝑚 = 𝑖 → ( ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑦 ) ) )
54 53 albidv ⊢ ( 𝑚 = 𝑖 → ( ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ∀ 𝑦 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑦 ) ) )
55 eqeq2 ⊢ ( 𝑦 = 𝑧 → ( ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ↔ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) )
56 55 anbi2d ⊢ ( 𝑦 = 𝑧 → ( ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ) ↔ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ) )
57 56 3anbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) ↔ ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) ) )
58 57 exbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) ↔ ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) ) )
59 breq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 𝑆 𝑦 ↔ 𝑥 𝑆 𝑧 ) )
60 58 59 imbi12d ⊢ ( 𝑦 = 𝑧 → ( ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑦 ) ↔ ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑧 ) ) )
61 60 cbvalvw ⊢ ( ∀ 𝑦 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑦 ) ↔ ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑧 ) )
62 54 61 bitrdi ⊢ ( 𝑚 = 𝑖 → ( ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑧 ) ) )
63 62 imbi2d ⊢ ( 𝑚 = 𝑖 → ( ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) ↔ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑧 ) ) ) )
64 suceq ⊢ ( 𝑚 = suc 𝑖 → suc 𝑚 = suc suc 𝑖 )
65 suceq ⊢ ( suc 𝑚 = suc suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖 )
66 64 65 syl ⊢ ( 𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖 )
67 66 fneq2d ⊢ ( 𝑚 = suc 𝑖 → ( 𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc suc 𝑖 ) )
68 64 fveqeq2d ⊢ ( 𝑚 = suc 𝑖 → ( ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ↔ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) )
69 68 anbi2d ⊢ ( 𝑚 = suc 𝑖 → ( ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ↔ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ) )
70 64 raleqdv ⊢ ( 𝑚 = suc 𝑖 → ( ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
71 67 69 70 3anbi123d ⊢ ( 𝑚 = suc 𝑖 → ( ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
72 71 exbidv ⊢ ( 𝑚 = suc 𝑖 → ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
73 72 imbi1d ⊢ ( 𝑚 = suc 𝑖 → ( ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) )
74 73 albidv ⊢ ( 𝑚 = suc 𝑖 → ( ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) )
75 74 imbi2d ⊢ ( 𝑚 = suc 𝑖 → ( ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) ↔ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) ) )
76 suceq ⊢ ( 𝑚 = 𝑛 → suc 𝑚 = suc 𝑛 )
77 suceq ⊢ ( suc 𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc 𝑛 )
78 76 77 syl ⊢ ( 𝑚 = 𝑛 → suc suc 𝑚 = suc suc 𝑛 )
79 78 fneq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑛 ) )
80 76 fveqeq2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ↔ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) )
81 80 anbi2d ⊢ ( 𝑚 = 𝑛 → ( ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ↔ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ) )
82 76 raleqdv ⊢ ( 𝑚 = 𝑛 → ( ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
83 79 81 82 3anbi123d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
84 83 exbidv ⊢ ( 𝑚 = 𝑛 → ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
85 84 imbi1d ⊢ ( 𝑚 = 𝑛 → ( ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) )
86 85 albidv ⊢ ( 𝑚 = 𝑛 → ( ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) )
87 86 imbi2d ⊢ ( 𝑚 = 𝑛 → ( ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑚 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) ↔ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) ) )
88 breq12 ⊢ ( ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) → ( ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ↔ 𝑥 𝑅 𝑦 ) )
89 88 biimpa ⊢ ( ( ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) → 𝑥 𝑅 𝑦 )
90 89 3adant1 ⊢ ( ( 𝑓 Fn suc suc ∅ ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) → 𝑥 𝑅 𝑦 )
91 ssbr ⊢ ( 𝑅 ⊆ 𝑆 → ( 𝑥 𝑅 𝑦 → 𝑥 𝑆 𝑦 ) )
92 91 adantr ⊢ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ( 𝑥 𝑅 𝑦 → 𝑥 𝑆 𝑦 ) )
93 90 92 syl5 ⊢ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ( ( 𝑓 Fn suc suc ∅ ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) → 𝑥 𝑆 𝑦 ) )
94 93 exlimdv ⊢ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ( ∃ 𝑓 ( 𝑓 Fn suc suc ∅ ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) → 𝑥 𝑆 𝑦 ) )
95 94 alrimiv ⊢ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc ∅ ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) → 𝑥 𝑆 𝑦 ) )
96 fvex ⊢ ( 𝑓 ‘ suc 𝑖 ) ∈ V
97 eqeq2 ⊢ ( 𝑧 = ( 𝑓 ‘ suc 𝑖 ) → ( ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ↔ ( 𝑔 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) )
98 97 anbi2d ⊢ ( 𝑧 = ( 𝑓 ‘ suc 𝑖 ) → ( ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ↔ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) ) )
99 98 3anbi2d ⊢ ( 𝑧 = ( 𝑓 ‘ suc 𝑖 ) → ( ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) ↔ ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) ) )
100 99 exbidv ⊢ ( 𝑧 = ( 𝑓 ‘ suc 𝑖 ) → ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) ↔ ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) ) )
101 breq2 ⊢ ( 𝑧 = ( 𝑓 ‘ suc 𝑖 ) → ( 𝑥 𝑆 𝑧 ↔ 𝑥 𝑆 ( 𝑓 ‘ suc 𝑖 ) ) )
102 100 101 imbi12d ⊢ ( 𝑧 = ( 𝑓 ‘ suc 𝑖 ) → ( ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑧 ) ↔ ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 ( 𝑓 ‘ suc 𝑖 ) ) ) )
103 96 102 spcv ⊢ ( ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑧 ) → ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 ( 𝑓 ‘ suc 𝑖 ) ) )
104 simpr1 ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → 𝑓 Fn suc suc suc 𝑖 )
105 sssucid ⊢ suc suc 𝑖 ⊆ suc suc suc 𝑖
106 fnssres ⊢ ( ( 𝑓 Fn suc suc suc 𝑖 ∧ suc suc 𝑖 ⊆ suc suc suc 𝑖 ) → ( 𝑓 ↾ suc suc 𝑖 ) Fn suc suc 𝑖 )
107 104 105 106 sylancl ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ↾ suc suc 𝑖 ) Fn suc suc 𝑖 )
108 peano2 ⊢ ( 𝑖 ∈ ω → suc 𝑖 ∈ ω )
109 108 ad2antrr ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → suc 𝑖 ∈ ω )
110 nnord ⊢ ( suc 𝑖 ∈ ω → Ord suc 𝑖 )
111 109 110 syl ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → Ord suc 𝑖 )
112 0elsuc ⊢ ( Ord suc 𝑖 → ∅ ∈ suc suc 𝑖 )
113 111 112 syl ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ∅ ∈ suc suc 𝑖 )
114 113 fvresd ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ ∅ ) = ( 𝑓 ‘ ∅ ) )
115 simpr2l ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ ∅ ) = 𝑥 )
116 114 115 eqtrd ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ ∅ ) = 𝑥 )
117 vex ⊢ 𝑖 ∈ V
118 117 sucex ⊢ suc 𝑖 ∈ V
119 118 sucid ⊢ suc 𝑖 ∈ suc suc 𝑖
120 fvres ⊢ ( suc 𝑖 ∈ suc suc 𝑖 → ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) )
121 119 120 mp1i ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) )
122 simplr3 ⊢ ( ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ∧ 𝑏 ∈ suc 𝑖 ) → ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) )
123 elelsuc ⊢ ( 𝑏 ∈ suc 𝑖 → 𝑏 ∈ suc suc 𝑖 )
124 123 adantl ⊢ ( ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ∧ 𝑏 ∈ suc 𝑖 ) → 𝑏 ∈ suc suc 𝑖 )
125 35 122 124 rspcdva ⊢ ( ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ∧ 𝑏 ∈ suc 𝑖 ) → ( 𝑓 ‘ 𝑏 ) 𝑅 ( 𝑓 ‘ suc 𝑏 ) )
126 124 fvresd ⊢ ( ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ∧ 𝑏 ∈ suc 𝑖 ) → ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ 𝑏 ) = ( 𝑓 ‘ 𝑏 ) )
127 ordsucelsuc ⊢ ( Ord suc 𝑖 → ( 𝑏 ∈ suc 𝑖 ↔ suc 𝑏 ∈ suc suc 𝑖 ) )
128 111 127 syl ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑏 ∈ suc 𝑖 ↔ suc 𝑏 ∈ suc suc 𝑖 ) )
129 128 biimpa ⊢ ( ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ∧ 𝑏 ∈ suc 𝑖 ) → suc 𝑏 ∈ suc suc 𝑖 )
130 129 fvresd ⊢ ( ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ∧ 𝑏 ∈ suc 𝑖 ) → ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ suc 𝑏 ) = ( 𝑓 ‘ suc 𝑏 ) )
131 125 126 130 3brtr4d ⊢ ( ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ∧ 𝑏 ∈ suc 𝑖 ) → ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ 𝑏 ) 𝑅 ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ suc 𝑏 ) )
132 131 ralrimiva ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ∀ 𝑏 ∈ suc 𝑖 ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ 𝑏 ) 𝑅 ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ suc 𝑏 ) )
133 vex ⊢ 𝑓 ∈ V
134 133 resex ⊢ ( 𝑓 ↾ suc suc 𝑖 ) ∈ V
135 fneq1 ⊢ ( 𝑔 = ( 𝑓 ↾ suc suc 𝑖 ) → ( 𝑔 Fn suc suc 𝑖 ↔ ( 𝑓 ↾ suc suc 𝑖 ) Fn suc suc 𝑖 ) )
136 fveq1 ⊢ ( 𝑔 = ( 𝑓 ↾ suc suc 𝑖 ) → ( 𝑔 ‘ ∅ ) = ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ ∅ ) )
137 136 eqeq1d ⊢ ( 𝑔 = ( 𝑓 ↾ suc suc 𝑖 ) → ( ( 𝑔 ‘ ∅ ) = 𝑥 ↔ ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ ∅ ) = 𝑥 ) )
138 fveq1 ⊢ ( 𝑔 = ( 𝑓 ↾ suc suc 𝑖 ) → ( 𝑔 ‘ suc 𝑖 ) = ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ suc 𝑖 ) )
139 138 eqeq1d ⊢ ( 𝑔 = ( 𝑓 ↾ suc suc 𝑖 ) → ( ( 𝑔 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ↔ ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) )
140 137 139 anbi12d ⊢ ( 𝑔 = ( 𝑓 ↾ suc suc 𝑖 ) → ( ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) ↔ ( ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ ∅ ) = 𝑥 ∧ ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) ) )
141 fveq1 ⊢ ( 𝑔 = ( 𝑓 ↾ suc suc 𝑖 ) → ( 𝑔 ‘ 𝑏 ) = ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ 𝑏 ) )
142 fveq1 ⊢ ( 𝑔 = ( 𝑓 ↾ suc suc 𝑖 ) → ( 𝑔 ‘ suc 𝑏 ) = ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ suc 𝑏 ) )
143 141 142 breq12d ⊢ ( 𝑔 = ( 𝑓 ↾ suc suc 𝑖 ) → ( ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ↔ ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ 𝑏 ) 𝑅 ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ suc 𝑏 ) ) )
144 143 ralbidv ⊢ ( 𝑔 = ( 𝑓 ↾ suc suc 𝑖 ) → ( ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ↔ ∀ 𝑏 ∈ suc 𝑖 ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ 𝑏 ) 𝑅 ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ suc 𝑏 ) ) )
145 135 140 144 3anbi123d ⊢ ( 𝑔 = ( 𝑓 ↾ 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 𝑏 ) ) ) )
146 134 145 spcev ⊢ ( ( ( 𝑓 ↾ suc suc 𝑖 ) Fn suc suc 𝑖 ∧ ( ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ ∅ ) = 𝑥 ∧ ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ 𝑏 ) 𝑅 ( ( 𝑓 ↾ suc suc 𝑖 ) ‘ suc 𝑏 ) ) → ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) )
147 107 116 121 132 146 syl121anc ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) )
148 simplrl ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → 𝑅 ⊆ 𝑆 )
149 simpr3 ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) )
150 ssbr ⊢ ( 𝑅 ⊆ 𝑆 → ( ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) → ( 𝑓 ‘ 𝑎 ) 𝑆 ( 𝑓 ‘ suc 𝑎 ) ) )
151 150 ralimdv ⊢ ( 𝑅 ⊆ 𝑆 → ( ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) → ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑆 ( 𝑓 ‘ suc 𝑎 ) ) )
152 148 149 151 sylc ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑆 ( 𝑓 ‘ suc 𝑎 ) )
153 fveq2 ⊢ ( 𝑎 = suc 𝑖 → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ suc 𝑖 ) )
154 suceq ⊢ ( 𝑎 = suc 𝑖 → suc 𝑎 = suc suc 𝑖 )
155 154 fveq2d ⊢ ( 𝑎 = suc 𝑖 → ( 𝑓 ‘ suc 𝑎 ) = ( 𝑓 ‘ suc suc 𝑖 ) )
156 153 155 breq12d ⊢ ( 𝑎 = suc 𝑖 → ( ( 𝑓 ‘ 𝑎 ) 𝑆 ( 𝑓 ‘ suc 𝑎 ) ↔ ( 𝑓 ‘ suc 𝑖 ) 𝑆 ( 𝑓 ‘ suc suc 𝑖 ) ) )
157 156 rspcv ⊢ ( suc 𝑖 ∈ suc suc 𝑖 → ( ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑆 ( 𝑓 ‘ suc 𝑎 ) → ( 𝑓 ‘ suc 𝑖 ) 𝑆 ( 𝑓 ‘ suc suc 𝑖 ) ) )
158 119 152 157 mpsyl ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ suc 𝑖 ) 𝑆 ( 𝑓 ‘ suc suc 𝑖 ) )
159 simpr2r ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 )
160 158 159 breqtrd ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ suc 𝑖 ) 𝑆 𝑦 )
161 breq1 ⊢ ( 𝑧 = ( 𝑓 ‘ suc 𝑖 ) → ( 𝑧 𝑆 𝑦 ↔ ( 𝑓 ‘ suc 𝑖 ) 𝑆 𝑦 ) )
162 101 161 anbi12d ⊢ ( 𝑧 = ( 𝑓 ‘ suc 𝑖 ) → ( ( 𝑥 𝑆 𝑧 ∧ 𝑧 𝑆 𝑦 ) ↔ ( 𝑥 𝑆 ( 𝑓 ‘ suc 𝑖 ) ∧ ( 𝑓 ‘ suc 𝑖 ) 𝑆 𝑦 ) ) )
163 96 162 spcev ⊢ ( ( 𝑥 𝑆 ( 𝑓 ‘ suc 𝑖 ) ∧ ( 𝑓 ‘ suc 𝑖 ) 𝑆 𝑦 ) → ∃ 𝑧 ( 𝑥 𝑆 𝑧 ∧ 𝑧 𝑆 𝑦 ) )
164 vex ⊢ 𝑥 ∈ V
165 vex ⊢ 𝑦 ∈ V
166 164 165 brco ⊢ ( 𝑥 ( 𝑆 ∘ 𝑆 ) 𝑦 ↔ ∃ 𝑧 ( 𝑥 𝑆 𝑧 ∧ 𝑧 𝑆 𝑦 ) )
167 163 166 sylibr ⊢ ( ( 𝑥 𝑆 ( 𝑓 ‘ suc 𝑖 ) ∧ ( 𝑓 ‘ suc 𝑖 ) 𝑆 𝑦 ) → 𝑥 ( 𝑆 ∘ 𝑆 ) 𝑦 )
168 simplrr ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 )
169 168 ssbrd ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑥 ( 𝑆 ∘ 𝑆 ) 𝑦 → 𝑥 𝑆 𝑦 ) )
170 167 169 syl5 ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( ( 𝑥 𝑆 ( 𝑓 ‘ suc 𝑖 ) ∧ ( 𝑓 ‘ suc 𝑖 ) 𝑆 𝑦 ) → 𝑥 𝑆 𝑦 ) )
171 160 170 mpan2d ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑥 𝑆 ( 𝑓 ‘ suc 𝑖 ) → 𝑥 𝑆 𝑦 ) )
172 147 171 embantd ⊢ ( ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) ∧ ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 ( 𝑓 ‘ suc 𝑖 ) ) → 𝑥 𝑆 𝑦 ) )
173 172 ex ⊢ ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) → ( ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → ( ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 ( 𝑓 ‘ suc 𝑖 ) ) → 𝑥 𝑆 𝑦 ) ) )
174 173 com23 ⊢ ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) → ( ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 ( 𝑓 ‘ suc 𝑖 ) ) → ( ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) )
175 103 174 syl5 ⊢ ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ) → ( ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑧 ) → ( ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) )
176 175 3impia ⊢ ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ∧ ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑧 ) ) → ( ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) )
177 176 exlimdv ⊢ ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ∧ ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑧 ) ) → ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) )
178 177 alrimiv ⊢ ( ( 𝑖 ∈ ω ∧ ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) ∧ ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑧 ) ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) )
179 178 3exp ⊢ ( 𝑖 ∈ ω → ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ( ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑧 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) ) )
180 179 a2d ⊢ ( 𝑖 ∈ ω → ( ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑧 ( ∃ 𝑔 ( 𝑔 Fn suc suc 𝑖 ∧ ( ( 𝑔 ‘ ∅ ) = 𝑥 ∧ ( 𝑔 ‘ suc 𝑖 ) = 𝑧 ) ∧ ∀ 𝑏 ∈ suc 𝑖 ( 𝑔 ‘ 𝑏 ) 𝑅 ( 𝑔 ‘ suc 𝑏 ) ) → 𝑥 𝑆 𝑧 ) ) → ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc suc 𝑖 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc suc 𝑖 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc suc 𝑖 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) ) )
181 24 63 75 87 95 180 finds ⊢ ( 𝑛 ∈ ω → ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) )
182 181 com12 ⊢ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ( 𝑛 ∈ ω → ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ) )
183 182 ralrimiv ⊢ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑛 ∈ ω ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) )
184 ralcom4 ⊢ ( ∀ 𝑛 ∈ ω ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ∀ 𝑦 ∀ 𝑛 ∈ ω ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) )
185 r19.23v ⊢ ( ∀ 𝑛 ∈ ω ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ( ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) )
186 185 albii ⊢ ( ∀ 𝑦 ∀ 𝑛 ∈ ω ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ∀ 𝑦 ( ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) )
187 184 186 bitri ⊢ ( ∀ 𝑛 ∈ ω ∀ 𝑦 ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ∀ 𝑦 ( ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) )
188 183 187 sylib ⊢ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑦 ( ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) )
189 brttrcl2 ⊢ ( 𝑥 t++ 𝑅 𝑦 ↔ ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
190 df-br ⊢ ( 𝑥 t++ 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ t++ 𝑅 )
191 189 190 bitr3i ⊢ ( ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ t++ 𝑅 )
192 df-br ⊢ ( 𝑥 𝑆 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 )
193 191 192 imbi12i ⊢ ( ( ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ t++ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) )
194 193 albii ⊢ ( ∀ 𝑦 ( ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 𝑆 𝑦 ) ↔ ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ t++ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) )
195 188 194 sylib ⊢ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ t++ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) )
196 195 alrimiv ⊢ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ t++ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) )
197 relttrcl ⊢ Rel t++ 𝑅
198 ssrel ⊢ ( Rel t++ 𝑅 → ( t++ 𝑅 ⊆ 𝑆 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ t++ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) ) )
199 197 198 ax-mp ⊢ ( t++ 𝑅 ⊆ 𝑆 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ t++ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) )
200 196 199 sylibr ⊢ ( ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → t++ 𝑅 ⊆ 𝑆 )