Metamath Proof Explorer

Theorem frxp2

Description: Another way of giving a well-founded order to a Cartesian product of two classes. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypotheses xpord2.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 ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
frxp2.1 
|- ( ph -> R Fr A )
frxp2.2 
|- ( ph -> S Fr B )
Assertion frxp2 
|- ( ph -> T Fr ( A X. B ) )

Proof

Step Hyp Ref Expression
1 xpord2.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 ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
2 frxp2.1 
 |-  ( ph -> R Fr A )
3 frxp2.2 
 |-  ( ph -> S Fr B )
4 dmss 
 |-  ( s C_ ( A X. B ) -> dom s C_ dom ( A X. B ) )
5 4 ad2antrl 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> dom s C_ dom ( A X. B ) )
6 dmxpss 
 |-  dom ( A X. B ) C_ A
7 5 6 sstrdi 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> dom s C_ A )
8 simprr 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> s =/= (/) )
9 relxp 
 |-  Rel ( A X. B )
10 relss 
 |-  ( s C_ ( A X. B ) -> ( Rel ( A X. B ) -> Rel s ) )
11 9 10 mpi 
 |-  ( s C_ ( A X. B ) -> Rel s )
12 11 ad2antrl 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> Rel s )
13 reldm0 
 |-  ( Rel s -> ( s = (/) <-> dom s = (/) ) )
14 12 13 syl 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> ( s = (/) <-> dom s = (/) ) )
15 14 necon3bid 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> ( s =/= (/) <-> dom s =/= (/) ) )
16 8 15 mpbid 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> dom s =/= (/) )
17 2 adantr 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> R Fr A )
18 df-fr 
 |-  ( R Fr A <-> A. c ( ( c C_ A /\ c =/= (/) ) -> E. a e. c A. b e. c -. b R a ) )
19 17 18 sylib 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> A. c ( ( c C_ A /\ c =/= (/) ) -> E. a e. c A. b e. c -. b R a ) )
20 vex 
 |-  s e. _V
21 20 dmex 
 |-  dom s e. _V
22 sseq1 
 |-  ( c = dom s -> ( c C_ A <-> dom s C_ A ) )
23 neeq1 
 |-  ( c = dom s -> ( c =/= (/) <-> dom s =/= (/) ) )
24 22 23 anbi12d 
 |-  ( c = dom s -> ( ( c C_ A /\ c =/= (/) ) <-> ( dom s C_ A /\ dom s =/= (/) ) ) )
25 raleq 
 |-  ( c = dom s -> ( A. b e. c -. b R a <-> A. b e. dom s -. b R a ) )
26 25 rexeqbi1dv 
 |-  ( c = dom s -> ( E. a e. c A. b e. c -. b R a <-> E. a e. dom s A. b e. dom s -. b R a ) )
27 24 26 imbi12d 
 |-  ( c = dom s -> ( ( ( c C_ A /\ c =/= (/) ) -> E. a e. c A. b e. c -. b R a ) <-> ( ( dom s C_ A /\ dom s =/= (/) ) -> E. a e. dom s A. b e. dom s -. b R a ) ) )
28 21 27 spcv 
 |-  ( A. c ( ( c C_ A /\ c =/= (/) ) -> E. a e. c A. b e. c -. b R a ) -> ( ( dom s C_ A /\ dom s =/= (/) ) -> E. a e. dom s A. b e. dom s -. b R a ) )
29 19 28 syl 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> ( ( dom s C_ A /\ dom s =/= (/) ) -> E. a e. dom s A. b e. dom s -. b R a ) )
30 7 16 29 mp2and 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> E. a e. dom s A. b e. dom s -. b R a )
31 imassrn 
 |-  ( s " { a } ) C_ ran s
32 rnss 
 |-  ( s C_ ( A X. B ) -> ran s C_ ran ( A X. B ) )
33 32 ad2antrl 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> ran s C_ ran ( A X. B ) )
34 33 adantr 
 |-  ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) -> ran s C_ ran ( A X. B ) )
35 rnxpss 
 |-  ran ( A X. B ) C_ B
36 34 35 sstrdi 
 |-  ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) -> ran s C_ B )
