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 1 suceqd 
 |-  ( m = (/) -> suc suc m = suc suc (/) )
3 2 fneq2d 
 |-  ( m = (/) -> ( f Fn suc suc m <-> f Fn suc suc (/) ) )
4 df-1o 
 |-  1o = suc (/)
5 1 4 eqtr4di 
 |-  ( m = (/) -> suc m = 1o )
6 5 fveqeq2d 
 |-  ( m = (/) -> ( ( f ` suc m ) = y <-> ( f ` 1o ) = y ) )
7 6 anbi2d 
 |-  ( m = (/) -> ( ( ( f ` (/) ) = x /\ ( f ` suc m ) = y ) <-> ( ( f ` (/) ) = x /\ ( f ` 1o ) = y ) ) )
8 df1o2 
 |-  1o = { (/) }
9 5 8 eqtrdi 
 |-  ( m = (/) -> suc m = { (/) } )
10 9 raleqdv 
 |-  ( m = (/) -> ( A. a e. suc m ( f ` a ) R ( f ` suc a ) <-> A. a e. { (/) } ( f ` a ) R ( f ` suc a ) ) )
11 0ex 
 |-  (/) e. _V
12 fveq2 
 |-  ( a = (/) -> ( f ` a ) = ( f ` (/) ) )
13 suceq 
 |-  ( a = (/) -> suc a = suc (/) )
14 13 4 eqtr4di 
 |-  ( a = (/) -> suc a = 1o )
15 14 fveq2d 
 |-  ( a = (/) -> ( f ` suc a ) = ( f ` 1o ) )
16 12 15 breq12d 
 |-  ( a = (/) -> ( ( f ` a ) R ( f ` suc a ) <-> ( f ` (/) ) R ( f ` 1o ) ) )
17 11 16 ralsn 
 |-  ( A. a e. { (/) } ( f ` a ) R ( f ` suc a ) <-> ( f ` (/) ) R ( f ` 1o ) )
18 10 17 bitrdi 
 |-  ( m = (/) -> ( A. a e. suc m ( f ` a ) R ( f ` suc a ) <-> ( f ` (/) ) R ( f ` 1o ) ) )
19 3 7 18 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 ) ) ) )
20 19 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 ) ) ) )
21 20 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 ) ) )
22 21 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 ) ) )
23 22 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 ) ) ) )
24 suceq 
 |-  ( m = i -> suc m = suc i )
25 24 suceqd 
 |-  ( m = i -> suc suc m = suc suc i )
26 25 fneq2d 
 |-  ( m = i -> ( f Fn suc suc m <-> f Fn suc suc i ) )
27 24 fveqeq2d 
 |-  ( m = i -> ( ( f ` suc m ) = y <-> ( f ` suc i ) = y ) )
28 27 anbi2d 
 |-  ( m = i -> ( ( ( f ` (/) ) = x /\ ( f ` suc m ) = y ) <-> ( ( f ` (/) ) = x /\ ( f ` suc i ) = y ) ) )
29 24 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 ) ) )
30 fveq2 
 |-  ( a = b -> ( f ` a ) = ( f ` b ) )
31 suceq 
 |-  ( a = b -> suc a = suc b )
32 31 fveq2d 
 |-  ( a = b -> ( f ` suc a ) = ( f ` suc b ) )
33 30 32 breq12d 
 |-  ( a = b -> ( ( f ` a ) R ( f ` suc a ) <-> ( f ` b ) R ( f ` suc b ) ) )
34 33 cbvralvw 
 |-  ( A. a e. suc i ( f ` a ) R ( f ` suc a ) <-> A. b e. suc i ( f ` b ) R ( f ` suc b ) )
35 29 34 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 ) ) )
36 26 28 35 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 ) ) ) )
37 36 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 ) ) ) )
38 fneq1 
 |-  ( f = g -> ( f Fn suc suc i <-> g Fn suc suc i ) )
