Metamath Proof Explorer

Theorem frxp2

Description: Another way of giving a founded order to a cross 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 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 } ) )
58 vex 
 |-  a e. _V
59 vex 
 |-  c e. _V
60 58 59 elimasn 
 |-  ( c e. ( s " { a } ) <-> <. a , c >. e. s )
61 57 60 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 )
62 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 )
63 elrel 
 |-  ( ( Rel s /\ q e. s ) -> E. e E. f q = <. e , f >. )
64 62 63 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 >. )
65 breq1 
 |-  ( d = f -> ( d S c <-> f S c ) )
66 65 notbid 
 |-  ( d = f -> ( -. d S c <-> -. f S c ) )
67 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 )
68 vex 
 |-  f e. _V
69 58 68 elimasn 
 |-  ( f e. ( s " { a } ) <-> <. a , f >. e. s )
70 69 biimpri 
 |-  ( <. a , f >. e. s -> f e. ( s " { a } ) )
71 70 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 } ) )
72 66 67 71 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 )
73 72 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 ) )
74 opeq1 
 |-  ( e = a -> <. e , f >. = <. a , f >. )
75 74 eleq1d 
 |-  ( e = a -> ( <. e , f >. e. s <-> <. a , f >. e. s ) )
76 75 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 ) ) )
77 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 ) ) ) )
78 olc 
 |-  ( e = a -> ( e R a \/ e = a ) )
79 78 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 ) ) ) ) )
80 neeq1 
 |-  ( e = a -> ( e =/= a <-> a =/= a ) )
81 80 orbi1d 
 |-  ( e = a -> ( ( e =/= a \/ f =/= c ) <-> ( a =/= a \/ f =/= c ) ) )
82 neirr 
 |-  -. a =/= a
83 biorf 
 |-  ( -. a =/= a -> ( f =/= c <-> ( a =/= a \/ f =/= c ) ) )
84 82 83 ax-mp 
 |-  ( f =/= c <-> ( a =/= a \/ f =/= c ) )
85 81 84 bitr4di 
 |-  ( e = a -> ( ( e =/= a \/ f =/= c ) <-> f =/= c ) )
86 85 anbi2d 
 |-  ( e = a -> ( ( ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) <-> ( ( f S c \/ f = c ) /\ f =/= c ) ) )
87 andir 
 |-  ( ( ( f S c \/ f = c ) /\ f =/= c ) <-> ( ( f S c /\ f =/= c ) \/ ( f = c /\ f =/= c ) ) )
88 nonconne 
 |-  -. ( f = c /\ f =/= c )
89 88 biorfi 
 |-  ( ( f S c /\ f =/= c ) <-> ( ( f S c /\ f =/= c ) \/ ( f = c /\ f =/= c ) ) )
90 87 89 bitr4i 
 |-  ( ( ( f S c \/ f = c ) /\ f =/= c ) <-> ( f S c /\ f =/= c ) )
91 86 90 bitrdi 
 |-  ( e = a -> ( ( ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) <-> ( f S c /\ f =/= c ) ) )
92 79 91 bitr3d 
 |-  ( e = a -> ( ( ( e R a \/ e = a ) /\ ( ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) ) <-> ( f S c /\ f =/= c ) ) )
93 77 92 syl5bb 
 |-  ( e = a -> ( ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) <-> ( f S c /\ f =/= c ) ) )
94 93 notbid 
 |-  ( e = a -> ( -. ( ( e R a \/ e = a ) /\ ( f S c \/ f = c ) /\ ( e =/= a \/ f =/= c ) ) <-> -. ( f S c /\ f =/= c ) ) )
95 76 94 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 ) ) ) )
96 73 95 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 ) ) ) )
97 96 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 ) ) )
98 breq1 
 |-  ( b = e -> ( b R a <-> e R a ) )
99 98 notbid 
 |-  ( b = e -> ( -. b R a <-> -. e R a ) )
100 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 )
101 100 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 )
102 vex 
 |-  e e. _V
103 102 68 opeldm 
 |-  ( <. e , f >. e. s -> e e. dom s )
104 103 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 )
105 104 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 )
106 99 101 105 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 )
107 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 )
108 107 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 )
109 ioran 
 |-  ( -. ( e R a \/ e = a ) <-> ( -. e R a /\ -. e = a ) )
110 106 108 109 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 ) )
111 110 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 ) ) )
112 97 111 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 ) ) )
113 112 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 ) ) ) )
114 eleq1 
 |-  ( q = <. e , f >. -> ( q e. s <-> <. e , f >. e. s ) )
115 114 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 ) ) )
116 breq1 
 |-  ( q = <. e , f >. -> ( q T <. a , c >. <-> <. e , f >. T <. a , c >. ) )
117 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 ) ) ) )
118 116 117 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 ) ) ) ) )
119 118 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 ) ) ) ) )
120 115 119 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 ) ) ) ) ) )
121 113 120 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 >. ) )
122 121 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 >. ) )
123 122 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 >. ) )
124 64 123 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 >. )
125 124 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 >. )
126 breq2 
 |-  ( p = <. a , c >. -> ( q T p <-> q T <. a , c >. ) )
127 126 notbid 
 |-  ( p = <. a , c >. -> ( -. q T p <-> -. q T <. a , c >. ) )
128 127 ralbidv 
 |-  ( p = <. a , c >. -> ( A. q e. s -. q T p <-> A. q e. s -. q T <. a , c >. ) )
129 128 rspcev 
 |-  ( ( <. a , c >. e. s /\ A. q e. s -. q T <. a , c >. ) -> E. p e. s A. q e. s -. q T p )
130 61 125 129 syl2anc 
 |-  ( ( ( ( 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 )
131 56 130 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 )
132 30 131 rexlimddv 
 |-  ( ( ph /\ ( s C_ ( A X. B ) /\ s =/= (/) ) ) -> E. p e. s A. q e. s -. q T p )
133 132 ex 
 |-  ( ph -> ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> E. p e. s A. q e. s -. q T p ) )
134 133 alrimiv 
 |-  ( ph -> A. s ( ( s C_ ( A X. B ) /\ s =/= (/) ) -> E. p e. s A. q e. s -. q T p ) )
135 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 ) )
136 134 135 sylibr 
 |-  ( ph -> T Fr ( A X. B ) )