37 31 36 sstrid 
 |-  ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) -> ( s " { a } ) C_ B )
38 simprl 
 |-  ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) -> a e. dom s )
39 imadisj 
 |-  ( ( s " { a } ) = (/) <-> ( dom s i^i { a } ) = (/) )
40 disjsn 
 |-  ( ( dom s i^i { a } ) = (/) <-> -. a e. dom s )
41 39 40 bitri 
 |-  ( ( s " { a } ) = (/) <-> -. a e. dom s )
42 41 necon2abii 
 |-  ( a e. dom s <-> ( s " { a } ) =/= (/) )
43 38 42 sylib 
 |-  ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) -> ( s " { a } ) =/= (/) )
44 df-fr 
 |-  ( S Fr B <-> A. e ( ( e C_ B /\ e =/= (/) ) -> E. c e. e A. d e. e -. d S c ) )
45 3 44 sylib 
 |-  ( ph -> A. e ( ( e C_ B /\ e =/= (/) ) -> E. c e. e A. d e. e -. d S c ) )
46 45 ad2antrr 
 |-  ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) -> A. e ( ( e C_ B /\ e =/= (/) ) -> E. c e. e A. d e. e -. d S c ) )
47 20 imaex 
 |-  ( s " { a } ) e. _V
48 sseq1 
 |-  ( e = ( s " { a } ) -> ( e C_ B <-> ( s " { a } ) C_ B ) )
49 neeq1 
 |-  ( e = ( s " { a } ) -> ( e =/= (/) <-> ( s " { a } ) =/= (/) ) )
50 48 49 anbi12d 
 |-  ( e = ( s " { a } ) -> ( ( e C_ B /\ e =/= (/) ) <-> ( ( s " { a } ) C_ B /\ ( s " { a } ) =/= (/) ) ) )
51 raleq 
 |-  ( e = ( s " { a } ) -> ( A. d e. e -. d S c <-> A. d e. ( s " { a } ) -. d S c ) )
52 51 rexeqbi1dv 
 |-  ( e = ( s " { a } ) -> ( E. c e. e A. d e. e -. d S c <-> E. c e. ( s " { a } ) A. d e. ( s " { a } ) -. d S c ) )
53 50 52 imbi12d 
 |-  ( e = ( s " { a } ) -> ( ( ( e C_ B /\ e =/= (/) ) -> E. c e. e A. d e. e -. d S c ) <-> ( ( ( s " { a } ) C_ B /\ ( s " { a } ) =/= (/) ) -> E. c e. ( s " { a } ) A. d e. ( s " { a } ) -. d S c ) ) )
54 47 53 spcv 
 |-  ( A. e ( ( e C_ B /\ e =/= (/) ) -> E. c e. e A. d e. e -. d S c ) -> ( ( ( s " { a } ) C_ B /\ ( s " { a } ) =/= (/) ) -> E. c e. ( s " { a } ) A. d e. ( s " { a } ) -. d S c ) )
55 46 54 syl 
 |-  ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) -> ( ( ( s " { a } ) C_ B /\ ( s " { a } ) =/= (/) ) -> E. c e. ( s " { a } ) A. d e. ( s " { a } ) -. d S c ) )
56 37 43 55 mp2and 
 |-  ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) -> E. c e. ( s " { a } ) A. d e. ( s " { a } ) -. d S c )
57 breq2 
 |-  ( p = <. a , c >. -> ( q T p <-> q T <. a , c >. ) )
58 57 notbid 
 |-  ( p = <. a , c >. -> ( -. q T p <-> -. q T <. a , c >. ) )
59 58 ralbidv 
 |-  ( p = <. a , c >. -> ( A. q e. s -. q T p <-> A. q e. s -. q T <. a , c >. ) )
60 simprl 
 |-  ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) -> c e. ( s " { a } ) )
61 vex 
 |-  a e. _V
62 vex 
 |-  c e. _V
63 61 62 elimasn 
 |-  ( c e. ( s " { a } ) <-> <. a , c >. e. s )
64 60 63 sylib 
 |-  ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) -> <. a , c >. e. s )
65 12 ad2antrr 
 |-  ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) -> Rel s )
66 elrel 
 |-  ( ( Rel s /\ q e. s ) -> E. e E. f q = <. e , f >. )
67 65 66 sylan 
 |-  ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ q e. s ) -> E. e E. f q = <. e , f >. )