39 fveq1 
 |-  ( f = g -> ( f ` (/) ) = ( g ` (/) ) )
40 39 eqeq1d 
 |-  ( f = g -> ( ( f ` (/) ) = x <-> ( g ` (/) ) = x ) )
41 fveq1 
 |-  ( f = g -> ( f ` suc i ) = ( g ` suc i ) )
42 41 eqeq1d 
 |-  ( f = g -> ( ( f ` suc i ) = y <-> ( g ` suc i ) = y ) )
43 40 42 anbi12d 
 |-  ( f = g -> ( ( ( f ` (/) ) = x /\ ( f ` suc i ) = y ) <-> ( ( g ` (/) ) = x /\ ( g ` suc i ) = y ) ) )
44 fveq1 
 |-  ( f = g -> ( f ` b ) = ( g ` b ) )
45 fveq1 
 |-  ( f = g -> ( f ` suc b ) = ( g ` suc b ) )
46 44 45 breq12d 
 |-  ( f = g -> ( ( f ` b ) R ( f ` suc b ) <-> ( g ` b ) R ( g ` suc b ) ) )
47 46 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 ) ) )
48 38 43 47 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 ) ) ) )
49 48 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 ) ) )
50 37 49 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 ) ) ) )
51 50 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 ) ) )
52 51 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 ) ) )
53 eqeq2 
 |-  ( y = z -> ( ( g ` suc i ) = y <-> ( g ` suc i ) = z ) )
54 53 anbi2d 
 |-  ( y = z -> ( ( ( g ` (/) ) = x /\ ( g ` suc i ) = y ) <-> ( ( g ` (/) ) = x /\ ( g ` suc i ) = z ) ) )
55 54 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 ) ) ) )
56 55 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 ) ) ) )
57 breq2 
 |-  ( y = z -> ( x S y <-> x S z ) )
58 56 57 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 ) ) )
59 58 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 ) )
60 52 59 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 ) ) )
61 60 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 ) ) ) )
62 suceq 
 |-  ( m = suc i -> suc m = suc suc i )
63 62 suceqd 
 |-  ( m = suc i -> suc suc m = suc suc suc i )
64 63 fneq2d 
 |-  ( m = suc i -> ( f Fn suc suc m <-> f Fn suc suc suc i ) )
65 62 fveqeq2d 
 |-  ( m = suc i -> ( ( f ` suc m ) = y <-> ( f ` suc suc i ) = y ) )
66 65 anbi2d 
 |-  ( m = suc i -> ( ( ( f ` (/) ) = x /\ ( f ` suc m ) = y ) <-> ( ( f ` (/) ) = x /\ ( f ` suc suc i ) = y ) ) )
67 62 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 ) ) )
68 64 66 67 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 ) ) ) )
69 68 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 ) ) ) )
70 69 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 ) ) )
71 70 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 ) ) )
72 71 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 ) ) ) )
73 suceq 
 |-  ( m = n -> suc m = suc n )
74 73 suceqd 
 |-  ( m = n -> suc suc m = suc suc n )
75 74 fneq2d 
 |-  ( m = n -> ( f Fn suc suc m <-> f Fn suc suc n ) )
76 73 fveqeq2d 
 |-  ( m = n -> ( ( f ` suc m ) = y <-> ( f ` suc n ) = y ) )
77 76 anbi2d 
 |-  ( m = n -> ( ( ( f ` (/) ) = x /\ ( f ` suc m ) = y ) <-> ( ( f ` (/) ) = x /\ ( f ` suc n ) = y ) ) )
78 73 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 ) ) )
79 75 77 78 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 ) ) ) )
80 79 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 ) ) ) )
81 80 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 ) ) )
82 81 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 ) ) )
83 82 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 ) ) ) )
84 breq12 
 |-  ( ( ( f ` (/) ) = x /\ ( f ` 1o ) = y ) -> ( ( f ` (/) ) R ( f ` 1o ) <-> x R y ) )
