Metamath Proof Explorer

Theorem frxp

Description: A lexicographical ordering of two well-founded classes. (Contributed by Scott Fenton, 17-Mar-2011) (Revised by Mario Carneiro, 7-Mar-2013) (Proof shortened by Wolf Lammen, 4-Oct-2014)

Ref Expression
Hypothesis frxp.1 
|- T = { <. x , y >. | ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) ) }
Assertion frxp 
|- ( ( R Fr A /\ S Fr B ) -> T Fr ( A X. B ) )

Proof

Step Hyp Ref Expression
1 frxp.1 
 |-  T = { <. x , y >. | ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) ) }
2 ssn0 
 |-  ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> ( A X. B ) =/= (/) )
3 xpnz 
 |-  ( ( A =/= (/) /\ B =/= (/) ) <-> ( A X. B ) =/= (/) )
4 3 biimpri 
 |-  ( ( A X. B ) =/= (/) -> ( A =/= (/) /\ B =/= (/) ) )
5 4 simprd 
 |-  ( ( A X. B ) =/= (/) -> B =/= (/) )
6 2 5 syl 
 |-  ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> B =/= (/) )
7 dmxp 
 |-  ( B =/= (/) -> dom ( A X. B ) = A )
8 dmss 
 |-  ( s C_ ( A X. B ) -> dom s C_ dom ( A X. B ) )
9 sseq2 
 |-  ( dom ( A X. B ) = A -> ( dom s C_ dom ( A X. B ) <-> dom s C_ A ) )
10 8 9 syl5ib 
 |-  ( dom ( A X. B ) = A -> ( s C_ ( A X. B ) -> dom s C_ A ) )
11 7 10 syl 
 |-  ( B =/= (/) -> ( s C_ ( A X. B ) -> dom s C_ A ) )
12 11 impcom 
 |-  ( ( s C_ ( A X. B ) /\ B =/= (/) ) -> dom s C_ A )
13 6 12 syldan 
 |-  ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> dom s C_ A )
14 relxp 
 |-  Rel ( A X. B )
15 relss 
 |-  ( s C_ ( A X. B ) -> ( Rel ( A X. B ) -> Rel s ) )
16 14 15 mpi 
 |-  ( s C_ ( A X. B ) -> Rel s )
17 reldm0 
 |-  ( Rel s -> ( s = (/) <-> dom s = (/) ) )
18 16 17 syl 
 |-  ( s C_ ( A X. B ) -> ( s = (/) <-> dom s = (/) ) )
19 18 necon3bid 
 |-  ( s C_ ( A X. B ) -> ( s =/= (/) <-> dom s =/= (/) ) )
20 19 biimpa 
 |-  ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> dom s =/= (/) )
21 13 20 jca 
 |-  ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> ( dom s C_ A /\ dom s =/= (/) ) )
22 df-fr 
 |-  ( R Fr A <-> A. v ( ( v C_ A /\ v =/= (/) ) -> E. a e. v A. c e. v -. c R a ) )
23 vex 
 |-  s e. _V
24 23 dmex 
 |-  dom s e. _V
25 sseq1 
 |-  ( v = dom s -> ( v C_ A <-> dom s C_ A ) )
26 neeq1 
 |-  ( v = dom s -> ( v =/= (/) <-> dom s =/= (/) ) )
27 25 26 anbi12d 
 |-  ( v = dom s -> ( ( v C_ A /\ v =/= (/) ) <-> ( dom s C_ A /\ dom s =/= (/) ) ) )
28 raleq 
 |-  ( v = dom s -> ( A. c e. v -. c R a <-> A. c e. dom s -. c R a ) )
29 28 rexeqbi1dv 
 |-  ( v = dom s -> ( E. a e. v A. c e. v -. c R a <-> E. a e. dom s A. c e. dom s -. c R a ) )
30 27 29 imbi12d 
 |-  ( v = dom s -> ( ( ( v C_ A /\ v =/= (/) ) -> E. a e. v A. c e. v -. c R a ) <-> ( ( dom s C_ A /\ dom s =/= (/) ) -> E. a e. dom s A. c e. dom s -. c R a ) ) )
