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