85 84 biimpa 
 |-  ( ( ( ( f ` (/) ) = x /\ ( f ` 1o ) = y ) /\ ( f ` (/) ) R ( f ` 1o ) ) -> x R y )
86 85 3adant1 
 |-  ( ( f Fn suc suc (/) /\ ( ( f ` (/) ) = x /\ ( f ` 1o ) = y ) /\ ( f ` (/) ) R ( f ` 1o ) ) -> x R y )
87 ssbr 
 |-  ( R C_ S -> ( x R y -> x S y ) )
88 87 adantr 
 |-  ( ( R C_ S /\ ( S o. S ) C_ S ) -> ( x R y -> x S y ) )
89 86 88 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 ) )
90 89 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 ) )
91 90 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 ) )
92 fvex 
 |-  ( f ` suc i ) e. _V
93 eqeq2 
 |-  ( z = ( f ` suc i ) -> ( ( g ` suc i ) = z <-> ( g ` suc i ) = ( f ` suc i ) ) )
94 93 anbi2d 
 |-  ( z = ( f ` suc i ) -> ( ( ( g ` (/) ) = x /\ ( g ` suc i ) = z ) <-> ( ( g ` (/) ) = x /\ ( g ` suc i ) = ( f ` suc i ) ) ) )
95 94 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 ) ) ) )
96 95 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 ) ) ) )
97 breq2 
 |-  ( z = ( f ` suc i ) -> ( x S z <-> x S ( f ` suc i ) ) )
98 96 97 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 ) ) ) )
99 92 98 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 ) ) )
100 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 )
101 sssucid 
 |-  suc suc i C_ suc suc suc i
102 fnssres 
 |-  ( ( f Fn suc suc suc i /\ suc suc i C_ suc suc suc i ) -> ( f |` suc suc i ) Fn suc suc i )
103 100 101 102 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 )
104 peano2 
 |-  ( i e. _om -> suc i e. _om )
105 104 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 )
106 nnord 
 |-  ( suc i e. _om -> Ord suc i )
107 0elsuc 
 |-  ( Ord suc i -> (/) e. suc suc i )
108 105 106 107 3syl 
 |-  ( ( ( 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 )
109 108 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 ` (/) ) )
110 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 )
111 109 110 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 )
112 vex 
 |-  i e. _V
113 112 sucex 
 |-  suc i e. _V
114 113 sucid 
 |-  suc i e. suc suc i
115 fvres 
 |-  ( suc i e. suc suc i -> ( ( f |` suc suc i ) ` suc i ) = ( f ` suc i ) )
116 114 115 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 ) )
117 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 ) )
118 elelsuc 
 |-  ( b e. suc i -> b e. suc suc i )
119 118 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 )
120 33 117 119 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 ) )
121 119 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 ) )
122 ordsucelsuc 
 |-  ( Ord suc i -> ( b e. suc i <-> suc b e. suc suc i ) )
123 105 106 122 3syl 
 |-  ( ( ( 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 ) )
124 123 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 )
125 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 ) ` suc b ) = ( f ` suc b ) )
126 120 121 125 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 ) )
127 126 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 ) )
128 vex 
 |-  f e. _V
