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 
|- ( ( R C_ S /\ ( S o. S ) C_ S ) -> t++ R C_ S )

Proof

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