Metamath Proof Explorer

Theorem ttrcltr

Description: The transitive closure of a class is transitive. (Contributed by Scott Fenton, 17-Oct-2024)

Ref Expression
Assertion ttrcltr 
|- ( t++ R o. t++ R ) C_ t++ R

Proof

Step Hyp Ref Expression
1 relco 
 |-  Rel ( t++ R o. t++ R )
2 eldifi 
 |-  ( n e. ( _om \ 1o ) -> n e. _om )
3 eldifi 
 |-  ( m e. ( _om \ 1o ) -> m e. _om )
4 nnacl 
 |-  ( ( n e. _om /\ m e. _om ) -> ( n +o m ) e. _om )
5 2 3 4 syl2an 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( n +o m ) e. _om )
6 eldif 
 |-  ( n e. ( _om \ 1o ) <-> ( n e. _om /\ -. n e. 1o ) )
7 1on 
 |-  1o e. On
8 7 onordi 
 |-  Ord 1o
9 nnord 
 |-  ( n e. _om -> Ord n )
10 ordtri1 
 |-  ( ( Ord 1o /\ Ord n ) -> ( 1o C_ n <-> -. n e. 1o ) )
11 8 9 10 sylancr 
 |-  ( n e. _om -> ( 1o C_ n <-> -. n e. 1o ) )
12 11 biimpar 
 |-  ( ( n e. _om /\ -. n e. 1o ) -> 1o C_ n )
13 6 12 sylbi 
 |-  ( n e. ( _om \ 1o ) -> 1o C_ n )
14 13 adantr 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> 1o C_ n )
15 nnaword1 
 |-  ( ( n e. _om /\ m e. _om ) -> n C_ ( n +o m ) )
16 2 3 15 syl2an 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> n C_ ( n +o m ) )
17 14 16 sstrd 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> 1o C_ ( n +o m ) )
18 nnord 
 |-  ( ( n +o m ) e. _om -> Ord ( n +o m ) )
19 5 18 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> Ord ( n +o m ) )
20 ordtri1 
 |-  ( ( Ord 1o /\ Ord ( n +o m ) ) -> ( 1o C_ ( n +o m ) <-> -. ( n +o m ) e. 1o ) )
21 8 19 20 sylancr 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( 1o C_ ( n +o m ) <-> -. ( n +o m ) e. 1o ) )
22 17 21 mpbid 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> -. ( n +o m ) e. 1o )
23 5 22 eldifd 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( n +o m ) e. ( _om \ 1o ) )
24 0elsuc 
 |-  ( Ord ( n +o m ) -> (/) e. suc ( n +o m ) )
25 19 24 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> (/) e. suc ( n +o m ) )
26 eleq1 
 |-  ( p = (/) -> ( p e. suc n <-> (/) e. suc n ) )
27 fveq2 
 |-  ( p = (/) -> ( f ` p ) = ( f ` (/) ) )
28 eqeq2 
 |-  ( p = (/) -> ( ( n +o q ) = p <-> ( n +o q ) = (/) ) )
29 28 riotabidv 
 |-  ( p = (/) -> ( iota_ q e. _om ( n +o q ) = p ) = ( iota_ q e. _om ( n +o q ) = (/) ) )
30 29 fveq2d 
 |-  ( p = (/) -> ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) = ( g ` ( iota_ q e. _om ( n +o q ) = (/) ) ) )
31 26 27 30 ifbieq12d 
 |-  ( p = (/) -> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) = if ( (/) e. suc n , ( f ` (/) ) , ( g ` ( iota_ q e. _om ( n +o q ) = (/) ) ) ) )
32 eqid 
 |-  ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) = ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) )
33 fvex 
 |-  ( f ` (/) ) e. _V
34 fvex 
 |-  ( g ` ( iota_ q e. _om ( n +o q ) = (/) ) ) e. _V
35 33 34 ifex 
 |-  if ( (/) e. suc n , ( f ` (/) ) , ( g ` ( iota_ q e. _om ( n +o q ) = (/) ) ) ) e. _V
36 31 32 35 fvmpt 
 |-  ( (/) e. suc ( n +o m ) -> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` (/) ) = if ( (/) e. suc n , ( f ` (/) ) , ( g ` ( iota_ q e. _om ( n +o q ) = (/) ) ) ) )
37 25 36 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` (/) ) = if ( (/) e. suc n , ( f ` (/) ) , ( g ` ( iota_ q e. _om ( n +o q ) = (/) ) ) ) )
38 2 adantr 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> n e. _om )
39 38 9 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> Ord n )
40 0elsuc 
 |-  ( Ord n -> (/) e. suc n )
41 39 40 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> (/) e. suc n )
42 41 iftrued 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> if ( (/) e. suc n , ( f ` (/) ) , ( g ` ( iota_ q e. _om ( n +o q ) = (/) ) ) ) = ( f ` (/) ) )
43 37 42 eqtrd 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` (/) ) = ( f ` (/) ) )
44 simpl2l 
 |-  ( ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) -> ( f ` (/) ) = x )
45 43 44 sylan9eq 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` (/) ) = x )
46 ovex 
 |-  ( n +o m ) e. _V
47 46 sucid 
 |-  ( n +o m ) e. suc ( n +o m )
48 eleq1 
 |-  ( p = ( n +o m ) -> ( p e. suc n <-> ( n +o m ) e. suc n ) )
49 fveq2 
 |-  ( p = ( n +o m ) -> ( f ` p ) = ( f ` ( n +o m ) ) )
50 eqeq2 
 |-  ( p = ( n +o m ) -> ( ( n +o q ) = p <-> ( n +o q ) = ( n +o m ) ) )
51 50 riotabidv 
 |-  ( p = ( n +o m ) -> ( iota_ q e. _om ( n +o q ) = p ) = ( iota_ q e. _om ( n +o q ) = ( n +o m ) ) )
52 51 fveq2d 
 |-  ( p = ( n +o m ) -> ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) = ( g ` ( iota_ q e. _om ( n +o q ) = ( n +o m ) ) ) )
53 48 49 52 ifbieq12d 
 |-  ( p = ( n +o m ) -> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) = if ( ( n +o m ) e. suc n , ( f ` ( n +o m ) ) , ( g ` ( iota_ q e. _om ( n +o q ) = ( n +o m ) ) ) ) )
54 fvex 
 |-  ( f ` ( n +o m ) ) e. _V