129 128 resex 
 |-  ( f |` suc suc i ) e. _V
130 fneq1 
 |-  ( g = ( f |` suc suc i ) -> ( g Fn suc suc i <-> ( f |` suc suc i ) Fn suc suc i ) )
131 fveq1 
 |-  ( g = ( f |` suc suc i ) -> ( g ` (/) ) = ( ( f |` suc suc i ) ` (/) ) )
132 131 eqeq1d 
 |-  ( g = ( f |` suc suc i ) -> ( ( g ` (/) ) = x <-> ( ( f |` suc suc i ) ` (/) ) = x ) )
133 fveq1 
 |-  ( g = ( f |` suc suc i ) -> ( g ` suc i ) = ( ( f |` suc suc i ) ` suc i ) )
134 133 eqeq1d 
 |-  ( g = ( f |` suc suc i ) -> ( ( g ` suc i ) = ( f ` suc i ) <-> ( ( f |` suc suc i ) ` suc i ) = ( f ` suc i ) ) )
135 132 134 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 ) ) ) )
136 fveq1 
 |-  ( g = ( f |` suc suc i ) -> ( g ` b ) = ( ( f |` suc suc i ) ` b ) )
137 fveq1 
 |-  ( g = ( f |` suc suc i ) -> ( g ` suc b ) = ( ( f |` suc suc i ) ` suc b ) )
138 136 137 breq12d 
 |-  ( g = ( f |` suc suc i ) -> ( ( g ` b ) R ( g ` suc b ) <-> ( ( f |` suc suc i ) ` b ) R ( ( f |` suc suc i ) ` suc b ) ) )
139 138 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 ) ) )
140 130 135 139 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 ) ) ) )
141 129 140 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 ) ) )
142 103 111 116 127 141 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 ) ) )
143 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 )
144 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 ) )
145 ssbr 
 |-  ( R C_ S -> ( ( f ` a ) R ( f ` suc a ) -> ( f ` a ) S ( f ` suc a ) ) )
146 145 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 ) ) )
147 143 144 146 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 ) )
148 fveq2 
 |-  ( a = suc i -> ( f ` a ) = ( f ` suc i ) )
149 suceq 
 |-  ( a = suc i -> suc a = suc suc i )
150 149 fveq2d 
 |-  ( a = suc i -> ( f ` suc a ) = ( f ` suc suc i ) )
151 148 150 breq12d 
 |-  ( a = suc i -> ( ( f ` a ) S ( f ` suc a ) <-> ( f ` suc i ) S ( f ` suc suc i ) ) )
152 151 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 ) ) )
153 114 147 152 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 ) )
154 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 )
155 153 154 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 )
156 vex 
 |-  x e. _V
157 vex 
 |-  y e. _V
158 156 92 157 brcoi 
 |-  ( ( x S ( f ` suc i ) /\ ( f ` suc i ) S y ) -> x ( S o. S ) y )
159 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 )
160 159 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 ) )
161 158 160 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 ) )
162 155 161 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 ) )
163 142 162 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 ) )
164 163 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 ) ) )
165 164 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 ) ) )
166 99 165 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 ) ) )
167 166 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 ) )
168 167 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 ) )
169 168 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 ) )
170 169 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 ) ) ) )
171 170 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 ) ) ) )
172 23 61 72 83 91 171 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 ) ) )
173 172 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 ) ) )
174 173 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 ) )
175 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 ) )
176 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 ) )
177 176 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 ) )
178 175 177 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 ) )
179 174 178 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 ) )
180 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 ) ) )
181 df-br 
 |-  ( x t++ R y <-> <. x , y >. e. t++ R )
182 180 181 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 )
183 df-br 
 |-  ( x S y <-> <. x , y >. e. S )
184 182 183 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 ) )
185 184 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 ) )
186 179 185 sylib 
 |-  ( ( R C_ S /\ ( S o. S ) C_ S ) -> A. y ( <. x , y >. e. t++ R -> <. x , y >. e. S ) )
187 186 alrimiv 
 |-  ( ( R C_ S /\ ( S o. S ) C_ S ) -> A. x A. y ( <. x , y >. e. t++ R -> <. x , y >. e. S ) )
188 relttrcl 
 |-  Rel t++ R
189 ssrel 
 |-  ( Rel t++ R -> ( t++ R C_ S <-> A. x A. y ( <. x , y >. e. t++ R -> <. x , y >. e. S ) ) )
190 188 189 ax-mp 
 |-  ( t++ R C_ S <-> A. x A. y ( <. x , y >. e. t++ R -> <. x , y >. e. S ) )
191 187 190 sylibr 
 |-  ( ( R C_ S /\ ( S o. S ) C_ S ) -> t++ R C_ S )