68 breq1 
 |-  ( d = f -> ( d S c <-> f S c ) )
69 68 notbid 
 |-  ( d = f -> ( -. d S c <-> -. f S c ) )
70 simplrr 
 |-  ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. a , f >. e. s ) -> A. d e. ( s " { a } ) -. d S c )
71 vex 
 |-  f e. _V
72 61 71 elimasn 
 |-  ( f e. ( s " { a } ) <-> <. a , f >. e. s )
73 72 biimpri 
 |-  ( <. a , f >. e. s -> f e. ( s " { a } ) )
74 73 adantl 
 |-  ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. a , f >. e. s ) -> f e. ( s " { a } ) )
75 69 70 74 rspcdva 
 |-  ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. a , f >. e. s ) -> -. f S c )
76 75 intnanrd 
 |-  ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. a , f >. e. s ) -> -. ( f S c /\ f =/= c ) )
77 opeq1 
 |-  ( e = a -> <. e , f >. = <. a , f >. )
78 77 eleq1d 
 |-  ( e = a -> ( <. e , f >. e. s <-> <. a , f >. e. s ) )
79 78 anbi2d 
 |-  ( e = a -> ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) <-> ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. a , f >. e. s ) ) )
80 3anass 
 |-  ( ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) <-> ( ( e R a \/ e = a ) /\ ( ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) ) )
81 olc 
 |-  ( e = a -> ( e R a \/ e = a ) )
82 81 biantrurd 
 |-  ( e = a -> ( ( ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) <-> ( ( e R a \/ e = a ) /\ ( ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) ) ) )
83 neeq1 
 |-  ( e = a -> ( e =/= a <-> a =/= a ) )
84 83 orbi1d 
 |-  ( e = a -> ( ( e =/= a \/ f =/= c ) <-> ( a =/= a \/ f =/= c ) ) )
85 neirr 
 |-  -. a =/= a
86 85 biorfi 
 |-  ( f =/= c <-> ( a =/= a \/ f =/= c ) )
87 84 86 bitr4di 
 |-  ( e = a -> ( ( e =/= a \/ f =/= c ) <-> f =/= c ) )
88 87 anbi2d 
 |-  ( e = a -> ( ( ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) <-> ( ( f S c \/ f = c ) /\ f =/= c ) ) )
89 andir 
 |-  ( ( ( f S c \/ f = c ) /\ f =/= c ) <-> ( ( f S c /\ f =/= c ) \/ ( f = c /\ f =/= c ) ) )
90 nonconne 
 |-  -. ( f = c /\ f =/= c )
91 90 biorfri 
 |-  ( ( f S c /\ f =/= c ) <-> ( ( f S c /\ f =/= c ) \/ ( f = c /\ f =/= c ) ) )
92 89 91 bitr4i 
 |-  ( ( ( f S c \/ f = c ) /\ f =/= c ) <-> ( f S c /\ f =/= c ) )
93 88 92 bitrdi 
 |-  ( e = a -> ( ( ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) <-> ( f S c /\ f =/= c ) ) )
94 82 93 bitr3d 
 |-  ( e = a -> ( ( ( e R a \/ e = a ) /\ ( ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) ) <-> ( f S c /\ f =/= c ) ) )
95 80 94 bitrid 
 |-  ( e = a -> ( ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) <-> ( f S c /\ f =/= c ) ) )
96 95 notbid 
 |-  ( e = a -> ( -. ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) <-> -. ( f S c /\ f =/= c ) ) )
97 79 96 imbi12d 
 |-  ( e = a -> ( ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) -> -. ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) ) <-> ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. a , f >. e. s ) -> -. ( f S c /\ f =/= c ) ) ) )
98 76 97 mpbiri 
 |-  ( e = a -> ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) -> -. ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) ) )
99 98 impcom 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) /\ e = a ) -> -. ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) )
100 breq1 
 |-  ( b = e -> ( b R a <-> e R a ) )
101 100 notbid 
 |-  ( b = e -> ( -. b R a <-> -. e R a ) )