55 fvex 
 |-  ( g ` ( iota_ q e. _om ( n +o q ) = ( n +o m ) ) ) e. _V
56 54 55 ifex 
 |-  if ( ( n +o m ) e. suc n , ( f ` ( n +o m ) ) , ( g ` ( iota_ q e. _om ( n +o q ) = ( n +o m ) ) ) ) e. _V
57 53 32 56 fvmpt 
 |-  ( ( n +o m ) e. suc ( n +o m ) -> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` ( n +o m ) ) = if ( ( n +o m ) e. suc n , ( f ` ( n +o m ) ) , ( g ` ( iota_ q e. _om ( n +o q ) = ( n +o m ) ) ) ) )
58 47 57 mp1i 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` ( n +o m ) ) = if ( ( n +o m ) e. suc n , ( f ` ( n +o m ) ) , ( g ` ( iota_ q e. _om ( n +o q ) = ( n +o m ) ) ) ) )
59 df-1o 
 |-  1o = suc (/)
60 59 difeq2i 
 |-  ( _om \ 1o ) = ( _om \ suc (/) )
61 60 eleq2i 
 |-  ( n e. ( _om \ 1o ) <-> n e. ( _om \ suc (/) ) )
62 peano1 
 |-  (/) e. _om
63 eldifsucnn 
 |-  ( (/) e. _om -> ( n e. ( _om \ suc (/) ) <-> E. x e. ( _om \ (/) ) n = suc x ) )
64 62 63 ax-mp 
 |-  ( n e. ( _om \ suc (/) ) <-> E. x e. ( _om \ (/) ) n = suc x )
65 dif0 
 |-  ( _om \ (/) ) = _om
66 65 rexeqi 
 |-  ( E. x e. ( _om \ (/) ) n = suc x <-> E. x e. _om n = suc x )
67 61 64 66 3bitri 
 |-  ( n e. ( _om \ 1o ) <-> E. x e. _om n = suc x )
68 60 eleq2i 
 |-  ( m e. ( _om \ 1o ) <-> m e. ( _om \ suc (/) ) )
69 eldifsucnn 
 |-  ( (/) e. _om -> ( m e. ( _om \ suc (/) ) <-> E. y e. ( _om \ (/) ) m = suc y ) )
70 62 69 ax-mp 
 |-  ( m e. ( _om \ suc (/) ) <-> E. y e. ( _om \ (/) ) m = suc y )
71 65 rexeqi 
 |-  ( E. y e. ( _om \ (/) ) m = suc y <-> E. y e. _om m = suc y )
72 68 70 71 3bitri 
 |-  ( m e. ( _om \ 1o ) <-> E. y e. _om m = suc y )
73 67 72 anbi12i 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) <-> ( E. x e. _om n = suc x /\ E. y e. _om m = suc y ) )
74 reeanv 
 |-  ( E. x e. _om E. y e. _om ( n = suc x /\ m = suc y ) <-> ( E. x e. _om n = suc x /\ E. y e. _om m = suc y ) )
75 73 74 bitr4i 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) <-> E. x e. _om E. y e. _om ( n = suc x /\ m = suc y ) )
76 peano2 
 |-  ( x e. _om -> suc x e. _om )
77 nnaword1 
 |-  ( ( suc x e. _om /\ y e. _om ) -> suc x C_ ( suc x +o y ) )
78 76 77 sylan 
 |-  ( ( x e. _om /\ y e. _om ) -> suc x C_ ( suc x +o y ) )
79 76 adantr 
 |-  ( ( x e. _om /\ y e. _om ) -> suc x e. _om )
80 nnord 
 |-  ( suc x e. _om -> Ord suc x )
81 79 80 syl 
 |-  ( ( x e. _om /\ y e. _om ) -> Ord suc x )
82 nnacl 
 |-  ( ( suc x e. _om /\ y e. _om ) -> ( suc x +o y ) e. _om )
83 76 82 sylan 
 |-  ( ( x e. _om /\ y e. _om ) -> ( suc x +o y ) e. _om )
84 nnord 
 |-  ( ( suc x +o y ) e. _om -> Ord ( suc x +o y ) )
85 83 84 syl 
 |-  ( ( x e. _om /\ y e. _om ) -> Ord ( suc x +o y ) )
86 ordsucsssuc 
 |-  ( ( Ord suc x /\ Ord ( suc x +o y ) ) -> ( suc x C_ ( suc x +o y ) <-> suc suc x C_ suc ( suc x +o y ) ) )
87 81 85 86 syl2anc 
 |-  ( ( x e. _om /\ y e. _om ) -> ( suc x C_ ( suc x +o y ) <-> suc suc x C_ suc ( suc x +o y ) ) )
88 78 87 mpbid 
 |-  ( ( x e. _om /\ y e. _om ) -> suc suc x C_ suc ( suc x +o y ) )
89 nnasuc 
 |-  ( ( suc x e. _om /\ y e. _om ) -> ( suc x +o suc y ) = suc ( suc x +o y ) )
90 76 89 sylan 
 |-  ( ( x e. _om /\ y e. _om ) -> ( suc x +o suc y ) = suc ( suc x +o y ) )
91 88 90 sseqtrrd 
 |-  ( ( x e. _om /\ y e. _om ) -> suc suc x C_ ( suc x +o suc y ) )
92 peano2 
 |-  ( suc x e. _om -> suc suc x e. _om )
93 79 92 syl 
 |-  ( ( x e. _om /\ y e. _om ) -> suc suc x e. _om )
94 nnord 
 |-  ( suc suc x e. _om -> Ord suc suc x )
95 93 94 syl 
 |-  ( ( x e. _om /\ y e. _om ) -> Ord suc suc x )
96 peano2 
 |-  ( y e. _om -> suc y e. _om )
97 nnacl 
 |-  ( ( suc x e. _om /\ suc y e. _om ) -> ( suc x +o suc y ) e. _om )
98 76 96 97 syl2an 
 |-  ( ( x e. _om /\ y e. _om ) -> ( suc x +o suc y ) e. _om )
99 nnord 
 |-  ( ( suc x +o suc y ) e. _om -> Ord ( suc x +o suc y ) )
100 98 99 syl 
 |-  ( ( x e. _om /\ y e. _om ) -> Ord ( suc x +o suc y ) )
101 ordtri1 
 |-  ( ( Ord suc suc x /\ Ord ( suc x +o suc y ) ) -> ( suc suc x C_ ( suc x +o suc y ) <-> -. ( suc x +o suc y ) e. suc suc x ) )
102 95 100 101 syl2anc 
 |-  ( ( x e. _om /\ y e. _om ) -> ( suc suc x C_ ( suc x +o suc y ) <-> -. ( suc x +o suc y ) e. suc suc x ) )
103 91 102 mpbid 
 |-  ( ( x e. _om /\ y e. _om ) -> -. ( suc x +o suc y ) e. suc suc x )
104 oveq12 
 |-  ( ( n = suc x /\ m = suc y ) -> ( n +o m ) = ( suc x +o suc y ) )
105 suceq 
 |-  ( n = suc x -> suc n = suc suc x )
106 105 adantr 
 |-  ( ( n = suc x /\ m = suc y ) -> suc n = suc suc x )
107 104 106 eleq12d 
 |-  ( ( n = suc x /\ m = suc y ) -> ( ( n +o m ) e. suc n <-> ( suc x +o suc y ) e. suc suc x ) )
108 107 notbid 
 |-  ( ( n = suc x /\ m = suc y ) -> ( -. ( n +o m ) e. suc n <-> -. ( suc x +o suc y ) e. suc suc x ) )
109 103 108 syl5ibrcom 
 |-  ( ( x e. _om /\ y e. _om ) -> ( ( n = suc x /\ m = suc y ) -> -. ( n +o m ) e. suc n ) )
110 109 rexlimivv 
 |-  ( E. x e. _om E. y e. _om ( n = suc x /\ m = suc y ) -> -. ( n +o m ) e. suc n )
111 75 110 sylbi 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> -. ( n +o m ) e. suc n )
112 111 iffalsed 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> if ( ( n +o m ) e. suc n , ( f ` ( n +o m ) ) , ( g ` ( iota_ q e. _om ( n +o q ) = ( n +o m ) ) ) ) = ( g ` ( iota_ q e. _om ( n +o q ) = ( n +o m ) ) ) )
113 3 adantl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> m e. _om )
114 38 adantr 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ q e. _om ) -> n e. _om )
115 simpr 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ q e. _om ) -> q e. _om )
116 113 adantr 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ q e. _om ) -> m e. _om )
117 nnacan 
 |-  ( ( n e. _om /\ q e. _om /\ m e. _om ) -> ( ( n +o q ) = ( n +o m ) <-> q = m ) )