31 24 30 spcv 
 |-  ( A. v ( ( v C_ A /\ v =/= (/) ) -> E. a e. v A. c e. v -. c R a ) -> ( ( dom s C_ A /\ dom s =/= (/) ) -> E. a e. dom s A. c e. dom s -. c R a ) )
32 22 31 sylbi 
 |-  ( R Fr A -> ( ( dom s C_ A /\ dom s =/= (/) ) -> E. a e. dom s A. c e. dom s -. c R a ) )
33 21 32 syl5 
 |-  ( R Fr A -> ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> E. a e. dom s A. c e. dom s -. c R a ) )
34 33 adantr 
 |-  ( ( R Fr A /\ S Fr B ) -> ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> E. a e. dom s A. c e. dom s -. c R a ) )
35 imassrn 
 |-  ( s " { a } ) C_ ran s
36 xpeq0 
 |-  ( ( A X. B ) = (/) <-> ( A = (/) \/ B = (/) ) )
37 36 biimpri 
 |-  ( ( A = (/) \/ B = (/) ) -> ( A X. B ) = (/) )
38 37 orcs 
 |-  ( A = (/) -> ( A X. B ) = (/) )
39 sseq2 
 |-  ( ( A X. B ) = (/) -> ( s C_ ( A X. B ) <-> s C_ (/) ) )
40 ss0 
 |-  ( s C_ (/) -> s = (/) )
41 39 40 syl6bi 
 |-  ( ( A X. B ) = (/) -> ( s C_ ( A X. B ) -> s = (/) ) )
42 38 41 syl 
 |-  ( A = (/) -> ( s C_ ( A X. B ) -> s = (/) ) )
43 rneq 
 |-  ( s = (/) -> ran s = ran (/) )
44 rn0 
 |-  ran (/) = (/)
45 0ss 
 |-  (/) C_ B
46 44 45 eqsstri 
 |-  ran (/) C_ B
47 43 46 eqsstrdi 
 |-  ( s = (/) -> ran s C_ B )
48 42 47 syl6 
 |-  ( A = (/) -> ( s C_ ( A X. B ) -> ran s C_ B ) )
49 rnxp 
 |-  ( A =/= (/) -> ran ( A X. B ) = B )
50 rnss 
 |-  ( s C_ ( A X. B ) -> ran s C_ ran ( A X. B ) )
51 sseq2 
 |-  ( ran ( A X. B ) = B -> ( ran s C_ ran ( A X. B ) <-> ran s C_ B ) )
52 50 51 syl5ib 
 |-  ( ran ( A X. B ) = B -> ( s C_ ( A X. B ) -> ran s C_ B ) )
53 49 52 syl 
 |-  ( A =/= (/) -> ( s C_ ( A X. B ) -> ran s C_ B ) )
54 48 53 pm2.61ine 
 |-  ( s C_ ( A X. B ) -> ran s C_ B )
55 35 54 sstrid 
 |-  ( s C_ ( A X. B ) -> ( s " { a } ) C_ B )
56 vex 
 |-  a e. _V
57 56 eldm 
 |-  ( a e. dom s <-> E. b a s b )
58 vex 
 |-  b e. _V
59 56 58 elimasn 
 |-  ( b e. ( s " { a } ) <-> <. a , b >. e. s )
60 df-br 
 |-  ( a s b <-> <. a , b >. e. s )
61 59 60 bitr4i 
 |-  ( b e. ( s " { a } ) <-> a s b )
62 ne0i 
 |-  ( b e. ( s " { a } ) -> ( s " { a } ) =/= (/) )
63 61 62 sylbir 
 |-  ( a s b -> ( s " { a } ) =/= (/) )
64 63 exlimiv 
 |-  ( E. b a s b -> ( s " { a } ) =/= (/) )
65 57 64 sylbi 
 |-  ( a e. dom s -> ( s " { a } ) =/= (/) )
66 df-fr 
 |-  ( S Fr B <-> A. v ( ( v C_ B /\ v =/= (/) ) -> E. b e. v A. d e. v -. d S b ) )
67 23 imaex 
 |-  ( s " { a } ) e. _V
68 sseq1 
 |-  ( v = ( s " { a } ) -> ( v C_ B <-> ( s " { a } ) C_ B ) )
69 neeq1 
 |-  ( v = ( s " { a } ) -> ( v =/= (/) <-> ( s " { a } ) =/= (/) ) )
70 68 69 anbi12d 
 |-  ( v = ( s " { a } ) -> ( ( v C_ B /\ v =/= (/) ) <-> ( ( s " { a } ) C_ B /\ ( s " { a } ) =/= (/) ) ) )
71 raleq 
 |-  ( v = ( s " { a } ) -> ( A. d e. v -. d S b <-> A. d e. ( s " { a } ) -. d S b ) )
72 71 rexeqbi1dv 
 |-  ( v = ( s " { a } ) -> ( E. b e. v A. d e. v -. d S b <-> E. b e. ( s " { a } ) A. d e. ( s " { a } ) -. d S b ) )
73 70 72 imbi12d 
 |-  ( v = ( s " { a } ) -> ( ( ( v C_ B /\ v =/= (/) ) -> E. b e. v A. d e. v -. d S b ) <-> ( ( ( s " { a } ) C_ B /\ ( s " { a } ) =/= (/) ) -> E. b e. ( s " { a } ) A. d e. ( s " { a } ) -. d S b ) ) )
74 67 73 spcv 
 |-  ( A. v ( ( v C_ B /\ v =/= (/) ) -> E. b e. v A. d e. v -. d S b ) -> ( ( ( s " { a } ) C_ B /\ ( s " { a } ) =/= (/) ) -> E. b e. ( s " { a } ) A. d e. ( s " { a } ) -. d S b ) )
75 66 74 sylbi 
 |-  ( S Fr B -> ( ( ( s " { a } ) C_ B /\ ( s " { a } ) =/= (/) ) -> E. b e. ( s " { a } ) A. d e. ( s " { a } ) -. d S b ) )
76 55 65 75 syl2ani 
 |-  ( S Fr B -> ( ( s C_ ( A X. B ) /\ a e. dom s ) -> E. b e. ( s " { a } ) A. d e. ( s " { a } ) -. d S b ) )
77 1stdm 
 |-  ( ( Rel s /\ w e. s ) -> ( 1st ` w ) e. dom s )
78 breq1 
 |-  ( c = ( 1st ` w ) -> ( c R a <-> ( 1st ` w ) R a ) )
79 78 notbid 
 |-  ( c = ( 1st ` w ) -> ( -. c R a <-> -. ( 1st ` w ) R a ) )
80 79 rspccv 
 |-  ( A. c e. dom s -. c R a -> ( ( 1st ` w ) e. dom s -> -. ( 1st ` w ) R a ) )
81 77 80 syl5 
 |-  ( A. c e. dom s -. c R a -> ( ( Rel s /\ w e. s ) -> -. ( 1st ` w ) R a ) )
82 81 expd 
 |-  ( A. c e. dom s -. c R a -> ( Rel s -> ( w e. s -> -. ( 1st ` w ) R a ) ) )
83 82 impcom 
 |-  ( ( Rel s /\ A. c e. dom s -. c R a ) -> ( w e. s -> -. ( 1st ` w ) R a ) )
84 83 adantr 
 |-  ( ( ( Rel s /\ A. c e. dom s -. c R a ) /\ A. d e. ( s " { a } ) -. d S b ) -> ( w e. s -> -. ( 1st ` w ) R a ) )
85 elrel 
 |-  ( ( Rel s /\ w e. s ) -> E. t E. u w = <. t , u >. )
86 85 ex 
 |-  ( Rel s -> ( w e. s -> E. t E. u w = <. t , u >. ) )
87 86 adantr 
 |-  ( ( Rel s /\ A. d e. ( s " { a } ) -. d S b ) -> ( w e. s -> E. t E. u w = <. t , u >. ) )
88 vex 
 |-  u e. _V
89 56 88 elimasn 
 |-  ( u e. ( s " { a } ) <-> <. a , u >. e. s )
90 breq1 
 |-  ( d = u -> ( d S b <-> u S b ) )
91 90 notbid 
 |-  ( d = u -> ( -. d S b <-> -. u S b ) )
92 91 rspccv 
 |-  ( A. d e. ( s " { a } ) -. d S b -> ( u e. ( s " { a } ) -> -. u S b ) )
93 89 92 syl5bir 
 |-  ( A. d e. ( s " { a } ) -. d S b -> ( <. a , u >. e. s -> -. u S b ) )
94 93 adantl 
 |-  ( ( Rel s /\ A. d e. ( s " { a } ) -. d S b ) -> ( <. a , u >. e. s -> -. u S b ) )
95 opeq1 
 |-  ( t = a -> <. t , u >. = <. a , u >. )
96 95 eleq1d 
 |-  ( t = a -> ( <. t , u >. e. s <-> <. a , u >. e. s ) )
97 96 imbi1d 
 |-  ( t = a -> ( ( <. t , u >. e. s -> -. u S b ) <-> ( <. a , u >. e. s -> -. u S b ) ) )
98 94 97 syl5ibr 
 |-  ( t = a -> ( ( Rel s /\ A. d e. ( s " { a } ) -. d S b ) -> ( <. t , u >. e. s -> -. u S b ) ) )
99 98 com3l 
 |-  ( ( Rel s /\ A. d e. ( s " { a } ) -. d S b ) -> ( <. t , u >. e. s -> ( t = a -> -. u S b ) ) )
100 eleq1 
 |-  ( w = <. t , u >. -> ( w e. s <-> <. t , u >. e. s ) )
101 vex 
 |-  t e. _V
102 101 88 op1std 
 |-  ( w = <. t , u >. -> ( 1st ` w ) = t )
103 102 eqeq1d 
 |-  ( w = <. t , u >. -> ( ( 1st ` w ) = a <-> t = a ) )
104 101 88 op2ndd 
 |-  ( w = <. t , u >. -> ( 2nd ` w ) = u )
105 104 breq1d 
 |-  ( w = <. t , u >. -> ( ( 2nd ` w ) S b <-> u S b ) )
106 105 notbid 
 |-  ( w = <. t , u >. -> ( -. ( 2nd ` w ) S b <-> -. u S b ) )
107 103 106 imbi12d 
 |-  ( w = <. t , u >. -> ( ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) <-> ( t = a -> -. u S b ) ) )
108 100 107 imbi12d 
 |-  ( w = <. t , u >. -> ( ( w e. s -> ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) <-> ( <. t , u >. e. s -> ( t = a -> -. u S b ) ) ) )
109 99 108 syl5ibr 
 |-  ( w = <. t , u >. -> ( ( Rel s /\ A. d e. ( s " { a } ) -. d S b ) -> ( w e. s -> ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) ) )
110 109 exlimivv 
 |-  ( E. t E. u w = <. t , u >. -> ( ( Rel s /\ A. d e. ( s " { a } ) -. d S b ) -> ( w e. s -> ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) ) )
111 110 com3l 
 |-  ( ( Rel s /\ A. d e. ( s " { a } ) -. d S b ) -> ( w e. s -> ( E. t E. u w = <. t , u >. -> ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) ) )
112 87 111 mpdd 
 |-  ( ( Rel s /\ A. d e. ( s " { a } ) -. d S b ) -> ( w e. s -> ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) )
113 112 adantlr 
 |-  ( ( ( Rel s /\ A. c e. dom s -. c R a ) /\ A. d e. ( s " { a } ) -. d S b ) -> ( w e. s -> ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) )
114 84 113 jcad 
 |-  ( ( ( Rel s /\ A. c e. dom s -. c R a ) /\ A. d e. ( s " { a } ) -. d S b ) -> ( w e. s -> ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) ) )
115 114 ralrimiv 
 |-  ( ( ( Rel s /\ A. c e. dom s -. c R a ) /\ A. d e. ( s " { a } ) -. d S b ) -> A. w e. s ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) )
116 115 ex 
 |-  ( ( Rel s /\ A. c e. dom s -. c R a ) -> ( A. d e. ( s " { a } ) -. d S b -> A. w e. s ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) ) )
117 16 116 sylan 
 |-  ( ( s C_ ( A X. B ) /\ A. c e. dom s -. c R a ) -> ( A. d e. ( s " { a } ) -. d S b -> A. w e. s ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) ) )
118 olc 
 |-  ( ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) -> ( -. ( w e. ( A X. B ) /\ <. a , b >. e. ( A X. B ) ) \/ ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) ) )
119 118 ralimi 
 |-  ( A. w e. s ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) -> A. w e. s ( -. ( w e. ( A X. B ) /\ <. a , b >. e. ( A X. B ) ) \/ ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) ) )
120 117 119 syl6 
 |-  ( ( s C_ ( A X. B ) /\ A. c e. dom s -. c R a ) -> ( A. d e. ( s " { a } ) -. d S b -> A. w e. s ( -. ( w e. ( A X. B ) /\ <. a , b >. e. ( A X. B ) ) \/ ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) ) ) )
121 ianor 
 |-  ( -. ( ( w e. ( A X. B ) /\ <. a , b >. e. ( A X. B ) ) /\ ( ( 1st ` w ) R a \/ ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) ) ) <-> ( -. ( w e. ( A X. B ) /\ <. a , b >. e. ( A X. B ) ) \/ -. ( ( 1st ` w ) R a \/ ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) ) ) )
122 vex 
 |-  w e. _V
123 opex 
 |-  <. a , b >. e. _V
124 eleq1 
 |-  ( x = w -> ( x e. ( A X. B ) <-> w e. ( A X. B ) ) )
125 124 anbi1d 
 |-  ( x = w -> ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) <-> ( w e. ( A X. B ) /\ y e. ( A X. B ) ) ) )
126 fveq2 
 |-  ( x = w -> ( 1st ` x ) = ( 1st ` w ) )
127 126 breq1d 
 |-  ( x = w -> ( ( 1st ` x ) R ( 1st ` y ) <-> ( 1st ` w ) R ( 1st ` y ) ) )
128 126 eqeq1d 
 |-  ( x = w -> ( ( 1st ` x ) = ( 1st ` y ) <-> ( 1st ` w ) = ( 1st ` y ) ) )
129 fveq2 
 |-  ( x = w -> ( 2nd ` x ) = ( 2nd ` w ) )
130 129 breq1d 
 |-  ( x = w -> ( ( 2nd ` x ) S ( 2nd ` y ) <-> ( 2nd ` w ) S ( 2nd ` y ) ) )
131 128 130 anbi12d 
 |-  ( x = w -> ( ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) <-> ( ( 1st ` w ) = ( 1st ` y ) /\ ( 2nd ` w ) S ( 2nd ` y ) ) ) )
132 127 131 orbi12d 
 |-  ( x = w -> ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) <-> ( ( 1st ` w ) R ( 1st ` y ) \/ ( ( 1st ` w ) = ( 1st ` y ) /\ ( 2nd ` w ) S ( 2nd ` y ) ) ) ) )
133 125 132 anbi12d 
 |-  ( x = w -> ( ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) ) <-> ( ( w e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` w ) R ( 1st ` y ) \/ ( ( 1st ` w ) = ( 1st ` y ) /\ ( 2nd ` w ) S ( 2nd ` y ) ) ) ) ) )
134 eleq1 
 |-  ( y = <. a , b >. -> ( y e. ( A X. B ) <-> <. a , b >. e. ( A X. B ) ) )
135 134 anbi2d 
 |-  ( y = <. a , b >. -> ( ( w e. ( A X. B ) /\ y e. ( A X. B ) ) <-> ( w e. ( A X. B ) /\ <. a , b >. e. ( A X. B ) ) ) )
136 56 58 op1std 
 |-  ( y = <. a , b >. -> ( 1st ` y ) = a )
137 136 breq2d 
 |-  ( y = <. a , b >. -> ( ( 1st ` w ) R ( 1st ` y ) <-> ( 1st ` w ) R a ) )
138 136 eqeq2d 
 |-  ( y = <. a , b >. -> ( ( 1st ` w ) = ( 1st ` y ) <-> ( 1st ` w ) = a ) )
139 56 58 op2ndd 
 |-  ( y = <. a , b >. -> ( 2nd ` y ) = b )
140 139 breq2d 
 |-  ( y = <. a , b >. -> ( ( 2nd ` w ) S ( 2nd ` y ) <-> ( 2nd ` w ) S b ) )
141 138 140 anbi12d 
 |-  ( y = <. a , b >. -> ( ( ( 1st ` w ) = ( 1st ` y ) /\ ( 2nd ` w ) S ( 2nd ` y ) ) <-> ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) ) )
142 137 141 orbi12d 
 |-  ( y = <. a , b >. -> ( ( ( 1st ` w ) R ( 1st ` y ) \/ ( ( 1st ` w ) = ( 1st ` y ) /\ ( 2nd ` w ) S ( 2nd ` y ) ) ) <-> ( ( 1st ` w ) R a \/ ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) ) ) )
143 135 142 anbi12d 
 |-  ( y = <. a , b >. -> ( ( ( w e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` w ) R ( 1st ` y ) \/ ( ( 1st ` w ) = ( 1st ` y ) /\ ( 2nd ` w ) S ( 2nd ` y ) ) ) ) <-> ( ( w e. ( A X. B ) /\ <. a , b >. e. ( A X. B ) ) /\ ( ( 1st ` w ) R a \/ ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) ) ) ) )
144 122 123 133 143 1 brab 
 |-  ( w T <. a , b >. <-> ( ( w e. ( A X. B ) /\ <. a , b >. e. ( A X. B ) ) /\ ( ( 1st ` w ) R a \/ ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) ) ) )
145 121 144 xchnxbir 
 |-  ( -. w T <. a , b >. <-> ( -. ( w e. ( A X. B ) /\ <. a , b >. e. ( A X. B ) ) \/ -. ( ( 1st ` w ) R a \/ ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) ) ) )
146 ioran 
 |-  ( -. ( ( 1st ` w ) R a \/ ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) ) <-> ( -. ( 1st ` w ) R a /\ -. ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) ) )
147 ianor 
 |-  ( -. ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) <-> ( -. ( 1st ` w ) = a \/ -. ( 2nd ` w ) S b ) )
148 pm4.62 
 |-  ( ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) <-> ( -. ( 1st ` w ) = a \/ -. ( 2nd ` w ) S b ) )
149 147 148 bitr4i 
 |-  ( -. ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) <-> ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) )
150 149 anbi2i 
 |-  ( ( -. ( 1st ` w ) R a /\ -. ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) ) <-> ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) )
151 146 150 bitri 
 |-  ( -. ( ( 1st ` w ) R a \/ ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) ) <-> ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) )
152 151 orbi2i 
 |-  ( ( -. ( w e. ( A X. B ) /\ <. a , b >. e. ( A X. B ) ) \/ -. ( ( 1st ` w ) R a \/ ( ( 1st ` w ) = a /\ ( 2nd ` w ) S b ) ) ) <-> ( -. ( w e. ( A X. B ) /\ <. a , b >. e. ( A X. B ) ) \/ ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) ) )
153 145 152 bitri 
 |-  ( -. w T <. a , b >. <-> ( -. ( w e. ( A X. B ) /\ <. a , b >. e. ( A X. B ) ) \/ ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) ) )
154 153 ralbii 
 |-  ( A. w e. s -. w T <. a , b >. <-> A. w e. s ( -. ( w e. ( A X. B ) /\ <. a , b >. e. ( A X. B ) ) \/ ( -. ( 1st ` w ) R a /\ ( ( 1st ` w ) = a -> -. ( 2nd ` w ) S b ) ) ) )
155 120 154 syl6ibr 
 |-  ( ( s C_ ( A X. B ) /\ A. c e. dom s -. c R a ) -> ( A. d e. ( s " { a } ) -. d S b -> A. w e. s -. w T <. a , b >. ) )
156 155 reximdv 
 |-  ( ( s C_ ( A X. B ) /\ A. c e. dom s -. c R a ) -> ( E. b e. ( s " { a } ) A. d e. ( s " { a } ) -. d S b -> E. b e. ( s " { a } ) A. w e. s -. w T <. a , b >. ) )
157 156 ex 
 |-  ( s C_ ( A X. B ) -> ( A. c e. dom s -. c R a -> ( E. b e. ( s " { a } ) A. d e. ( s " { a } ) -. d S b -> E. b e. ( s " { a } ) A. w e. s -. w T <. a , b >. ) ) )
158 157 com23 
 |-  ( s C_ ( A X. B ) -> ( E. b e. ( s " { a } ) A. d e. ( s " { a } ) -. d S b -> ( A. c e. dom s -. c R a -> E. b e. ( s " { a } ) A. w e. s -. w T <. a , b >. ) ) )
159 158 adantr 
 |-  ( ( s C_ ( A X. B ) /\ a e. dom s ) -> ( E. b e. ( s " { a } ) A. d e. ( s " { a } ) -. d S b -> ( A. c e. dom s -. c R a -> E. b e. ( s " { a } ) A. w e. s -. w T <. a , b >. ) ) )
160 76 159 sylcom 
 |-  ( S Fr B -> ( ( s C_ ( A X. B ) /\ a e. dom s ) -> ( A. c e. dom s -. c R a -> E. b e. ( s " { a } ) A. w e. s -. w T <. a , b >. ) ) )
161 160 impl 
 |-  ( ( ( S Fr B /\ s C_ ( A X. B ) ) /\ a e. dom s ) -> ( A. c e. dom s -. c R a -> E. b e. ( s " { a } ) A. w e. s -. w T <. a , b >. ) )
162 161 expimpd 
 |-  ( ( S Fr B /\ s C_ ( A X. B ) ) -> ( ( a e. dom s /\ A. c e. dom s -. c R a ) -> E. b e. ( s " { a } ) A. w e. s -. w T <. a , b >. ) )
163 162 3adant3 
 |-  ( ( S Fr B /\ s C_ ( A X. B ) /\ s =/= (/) ) -> ( ( a e. dom s /\ A. c e. dom s -. c R a ) -> E. b e. ( s " { a } ) A. w e. s -. w T <. a , b >. ) )
164 resss 
 |-  ( s |` { a } ) C_ s
165 df-rex 
 |-  ( E. b e. ( s " { a } ) A. w e. s -. w T <. a , b >. <-> E. b ( b e. ( s " { a } ) /\ A. w e. s -. w T <. a , b >. ) )
166 eqid 
 |-  <. a , b >. = <. a , b >.
167 eqeq1 
 |-  ( z = <. a , b >. -> ( z = <. a , b >. <-> <. a , b >. = <. a , b >. ) )
168 breq2 
 |-  ( z = <. a , b >. -> ( w T z <-> w T <. a , b >. ) )
169 168 notbid 
 |-  ( z = <. a , b >. -> ( -. w T z <-> -. w T <. a , b >. ) )
170 169 ralbidv 
 |-  ( z = <. a , b >. -> ( A. w e. s -. w T z <-> A. w e. s -. w T <. a , b >. ) )
171 170 anbi2d 
 |-  ( z = <. a , b >. -> ( ( <. a , b >. e. s /\ A. w e. s -. w T z ) <-> ( <. a , b >. e. s /\ A. w e. s -. w T <. a , b >. ) ) )
172 167 171 anbi12d 
 |-  ( z = <. a , b >. -> ( ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) <-> ( <. a , b >. = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T <. a , b >. ) ) ) )
173 123 172 spcev 
 |-  ( ( <. a , b >. = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T <. a , b >. ) ) -> E. z ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) )
174 166 173 mpan 
 |-  ( ( <. a , b >. e. s /\ A. w e. s -. w T <. a , b >. ) -> E. z ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) )
175 59 174 sylanb 
 |-  ( ( b e. ( s " { a } ) /\ A. w e. s -. w T <. a , b >. ) -> E. z ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) )
176 175 eximi 
 |-  ( E. b ( b e. ( s " { a } ) /\ A. w e. s -. w T <. a , b >. ) -> E. b E. z ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) )
177 165 176 sylbi 
 |-  ( E. b e. ( s " { a } ) A. w e. s -. w T <. a , b >. -> E. b E. z ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) )
178 excom 
 |-  ( E. b E. z ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) <-> E. z E. b ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) )
179 177 178 sylib 
 |-  ( E. b e. ( s " { a } ) A. w e. s -. w T <. a , b >. -> E. z E. b ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) )
180 df-rex 
 |-  ( E. z e. ( s |` { a } ) A. w e. s -. w T z <-> E. z ( z e. ( s |` { a } ) /\ A. w e. s -. w T z ) )
181 56 elsnres 
 |-  ( z e. ( s |` { a } ) <-> E. b ( z = <. a , b >. /\ <. a , b >. e. s ) )
182 181 anbi1i 
 |-  ( ( z e. ( s |` { a } ) /\ A. w e. s -. w T z ) <-> ( E. b ( z = <. a , b >. /\ <. a , b >. e. s ) /\ A. w e. s -. w T z ) )
183 19.41v 
 |-  ( E. b ( ( z = <. a , b >. /\ <. a , b >. e. s ) /\ A. w e. s -. w T z ) <-> ( E. b ( z = <. a , b >. /\ <. a , b >. e. s ) /\ A. w e. s -. w T z ) )
184 anass 
 |-  ( ( ( z = <. a , b >. /\ <. a , b >. e. s ) /\ A. w e. s -. w T z ) <-> ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) )
185 184 exbii 
 |-  ( E. b ( ( z = <. a , b >. /\ <. a , b >. e. s ) /\ A. w e. s -. w T z ) <-> E. b ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) )
186 182 183 185 3bitr2i 
 |-  ( ( z e. ( s |` { a } ) /\ A. w e. s -. w T z ) <-> E. b ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) )
187 186 exbii 
 |-  ( E. z ( z e. ( s |` { a } ) /\ A. w e. s -. w T z ) <-> E. z E. b ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) )
188 180 187 bitri 
 |-  ( E. z e. ( s |` { a } ) A. w e. s -. w T z <-> E. z E. b ( z = <. a , b >. /\ ( <. a , b >. e. s /\ A. w e. s -. w T z ) ) )
189 179 188 sylibr 
 |-  ( E. b e. ( s " { a } ) A. w e. s -. w T <. a , b >. -> E. z e. ( s |` { a } ) A. w e. s -. w T z )
190 ssrexv 
 |-  ( ( s |` { a } ) C_ s -> ( E. z e. ( s |` { a } ) A. w e. s -. w T z -> E. z e. s A. w e. s -. w T z ) )
191 164 189 190 mpsyl 
 |-  ( E. b e. ( s " { a } ) A. w e. s -. w T <. a , b >. -> E. z e. s A. w e. s -. w T z )
192 163 191 syl6 
 |-  ( ( S Fr B /\ s C_ ( A X. B ) /\ s =/= (/) ) -> ( ( a e. dom s /\ A. c e. dom s -. c R a ) -> E. z e. s A. w e. s -. w T z ) )
193 192 expd 
 |-  ( ( S Fr B /\ s C_ ( A X. B ) /\ s =/= (/) ) -> ( a e. dom s -> ( A. c e. dom s -. c R a -> E. z e. s A. w e. s -. w T z ) ) )
194 193 rexlimdv 
 |-  ( ( S Fr B /\ s C_ ( A X. B ) /\ s =/= (/) ) -> ( E. a e. dom s A. c e. dom s -. c R a -> E. z e. s A. w e. s -. w T z ) )
195 194 3expib 
 |-  ( S Fr B -> ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> ( E. a e. dom s A. c e. dom s -. c R a -> E. z e. s A. w e. s -. w T z ) ) )
196 195 adantl 
 |-  ( ( R Fr A /\ S Fr B ) -> ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> ( E. a e. dom s A. c e. dom s -. c R a -> E. z e. s A. w e. s -. w T z ) ) )
197 34 196 mpdd 
 |-  ( ( R Fr A /\ S Fr B ) -> ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> E. z e. s A. w e. s -. w T z ) )
198 197 alrimiv 
 |-  ( ( R Fr A /\ S Fr B ) -> A. s ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> E. z e. s A. w e. s -. w T z ) )
199 df-fr 
 |-  ( T Fr ( A X. B ) <-> A. s ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> E. z e. s A. w e. s -. w T z ) )
200 198 199 sylibr 
 |-  ( ( R Fr A /\ S Fr B ) -> T Fr ( A X. B ) )