102 simplrr 
 |-  ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) -> A. b e. dom s -. b R a )
103 102 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) /\ e =/= a ) -> A. b e. dom s -. b R a )
104 vex 
 |-  e e. _V
105 104 71 opeldm 
 |-  ( <. e , f >. e. s -> e e. dom s )
106 105 adantl 
 |-  ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) -> e e. dom s )
107 106 adantr 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) /\ e =/= a ) -> e e. dom s )
108 101 103 107 rspcdva 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) /\ e =/= a ) -> -. e R a )
109 simpr 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) /\ e =/= a ) -> e =/= a )
110 109 neneqd 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) /\ e =/= a ) -> -. e = a )
111 ioran 
 |-  ( -. ( e R a \/ e = a ) <-> ( -. e R a /\ -. e = a ) )
112 108 110 111 sylanbrc 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) /\ e =/= a ) -> -. ( e R a \/ e = a ) )
113 112 intn3an1d 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) /\ e =/= a ) -> -. ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) )
114 99 113 pm2.61dane 
 |-  ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) -> -. ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) )
115 114 intn3an3d 
 |-  ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) -> -. ( ( e e. A /\ f e. B ) /\ ( a e. A /\ c e. B ) /\ ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) ) )
116 eleq1 
 |-  ( q = <. e , f >. -> ( q e. s <-> <. e , f >. e. s ) )
117 116 anbi2d 
 |-  ( q = <. e , f >. -> ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ q e. s ) <-> ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) ) )
118 breq1 
 |-  ( q = <. e , f >. -> ( q T <. a , c >. <-> <. e , f >. T <. a , c >. ) )
119 1 xpord2lem 
 |-  ( <. e , f >. T <. a , c >. <-> ( ( e e. A /\ f e. B ) /\ ( a e. A /\ c e. B ) /\ ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) ) )
120 118 119 bitrdi 
 |-  ( q = <. e , f >. -> ( q T <. a , c >. <-> ( ( e e. A /\ f e. B ) /\ ( a e. A /\ c e. B ) /\ ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) ) ) )
121 120 notbid 
 |-  ( q = <. e , f >. -> ( -. q T <. a , c >. <-> -. ( ( e e. A /\ f e. B ) /\ ( a e. A /\ c e. B ) /\ ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) ) ) )
122 117 121 imbi12d 
 |-  ( q = <. e , f >. -> ( ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ q e. s ) -> -. q T <. a , c >. ) <-> ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ <. e , f >. e. s ) -> -. ( ( e e. A /\ f e. B ) /\ ( a e. A /\ c e. B ) /\ ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) ) ) ) )
123 115 122 mpbiri 
 |-  ( q = <. e , f >. -> ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ q e. s ) -> -. q T <. a , c >. ) )
124 123 com12 
 |-  ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ q e. s ) -> ( q = <. e , f >. -> -. q T <. a , c >. ) )
125 124 exlimdvv 
 |-  ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ q e. s ) -> ( E. e E. f q = <. e , f >. -> -. q T <. a , c >. ) )
126 67 125 mpd 
 |-  ( ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) /\ q e. s ) -> -. q T <. a , c >. )
127 126 ralrimiva 
 |-  ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) -> A. q e. s -. q T <. a , c >. )
128 59 64 127 rspcedvdw 
 |-  ( ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) /\ ( c e. ( s " { a } ) /\ A. d e. ( s " { a } ) -. d S c ) ) -> E. p e. s A. q e. s -. q T p )
129 56 128 rexlimddv 
 |-  ( ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) /\ ( a e. dom s /\ A. b e. dom s -. b R a ) ) -> E. p e. s A. q e. s -. q T p )
130 30 129 rexlimddv 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> E. p e. s A. q e. s -. q T p )
131 130 ex 
 |-  ( ph -> ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> E. p e. s A. q e. s -. q T p ) )
132 131 alrimiv 
 |-  ( ph -> A. s ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> E. p e. s A. q e. s -. q T p ) )
133 df-fr 
 |-  ( T Fr ( A X. B ) <-> A. s ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> E. p e. s A. q e. s -. q T p ) )
134 132 133 sylibr 
 |-  ( ph -> T Fr ( A X. B ) )