118 114 115 116 117 syl3anc 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ q e. _om ) -> ( ( n +o q ) = ( n +o m ) <-> q = m ) )
119 113 118 riota5 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( iota_ q e. _om ( n +o q ) = ( n +o m ) ) = m )
120 119 fveq2d 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( g ` ( iota_ q e. _om ( n +o q ) = ( n +o m ) ) ) = ( g ` m ) )
121 58 112 120 3eqtrd 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` ( n +o m ) ) = ( g ` m ) )
122 simpr2r 
 |-  ( ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) -> ( g ` m ) = y )
123 121 122 sylan9eq 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` ( n +o m ) ) = y )
124 simprl3 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> A. a e. n ( f ` a ) R ( f ` suc a ) )
125 fveq2 
 |-  ( a = c -> ( f ` a ) = ( f ` c ) )
126 suceq 
 |-  ( a = c -> suc a = suc c )
127 126 fveq2d 
 |-  ( a = c -> ( f ` suc a ) = ( f ` suc c ) )
128 125 127 breq12d 
 |-  ( a = c -> ( ( f ` a ) R ( f ` suc a ) <-> ( f ` c ) R ( f ` suc c ) ) )
129 128 rspcv 
 |-  ( c e. n -> ( A. a e. n ( f ` a ) R ( f ` suc a ) -> ( f ` c ) R ( f ` suc c ) ) )
130 124 129 mpan9 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. n ) -> ( f ` c ) R ( f ` suc c ) )
131 elelsuc 
 |-  ( c e. n -> c e. suc n )
132 131 adantl 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. n ) -> c e. suc n )
133 132 iftrued 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. n ) -> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) = ( f ` c ) )
134 ordsucelsuc 
 |-  ( Ord n -> ( c e. n <-> suc c e. suc n ) )
135 39 134 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( c e. n <-> suc c e. suc n ) )
136 135 adantr 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> ( c e. n <-> suc c e. suc n ) )
137 136 biimpa 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. n ) -> suc c e. suc n )
138 137 iftrued 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. n ) -> if ( suc c e. suc n , ( f ` suc c ) , ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) = ( f ` suc c ) )
139 130 133 138 3brtr4d 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. n ) -> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) R if ( suc c e. suc n , ( f ` suc c ) , ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) )
140 139 adantlr 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ c e. n ) -> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) R if ( suc c e. suc n , ( f ` suc c ) , ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) )
141 39 adantr 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> Ord n )
142 5 adantr 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> ( n +o m ) e. _om )
143 elnn 
 |-  ( ( c e. ( n +o m ) /\ ( n +o m ) e. _om ) -> c e. _om )
144 143 ancoms 
 |-  ( ( ( n +o m ) e. _om /\ c e. ( n +o m ) ) -> c e. _om )
145 142 144 sylan 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> c e. _om )
146 nnord 
 |-  ( c e. _om -> Ord c )
147 145 146 syl 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> Ord c )
148 ordtri3or 
 |-  ( ( Ord n /\ Ord c ) -> ( n e. c \/ n = c \/ c e. n ) )
149 141 147 148 syl2an2r 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> ( n e. c \/ n = c \/ c e. n ) )
150 3orel3 
 |-  ( -. c e. n -> ( ( n e. c \/ n = c \/ c e. n ) -> ( n e. c \/ n = c ) ) )
151 149 150 syl5com 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> ( -. c e. n -> ( n e. c \/ n = c ) ) )
152 fveq2 
 |-  ( b = ( iota_ q e. _om ( n +o q ) = c ) -> ( g ` b ) = ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) )
153 suceq 
 |-  ( b = ( iota_ q e. _om ( n +o q ) = c ) -> suc b = suc ( iota_ q e. _om ( n +o q ) = c ) )
154 153 fveq2d 
 |-  ( b = ( iota_ q e. _om ( n +o q ) = c ) -> ( g ` suc b ) = ( g ` suc ( iota_ q e. _om ( n +o q ) = c ) ) )
155 152 154 breq12d 
 |-  ( b = ( iota_ q e. _om ( n +o q ) = c ) -> ( ( g ` b ) R ( g ` suc b ) <-> ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) R ( g ` suc ( iota_ q e. _om ( n +o q ) = c ) ) ) )
156 simprr3 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> A. b e. m ( g ` b ) R ( g ` suc b ) )
157 156 adantr 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> A. b e. m ( g ` b ) R ( g ` suc b ) )
158 157 adantr 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> A. b e. m ( g ` b ) R ( g ` suc b ) )
159 ordelss 
 |-  ( ( Ord c /\ n e. c ) -> n C_ c )
160 147 159 sylan 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> n C_ c )
161 38 adantr 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> n e. _om )
162 161 adantr 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> n e. _om )
163 145 adantr 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> c e. _om )
164 nnawordex 
 |-  ( ( n e. _om /\ c e. _om ) -> ( n C_ c <-> E. q e. _om ( n +o q ) = c ) )
165 162 163 164 syl2an2r 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( n C_ c <-> E. q e. _om ( n +o q ) = c ) )
166 160 165 mpbid 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> E. q e. _om ( n +o q ) = c )
167 oveq2 
 |-  ( q = p -> ( n +o q ) = ( n +o p ) )
168 167 eqeq1d 
 |-  ( q = p -> ( ( n +o q ) = c <-> ( n +o p ) = c ) )
169 168 cbvrexvw 
 |-  ( E. q e. _om ( n +o q ) = c <-> E. p e. _om ( n +o p ) = c )
170 166 169 sylib 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> E. p e. _om ( n +o p ) = c )
171 simprr 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ ( p e. _om /\ ( n +o p ) = c ) ) -> ( n +o p ) = c )
172 simpllr 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ ( p e. _om /\ ( n +o p ) = c ) ) -> c e. ( n +o m ) )
173 171 172 eqeltrd 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ ( p e. _om /\ ( n +o p ) = c ) ) -> ( n +o p ) e. ( n +o m ) )
174 simprl 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ ( p e. _om /\ ( n +o p ) = c ) ) -> p e. _om )
175 3 ad4antlr 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> m e. _om )
176 175 adantr 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ ( p e. _om /\ ( n +o p ) = c ) ) -> m e. _om )
177 162 adantr 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> n e. _om )
178 177 adantr 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ ( p e. _om /\ ( n +o p ) = c ) ) -> n e. _om )
179 nnaord 
 |-  ( ( p e. _om /\ m e. _om /\ n e. _om ) -> ( p e. m <-> ( n +o p ) e. ( n +o m ) ) )
180 174 176 178 179 syl3anc 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ ( p e. _om /\ ( n +o p ) = c ) ) -> ( p e. m <-> ( n +o p ) e. ( n +o m ) ) )
181 173 180 mpbird 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ ( p e. _om /\ ( n +o p ) = c ) ) -> p e. m )
182 170 181 171 reximssdv 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> E. p e. m ( n +o p ) = c )
183 elnn 
 |-  ( ( p e. m /\ m e. _om ) -> p e. _om )
184 183 ancoms 
 |-  ( ( m e. _om /\ p e. m ) -> p e. _om )
185 175 184 sylan 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ p e. m ) -> p e. _om )
186 nnasmo 
 |-  ( n e. _om -> E* q e. _om ( n +o q ) = c )
187 177 186 syl 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> E* q e. _om ( n +o q ) = c )
188 reu5 
 |-  ( E! q e. _om ( n +o q ) = c <-> ( E. q e. _om ( n +o q ) = c /\ E* q e. _om ( n +o q ) = c ) )
189 166 187 188 sylanbrc 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> E! q e. _om ( n +o q ) = c )
190 189 adantr 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ p e. m ) -> E! q e. _om ( n +o q ) = c )
191 168 riota2 
 |-  ( ( p e. _om /\ E! q e. _om ( n +o q ) = c ) -> ( ( n +o p ) = c <-> ( iota_ q e. _om ( n +o q ) = c ) = p ) )
192 185 190 191 syl2anc 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ p e. m ) -> ( ( n +o p ) = c <-> ( iota_ q e. _om ( n +o q ) = c ) = p ) )
193 eqcom 
 |-  ( ( iota_ q e. _om ( n +o q ) = c ) = p <-> p = ( iota_ q e. _om ( n +o q ) = c ) )
194 192 193 bitrdi 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ p e. m ) -> ( ( n +o p ) = c <-> p = ( iota_ q e. _om ( n +o q ) = c ) ) )
195 194 rexbidva 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( E. p e. m ( n +o p ) = c <-> E. p e. m p = ( iota_ q e. _om ( n +o q ) = c ) ) )
196 182 195 mpbid 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> E. p e. m p = ( iota_ q e. _om ( n +o q ) = c ) )
197 risset 
 |-  ( ( iota_ q e. _om ( n +o q ) = c ) e. m <-> E. p e. m p = ( iota_ q e. _om ( n +o q ) = c ) )
198 196 197 sylibr 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( iota_ q e. _om ( n +o q ) = c ) e. m )
199 155 158 198 rspcdva 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) R ( g ` suc ( iota_ q e. _om ( n +o q ) = c ) ) )
200 simpr 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> n e. c )
201 vex 
 |-  n e. _V
202 147 adantr 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> Ord c )
203 ordelsuc 
 |-  ( ( n e. _V /\ Ord c ) -> ( n e. c <-> suc n C_ c ) )
204 201 202 203 sylancr 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( n e. c <-> suc n C_ c ) )
205 peano2 
 |-  ( n e. _om -> suc n e. _om )
206 38 205 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> suc n e. _om )
207 nnord 
 |-  ( suc n e. _om -> Ord suc n )
208 206 207 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> Ord suc n )
209 208 adantr 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> Ord suc n )
210 209 adantr 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> Ord suc n )
211 ordtri1 
 |-  ( ( Ord suc n /\ Ord c ) -> ( suc n C_ c <-> -. c e. suc n ) )
212 210 202 211 syl2an2r 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( suc n C_ c <-> -. c e. suc n ) )
213 204 212 bitrd 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( n e. c <-> -. c e. suc n ) )
214 200 213 mpbid 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> -. c e. suc n )
215 214 iffalsed 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) = ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) )
216 riotacl 
 |-  ( E! q e. _om ( n +o q ) = c -> ( iota_ q e. _om ( n +o q ) = c ) e. _om )
217 189 216 syl 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( iota_ q e. _om ( n +o q ) = c ) e. _om )
218 nnasuc 
 |-  ( ( n e. _om /\ ( iota_ q e. _om ( n +o q ) = c ) e. _om ) -> ( n +o suc ( iota_ q e. _om ( n +o q ) = c ) ) = suc ( n +o ( iota_ q e. _om ( n +o q ) = c ) ) )
219 162 217 218 syl2an2r 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( n +o suc ( iota_ q e. _om ( n +o q ) = c ) ) = suc ( n +o ( iota_ q e. _om ( n +o q ) = c ) ) )
220 eqidd 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( iota_ q e. _om ( n +o q ) = c ) = ( iota_ q e. _om ( n +o q ) = c ) )
221 nfriota1 
 |-  F/_ q ( iota_ q e. _om ( n +o q ) = c )
222 nfcv 
 |-  F/_ q n
223 nfcv 
 |-  F/_ q +o
224 222 223 221 nfov 
 |-  F/_ q ( n +o ( iota_ q e. _om ( n +o q ) = c ) )
225 224 nfeq1 
 |-  F/ q ( n +o ( iota_ q e. _om ( n +o q ) = c ) ) = c
226 oveq2 
 |-  ( q = ( iota_ q e. _om ( n +o q ) = c ) -> ( n +o q ) = ( n +o ( iota_ q e. _om ( n +o q ) = c ) ) )
227 226 eqeq1d 
 |-  ( q = ( iota_ q e. _om ( n +o q ) = c ) -> ( ( n +o q ) = c <-> ( n +o ( iota_ q e. _om ( n +o q ) = c ) ) = c ) )
228 221 225 227 riota2f 
 |-  ( ( ( iota_ q e. _om ( n +o q ) = c ) e. _om /\ E! q e. _om ( n +o q ) = c ) -> ( ( n +o ( iota_ q e. _om ( n +o q ) = c ) ) = c <-> ( iota_ q e. _om ( n +o q ) = c ) = ( iota_ q e. _om ( n +o q ) = c ) ) )
229 217 189 228 syl2anc 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( ( n +o ( iota_ q e. _om ( n +o q ) = c ) ) = c <-> ( iota_ q e. _om ( n +o q ) = c ) = ( iota_ q e. _om ( n +o q ) = c ) ) )
230 220 229 mpbird 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( n +o ( iota_ q e. _om ( n +o q ) = c ) ) = c )
231 suceq 
 |-  ( ( n +o ( iota_ q e. _om ( n +o q ) = c ) ) = c -> suc ( n +o ( iota_ q e. _om ( n +o q ) = c ) ) = suc c )
232 230 231 syl 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> suc ( n +o ( iota_ q e. _om ( n +o q ) = c ) ) = suc c )
233 219 232 eqtrd 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( n +o suc ( iota_ q e. _om ( n +o q ) = c ) ) = suc c )
234 peano2 
 |-  ( ( iota_ q e. _om ( n +o q ) = c ) e. _om -> suc ( iota_ q e. _om ( n +o q ) = c ) e. _om )
235 217 234 syl 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> suc ( iota_ q e. _om ( n +o q ) = c ) e. _om )
236 peano2 
 |-  ( p e. _om -> suc p e. _om )
237 nnasuc 
 |-  ( ( n e. _om /\ p e. _om ) -> ( n +o suc p ) = suc ( n +o p ) )
238 177 237 sylan 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ p e. _om ) -> ( n +o suc p ) = suc ( n +o p ) )
239 oveq2 
 |-  ( q = suc p -> ( n +o q ) = ( n +o suc p ) )
240 239 eqeq1d 
 |-  ( q = suc p -> ( ( n +o q ) = suc ( n +o p ) <-> ( n +o suc p ) = suc ( n +o p ) ) )
241 240 rspcev 
 |-  ( ( suc p e. _om /\ ( n +o suc p ) = suc ( n +o p ) ) -> E. q e. _om ( n +o q ) = suc ( n +o p ) )
242 236 238 241 syl2an2 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ p e. _om ) -> E. q e. _om ( n +o q ) = suc ( n +o p ) )
243 suceq 
 |-  ( ( n +o p ) = c -> suc ( n +o p ) = suc c )
244 243 eqeq2d 
 |-  ( ( n +o p ) = c -> ( ( n +o q ) = suc ( n +o p ) <-> ( n +o q ) = suc c ) )
245 244 rexbidv 
 |-  ( ( n +o p ) = c -> ( E. q e. _om ( n +o q ) = suc ( n +o p ) <-> E. q e. _om ( n +o q ) = suc c ) )
246 242 245 syl5ibcom 
 |-  ( ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) /\ p e. _om ) -> ( ( n +o p ) = c -> E. q e. _om ( n +o q ) = suc c ) )
247 246 rexlimdva 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( E. p e. _om ( n +o p ) = c -> E. q e. _om ( n +o q ) = suc c ) )
248 170 247 mpd 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> E. q e. _om ( n +o q ) = suc c )
249 nnasmo 
 |-  ( n e. _om -> E* q e. _om ( n +o q ) = suc c )
250 177 249 syl 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> E* q e. _om ( n +o q ) = suc c )
251 reu5 
 |-  ( E! q e. _om ( n +o q ) = suc c <-> ( E. q e. _om ( n +o q ) = suc c /\ E* q e. _om ( n +o q ) = suc c ) )
252 248 250 251 sylanbrc 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> E! q e. _om ( n +o q ) = suc c )
253 221 nfsuc 
 |-  F/_ q suc ( iota_ q e. _om ( n +o q ) = c )
254 222 223 253 nfov 
 |-  F/_ q ( n +o suc ( iota_ q e. _om ( n +o q ) = c ) )
255 254 nfeq1 
 |-  F/ q ( n +o suc ( iota_ q e. _om ( n +o q ) = c ) ) = suc c
256 oveq2 
 |-  ( q = suc ( iota_ q e. _om ( n +o q ) = c ) -> ( n +o q ) = ( n +o suc ( iota_ q e. _om ( n +o q ) = c ) ) )
257 256 eqeq1d 
 |-  ( q = suc ( iota_ q e. _om ( n +o q ) = c ) -> ( ( n +o q ) = suc c <-> ( n +o suc ( iota_ q e. _om ( n +o q ) = c ) ) = suc c ) )
258 253 255 257 riota2f 
 |-  ( ( suc ( iota_ q e. _om ( n +o q ) = c ) e. _om /\ E! q e. _om ( n +o q ) = suc c ) -> ( ( n +o suc ( iota_ q e. _om ( n +o q ) = c ) ) = suc c <-> ( iota_ q e. _om ( n +o q ) = suc c ) = suc ( iota_ q e. _om ( n +o q ) = c ) ) )
259 235 252 258 syl2anc 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( ( n +o suc ( iota_ q e. _om ( n +o q ) = c ) ) = suc c <-> ( iota_ q e. _om ( n +o q ) = suc c ) = suc ( iota_ q e. _om ( n +o q ) = c ) ) )
260 233 259 mpbid 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( iota_ q e. _om ( n +o q ) = suc c ) = suc ( iota_ q e. _om ( n +o q ) = c ) )
261 260 fveq2d 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) = ( g ` suc ( iota_ q e. _om ( n +o q ) = c ) ) )
262 199 215 261 3brtr4d 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ n e. c ) -> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) R ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) )
263 262 ex 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> ( n e. c -> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) R ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) )
264 fveq2 
 |-  ( b = (/) -> ( g ` b ) = ( g ` (/) ) )
265 suceq 
 |-  ( b = (/) -> suc b = suc (/) )
266 265 59 eqtr4di 
 |-  ( b = (/) -> suc b = 1o )
267 266 fveq2d 
 |-  ( b = (/) -> ( g ` suc b ) = ( g ` 1o ) )
268 264 267 breq12d 
 |-  ( b = (/) -> ( ( g ` b ) R ( g ` suc b ) <-> ( g ` (/) ) R ( g ` 1o ) ) )
269 eldif 
 |-  ( m e. ( _om \ 1o ) <-> ( m e. _om /\ -. m e. 1o ) )
270 nnord 
 |-  ( m e. _om -> Ord m )
271 ordtri1 
 |-  ( ( Ord 1o /\ Ord m ) -> ( 1o C_ m <-> -. m e. 1o ) )
272 8 270 271 sylancr 
 |-  ( m e. _om -> ( 1o C_ m <-> -. m e. 1o ) )
273 272 biimpar 
 |-  ( ( m e. _om /\ -. m e. 1o ) -> 1o C_ m )
274 269 273 sylbi 
 |-  ( m e. ( _om \ 1o ) -> 1o C_ m )
275 274 adantl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> 1o C_ m )
276 59 275 eqsstrrid 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> suc (/) C_ m )
277 0ex 
 |-  (/) e. _V
278 113 270 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> Ord m )
279 ordelsuc 
 |-  ( ( (/) e. _V /\ Ord m ) -> ( (/) e. m <-> suc (/) C_ m ) )
280 277 278 279 sylancr 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( (/) e. m <-> suc (/) C_ m ) )
281 276 280 mpbird 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> (/) e. m )
282 281 adantr 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> (/) e. m )
283 268 156 282 rspcdva 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> ( g ` (/) ) R ( g ` 1o ) )
284 simpl2r 
 |-  ( ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) -> ( f ` n ) = z )
285 simpr2l 
 |-  ( ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) -> ( g ` (/) ) = z )
286 284 285 eqtr4d 
 |-  ( ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) -> ( f ` n ) = ( g ` (/) ) )
287 286 adantl 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> ( f ` n ) = ( g ` (/) ) )
288 nnon 
 |-  ( n e. _om -> n e. On )
289 38 288 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> n e. On )
290 oa1suc 
 |-  ( n e. On -> ( n +o 1o ) = suc n )
291 289 290 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( n +o 1o ) = suc n )
292 1onn 
 |-  1o e. _om
293 oveq2 
 |-  ( q = 1o -> ( n +o q ) = ( n +o 1o ) )
294 293 eqeq1d 
 |-  ( q = 1o -> ( ( n +o q ) = suc n <-> ( n +o 1o ) = suc n ) )
295 294 rspcev 
 |-  ( ( 1o e. _om /\ ( n +o 1o ) = suc n ) -> E. q e. _om ( n +o q ) = suc n )
296 292 291 295 sylancr 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> E. q e. _om ( n +o q ) = suc n )
297 nnasmo 
 |-  ( n e. _om -> E* q e. _om ( n +o q ) = suc n )
298 38 297 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> E* q e. _om ( n +o q ) = suc n )
299 reu5 
 |-  ( E! q e. _om ( n +o q ) = suc n <-> ( E. q e. _om ( n +o q ) = suc n /\ E* q e. _om ( n +o q ) = suc n ) )
300 296 298 299 sylanbrc 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> E! q e. _om ( n +o q ) = suc n )
301 294 riota2 
 |-  ( ( 1o e. _om /\ E! q e. _om ( n +o q ) = suc n ) -> ( ( n +o 1o ) = suc n <-> ( iota_ q e. _om ( n +o q ) = suc n ) = 1o ) )
302 292 300 301 sylancr 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( ( n +o 1o ) = suc n <-> ( iota_ q e. _om ( n +o q ) = suc n ) = 1o ) )
303 291 302 mpbid 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( iota_ q e. _om ( n +o q ) = suc n ) = 1o )
304 303 adantr 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> ( iota_ q e. _om ( n +o q ) = suc n ) = 1o )
305 304 fveq2d 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> ( g ` ( iota_ q e. _om ( n +o q ) = suc n ) ) = ( g ` 1o ) )
306 283 287 305 3brtr4d 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> ( f ` n ) R ( g ` ( iota_ q e. _om ( n +o q ) = suc n ) ) )
307 201 sucid 
 |-  n e. suc n
308 307 iftruei 
 |-  if ( n e. suc n , ( f ` n ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) = ( f ` n )
309 eleq1 
 |-  ( n = c -> ( n e. suc n <-> c e. suc n ) )
310 fveq2 
 |-  ( n = c -> ( f ` n ) = ( f ` c ) )
311 309 310 ifbieq1d 
 |-  ( n = c -> if ( n e. suc n , ( f ` n ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) = if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) )
312 308 311 eqtr3id 
 |-  ( n = c -> ( f ` n ) = if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) )
313 suceq 
 |-  ( n = c -> suc n = suc c )
314 313 eqeq2d 
 |-  ( n = c -> ( ( n +o q ) = suc n <-> ( n +o q ) = suc c ) )
315 314 riotabidv 
 |-  ( n = c -> ( iota_ q e. _om ( n +o q ) = suc n ) = ( iota_ q e. _om ( n +o q ) = suc c ) )
316 315 fveq2d 
 |-  ( n = c -> ( g ` ( iota_ q e. _om ( n +o q ) = suc n ) ) = ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) )
317 312 316 breq12d 
 |-  ( n = c -> ( ( f ` n ) R ( g ` ( iota_ q e. _om ( n +o q ) = suc n ) ) <-> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) R ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) )
318 306 317 syl5ibcom 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> ( n = c -> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) R ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) )
319 318 adantr 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> ( n = c -> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) R ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) )
320 263 319 jaod 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> ( ( n e. c \/ n = c ) -> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) R ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) )
321 151 320 syld 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> ( -. c e. n -> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) R ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) )
322 321 imp 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ -. c e. n ) -> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) R ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) )
323 135 notbid 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( -. c e. n <-> -. suc c e. suc n ) )
324 323 adantr 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> ( -. c e. n <-> -. suc c e. suc n ) )
325 324 adantr 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> ( -. c e. n <-> -. suc c e. suc n ) )
326 325 biimpa 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ -. c e. n ) -> -. suc c e. suc n )
327 326 iffalsed 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ -. c e. n ) -> if ( suc c e. suc n , ( f ` suc c ) , ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) = ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) )
328 322 327 breqtrrd 
 |-  ( ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) /\ -. c e. n ) -> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) R if ( suc c e. suc n , ( f ` suc c ) , ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) )
329 140 328 pm2.61dan 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) R if ( suc c e. suc n , ( f ` suc c ) , ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) )
330 elelsuc 
 |-  ( c e. ( n +o m ) -> c e. suc ( n +o m ) )
331 330 adantl 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> c e. suc ( n +o m ) )
332 eleq1 
 |-  ( p = c -> ( p e. suc n <-> c e. suc n ) )
333 fveq2 
 |-  ( p = c -> ( f ` p ) = ( f ` c ) )
334 eqeq2 
 |-  ( p = c -> ( ( n +o q ) = p <-> ( n +o q ) = c ) )
335 334 riotabidv 
 |-  ( p = c -> ( iota_ q e. _om ( n +o q ) = p ) = ( iota_ q e. _om ( n +o q ) = c ) )
336 335 fveq2d 
 |-  ( p = c -> ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) = ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) )
337 332 333 336 ifbieq12d 
 |-  ( p = c -> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) = if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) )
338 fvex 
 |-  ( f ` c ) e. _V
339 fvex 
 |-  ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) e. _V
340 338 339 ifex 
 |-  if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) e. _V
341 337 32 340 fvmpt 
 |-  ( c e. suc ( n +o m ) -> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` c ) = if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) )
342 331 341 syl 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` c ) = if ( c e. suc n , ( f ` c ) , ( g ` ( iota_ q e. _om ( n +o q ) = c ) ) ) )
343 ordsucelsuc 
 |-  ( Ord ( n +o m ) -> ( c e. ( n +o m ) <-> suc c e. suc ( n +o m ) ) )
344 19 343 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( c e. ( n +o m ) <-> suc c e. suc ( n +o m ) ) )
345 344 adantr 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> ( c e. ( n +o m ) <-> suc c e. suc ( n +o m ) ) )
346 345 biimpa 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> suc c e. suc ( n +o m ) )
347 eleq1 
 |-  ( p = suc c -> ( p e. suc n <-> suc c e. suc n ) )
348 fveq2 
 |-  ( p = suc c -> ( f ` p ) = ( f ` suc c ) )
349 eqeq2 
 |-  ( p = suc c -> ( ( n +o q ) = p <-> ( n +o q ) = suc c ) )
350 349 riotabidv 
 |-  ( p = suc c -> ( iota_ q e. _om ( n +o q ) = p ) = ( iota_ q e. _om ( n +o q ) = suc c ) )
351 350 fveq2d 
 |-  ( p = suc c -> ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) = ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) )
352 347 348 351 ifbieq12d 
 |-  ( p = suc c -> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) = if ( suc c e. suc n , ( f ` suc c ) , ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) )
353 fvex 
 |-  ( f ` suc c ) e. _V
354 fvex 
 |-  ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) e. _V
355 353 354 ifex 
 |-  if ( suc c e. suc n , ( f ` suc c ) , ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) e. _V
356 352 32 355 fvmpt 
 |-  ( suc c e. suc ( n +o m ) -> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` suc c ) = if ( suc c e. suc n , ( f ` suc c ) , ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) )
357 346 356 syl 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` suc c ) = if ( suc c e. suc n , ( f ` suc c ) , ( g ` ( iota_ q e. _om ( n +o q ) = suc c ) ) ) )
358 329 342 357 3brtr4d 
 |-  ( ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) /\ c e. ( n +o m ) ) -> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` c ) R ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` suc c ) )
359 358 ralrimiva 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> A. c e. ( n +o m ) ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` c ) R ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` suc c ) )
360 fvex 
 |-  ( f ` p ) e. _V
361 fvex 
 |-  ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) e. _V
362 360 361 ifex 
 |-  if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) e. _V
363 362 32 fnmpti 
 |-  ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) Fn suc ( n +o m )
364 46 sucex 
 |-  suc ( n +o m ) e. _V
365 364 mptex 
 |-  ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) e. _V
366 fneq1 
 |-  ( h = ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) -> ( h Fn suc ( n +o m ) <-> ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) Fn suc ( n +o m ) ) )
367 fveq1 
 |-  ( h = ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) -> ( h ` (/) ) = ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` (/) ) )
368 367 eqeq1d 
 |-  ( h = ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) -> ( ( h ` (/) ) = x <-> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` (/) ) = x ) )
369 fveq1 
 |-  ( h = ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) -> ( h ` ( n +o m ) ) = ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` ( n +o m ) ) )
370 369 eqeq1d 
 |-  ( h = ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) -> ( ( h ` ( n +o m ) ) = y <-> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` ( n +o m ) ) = y ) )
371 368 370 anbi12d 
 |-  ( h = ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) -> ( ( ( h ` (/) ) = x /\ ( h ` ( n +o m ) ) = y ) <-> ( ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` (/) ) = x /\ ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` ( n +o m ) ) = y ) ) )
372 fveq1 
 |-  ( h = ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) -> ( h ` c ) = ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` c ) )
373 fveq1 
 |-  ( h = ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) -> ( h ` suc c ) = ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` suc c ) )
374 372 373 breq12d 
 |-  ( h = ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) -> ( ( h ` c ) R ( h ` suc c ) <-> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` c ) R ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` suc c ) ) )
375 374 ralbidv 
 |-  ( h = ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) -> ( A. c e. ( n +o m ) ( h ` c ) R ( h ` suc c ) <-> A. c e. ( n +o m ) ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` c ) R ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` suc c ) ) )
376 366 371 375 3anbi123d 
 |-  ( h = ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) -> ( ( h Fn suc ( n +o m ) /\ ( ( h ` (/) ) = x /\ ( h ` ( n +o m ) ) = y ) /\ A. c e. ( n +o m ) ( h ` c ) R ( h ` suc c ) ) <-> ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) Fn suc ( n +o m ) /\ ( ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` (/) ) = x /\ ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` ( n +o m ) ) = y ) /\ A. c e. ( n +o m ) ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` c ) R ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` suc c ) ) ) )
377 365 376 spcev 
 |-  ( ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) Fn suc ( n +o m ) /\ ( ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` (/) ) = x /\ ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` ( n +o m ) ) = y ) /\ A. c e. ( n +o m ) ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` c ) R ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` suc c ) ) -> E. h ( h Fn suc ( n +o m ) /\ ( ( h ` (/) ) = x /\ ( h ` ( n +o m ) ) = y ) /\ A. c e. ( n +o m ) ( h ` c ) R ( h ` suc c ) ) )
378 363 377 mp3an1 
 |-  ( ( ( ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` (/) ) = x /\ ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` ( n +o m ) ) = y ) /\ A. c e. ( n +o m ) ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` c ) R ( ( p e. suc ( n +o m ) |-> if ( p e. suc n , ( f ` p ) , ( g ` ( iota_ q e. _om ( n +o q ) = p ) ) ) ) ` suc c ) ) -> E. h ( h Fn suc ( n +o m ) /\ ( ( h ` (/) ) = x /\ ( h ` ( n +o m ) ) = y ) /\ A. c e. ( n +o m ) ( h ` c ) R ( h ` suc c ) ) )
379 45 123 359 378 syl21anc 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> E. h ( h Fn suc ( n +o m ) /\ ( ( h ` (/) ) = x /\ ( h ` ( n +o m ) ) = y ) /\ A. c e. ( n +o m ) ( h ` c ) R ( h ` suc c ) ) )
380 suceq 
 |-  ( p = ( n +o m ) -> suc p = suc ( n +o m ) )
381 380 fneq2d 
 |-  ( p = ( n +o m ) -> ( h Fn suc p <-> h Fn suc ( n +o m ) ) )
382 fveqeq2 
 |-  ( p = ( n +o m ) -> ( ( h ` p ) = y <-> ( h ` ( n +o m ) ) = y ) )
383 382 anbi2d 
 |-  ( p = ( n +o m ) -> ( ( ( h ` (/) ) = x /\ ( h ` p ) = y ) <-> ( ( h ` (/) ) = x /\ ( h ` ( n +o m ) ) = y ) ) )
384 raleq 
 |-  ( p = ( n +o m ) -> ( A. c e. p ( h ` c ) R ( h ` suc c ) <-> A. c e. ( n +o m ) ( h ` c ) R ( h ` suc c ) ) )
385 381 383 384 3anbi123d 
 |-  ( p = ( n +o m ) -> ( ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) <-> ( h Fn suc ( n +o m ) /\ ( ( h ` (/) ) = x /\ ( h ` ( n +o m ) ) = y ) /\ A. c e. ( n +o m ) ( h ` c ) R ( h ` suc c ) ) ) )
386 385 exbidv 
 |-  ( p = ( n +o m ) -> ( E. h ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) <-> E. h ( h Fn suc ( n +o m ) /\ ( ( h ` (/) ) = x /\ ( h ` ( n +o m ) ) = y ) /\ A. c e. ( n +o m ) ( h ` c ) R ( h ` suc c ) ) ) )
387 386 rspcev 
 |-  ( ( ( n +o m ) e. ( _om \ 1o ) /\ E. h ( h Fn suc ( n +o m ) /\ ( ( h ` (/) ) = x /\ ( h ` ( n +o m ) ) = y ) /\ A. c e. ( n +o m ) ( h ` c ) R ( h ` suc c ) ) ) -> E. p e. ( _om \ 1o ) E. h ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) )
388 23 379 387 syl2an2r 
 |-  ( ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) /\ ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) ) -> E. p e. ( _om \ 1o ) E. h ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) )
389 388 ex 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) -> E. p e. ( _om \ 1o ) E. h ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) ) )
390 389 exlimdvv 
 |-  ( ( n e. ( _om \ 1o ) /\ m e. ( _om \ 1o ) ) -> ( E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) -> E. p e. ( _om \ 1o ) E. h ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) ) )
391 390 rexlimivv 
 |-  ( E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) -> E. p e. ( _om \ 1o ) E. h ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) )
392 391 exlimiv 
 |-  ( E. z E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) -> E. p e. ( _om \ 1o ) E. h ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) )
393 vex 
 |-  x e. _V
394 vex 
 |-  y e. _V
395 393 394 opelco 
 |-  ( <. x , y >. e. ( t++ R o. t++ R ) <-> E. z ( x t++ R z /\ z t++ R y ) )
396 reeanv 
 |-  ( E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) ( E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ E. g ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) <-> ( E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ E. m e. ( _om \ 1o ) E. g ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) )
397 eeanv 
 |-  ( E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) <-> ( E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ E. g ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) )
398 397 2rexbii 
 |-  ( E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) <-> E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) ( E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ E. g ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) )
399 brttrcl 
 |-  ( x t++ R z <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) )
400 brttrcl 
 |-  ( z t++ R y <-> E. m e. ( _om \ 1o ) E. g ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) )
401 399 400 anbi12i 
 |-  ( ( x t++ R z /\ z t++ R y ) <-> ( E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ E. m e. ( _om \ 1o ) E. g ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) )
402 396 398 401 3bitr4ri 
 |-  ( ( x t++ R z /\ z t++ R y ) <-> E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) )
403 402 exbii 
 |-  ( E. z ( x t++ R z /\ z t++ R y ) <-> E. z E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) )
404 395 403 bitri 
 |-  ( <. x , y >. e. ( t++ R o. t++ R ) <-> E. z E. n e. ( _om \ 1o ) E. m e. ( _om \ 1o ) E. f E. g ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) /\ ( g Fn suc m /\ ( ( g ` (/) ) = z /\ ( g ` m ) = y ) /\ A. b e. m ( g ` b ) R ( g ` suc b ) ) ) )
405 df-br 
 |-  ( x t++ R y <-> <. x , y >. e. t++ R )
406 brttrcl 
 |-  ( x t++ R y <-> E. p e. ( _om \ 1o ) E. h ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) )
407 405 406 bitr3i 
 |-  ( <. x , y >. e. t++ R <-> E. p e. ( _om \ 1o ) E. h ( h Fn suc p /\ ( ( h ` (/) ) = x /\ ( h ` p ) = y ) /\ A. c e. p ( h ` c ) R ( h ` suc c ) ) )
408 392 404 407 3imtr4i 
 |-  ( <. x , y >. e. ( t++ R o. t++ R ) -> <. x , y >. e. t++ R )
409 1 408 relssi 
 |-  ( t++ R o. t++ R ) C_ t++ R