Metamath Proof Explorer

Theorem frxp3

Description: Give foundedness over a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Hypotheses xpord3.1 
|- U = { <. x , y >. | ( x e. ( ( A X. B ) X. C ) /\ y e. ( ( A X. B ) X. C ) /\ ( ( ( ( 1st ` ( 1st ` x ) ) R ( 1st ` ( 1st ` y ) ) \/ ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) ) /\ ( ( 2nd ` ( 1st ` x ) ) S ( 2nd ` ( 1st ` y ) ) \/ ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) ) /\ ( ( 2nd ` x ) T ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) ) /\ x =/= y ) ) }
frxp3.1 
|- ( ph -> R Fr A )
frxp3.2 
|- ( ph -> S Fr B )
frxp3.3 
|- ( ph -> T Fr C )
Assertion frxp3 
|- ( ph -> U Fr ( ( A X. B ) X. C ) )

Proof

Step Hyp Ref Expression
1 xpord3.1 
 |-  U = { <. x , y >. | ( x e. ( ( A X. B ) X. C ) /\ y e. ( ( A X. B ) X. C ) /\ ( ( ( ( 1st ` ( 1st ` x ) ) R ( 1st ` ( 1st ` y ) ) \/ ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) ) /\ ( ( 2nd ` ( 1st ` x ) ) S ( 2nd ` ( 1st ` y ) ) \/ ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) ) /\ ( ( 2nd ` x ) T ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) ) /\ x =/= y ) ) }
2 frxp3.1 
 |-  ( ph -> R Fr A )
3 frxp3.2 
 |-  ( ph -> S Fr B )
4 frxp3.3 
 |-  ( ph -> T Fr C )
5 dmss 
 |-  ( s C_ ( ( A X. B ) X. C ) -> dom s C_ dom ( ( A X. B ) X. C ) )
6 5 ad2antrl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> dom s C_ dom ( ( A X. B ) X. C ) )
7 dmxpss 
 |-  dom ( ( A X. B ) X. C ) C_ ( A X. B )
8 6 7 sstrdi 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> dom s C_ ( A X. B ) )
9 dmss 
 |-  ( dom s C_ ( A X. B ) -> dom dom s C_ dom ( A X. B ) )
10 8 9 syl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> dom dom s C_ dom ( A X. B ) )
11 dmxpss 
 |-  dom ( A X. B ) C_ A
12 10 11 sstrdi 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> dom dom s C_ A )
13 simprr 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> s =/= (/) )
14 simprl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> s C_ ( ( A X. B ) X. C ) )
15 relxp 
 |-  Rel ( ( A X. B ) X. C )
16 relss 
 |-  ( s C_ ( ( A X. B ) X. C ) -> ( Rel ( ( A X. B ) X. C ) -> Rel s ) )
17 14 15 16 mpisyl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> Rel s )
18 reldm0 
 |-  ( Rel s -> ( s = (/) <-> dom s = (/) ) )
19 17 18 syl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ( s = (/) <-> dom s = (/) ) )
20 19 necon3bid 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ( s =/= (/) <-> dom s =/= (/) ) )
21 13 20 mpbid 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> dom s =/= (/) )
22 relxp 
 |-  Rel ( A X. B )
23 relss 
 |-  ( dom s C_ ( A X. B ) -> ( Rel ( A X. B ) -> Rel dom s ) )
24 8 22 23 mpisyl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> Rel dom s )
25 reldm0 
 |-  ( Rel dom s -> ( dom s = (/) <-> dom dom s = (/) ) )
26 24 25 syl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ( dom s = (/) <-> dom dom s = (/) ) )
27 26 necon3bid 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ( dom s =/= (/) <-> dom dom s =/= (/) ) )
28 21 27 mpbid 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> dom dom s =/= (/) )
29 df-fr 
 |-  ( R Fr A <-> A. g ( ( g C_ A /\ g =/= (/) ) -> E. a e. g A. d e. g -. d R a ) )
30 2 29 sylib 
 |-  ( ph -> A. g ( ( g C_ A /\ g =/= (/) ) -> E. a e. g A. d e. g -. d R a ) )
31 30 adantr 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> A. g ( ( g C_ A /\ g =/= (/) ) -> E. a e. g A. d e. g -. d R a ) )
32 vex 
 |-  s e. _V
33 32 dmex 
 |-  dom s e. _V
34 33 dmex 
 |-  dom dom s e. _V
35 sseq1 
 |-  ( g = dom dom s -> ( g C_ A <-> dom dom s C_ A ) )
36 neeq1 
 |-  ( g = dom dom s -> ( g =/= (/) <-> dom dom s =/= (/) ) )
37 35 36 anbi12d 
 |-  ( g = dom dom s -> ( ( g C_ A /\ g =/= (/) ) <-> ( dom dom s C_ A /\ dom dom s =/= (/) ) ) )
38 raleq 
 |-  ( g = dom dom s -> ( A. d e. g -. d R a <-> A. d e. dom dom s -. d R a ) )
39 38 rexeqbi1dv 
 |-  ( g = dom dom s -> ( E. a e. g A. d e. g -. d R a <-> E. a e. dom dom s A. d e. dom dom s -. d R a ) )
40 37 39 imbi12d 
 |-  ( g = dom dom s -> ( ( ( g C_ A /\ g =/= (/) ) -> E. a e. g A. d e. g -. d R a ) <-> ( ( dom dom s C_ A /\ dom dom s =/= (/) ) -> E. a e. dom dom s A. d e. dom dom s -. d R a ) ) )
41 34 40 spcv 
 |-  ( A. g ( ( g C_ A /\ g =/= (/) ) -> E. a e. g A. d e. g -. d R a ) -> ( ( dom dom s C_ A /\ dom dom s =/= (/) ) -> E. a e. dom dom s A. d e. dom dom s -. d R a ) )
42 31 41 syl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ( ( dom dom s C_ A /\ dom dom s =/= (/) ) -> E. a e. dom dom s A. d e. dom dom s -. d R a ) )
43 12 28 42 mp2and 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> E. a e. dom dom s A. d e. dom dom s -. d R a )
44 imassrn 
 |-  ( dom s " { a } ) C_ ran dom s
45 rnss 
 |-  ( dom s C_ ( A X. B ) -> ran dom s C_ ran ( A X. B ) )
46 8 45 syl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ran dom s C_ ran ( A X. B ) )
47 rnxpss 
 |-  ran ( A X. B ) C_ B
48 46 47 sstrdi 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ran dom s C_ B )
49 48 adantr 
 |-  ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) -> ran dom s C_ B )
50 44 49 sstrid 
 |-  ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) -> ( dom s " { a } ) C_ B )
51 simprl 
 |-  ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) -> a e. dom dom s )
52 imadisj 
 |-  ( ( dom s " { a } ) = (/) <-> ( dom dom s i^i { a } ) = (/) )
53 disjsn 
 |-  ( ( dom dom s i^i { a } ) = (/) <-> -. a e. dom dom s )
54 52 53 bitri 
 |-  ( ( dom s " { a } ) = (/) <-> -. a e. dom dom s )
55 54 necon2abii 
 |-  ( a e. dom dom s <-> ( dom s " { a } ) =/= (/) )
56 51 55 sylib 
 |-  ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) -> ( dom s " { a } ) =/= (/) )
57 df-fr 
 |-  ( S Fr B <-> A. g ( ( g C_ B /\ g =/= (/) ) -> E. b e. g A. e e. g -. e S b ) )
58 3 57 sylib 
 |-  ( ph -> A. g ( ( g C_ B /\ g =/= (/) ) -> E. b e. g A. e e. g -. e S b ) )
59 33 imaex 
 |-  ( dom s " { a } ) e. _V
60 sseq1 
 |-  ( g = ( dom s " { a } ) -> ( g C_ B <-> ( dom s " { a } ) C_ B ) )
61 neeq1 
 |-  ( g = ( dom s " { a } ) -> ( g =/= (/) <-> ( dom s " { a } ) =/= (/) ) )
62 60 61 anbi12d 
 |-  ( g = ( dom s " { a } ) -> ( ( g C_ B /\ g =/= (/) ) <-> ( ( dom s " { a } ) C_ B /\ ( dom s " { a } ) =/= (/) ) ) )
63 raleq 
 |-  ( g = ( dom s " { a } ) -> ( A. e e. g -. e S b <-> A. e e. ( dom s " { a } ) -. e S b ) )
64 63 rexeqbi1dv 
 |-  ( g = ( dom s " { a } ) -> ( E. b e. g A. e e. g -. e S b <-> E. b e. ( dom s " { a } ) A. e e. ( dom s " { a } ) -. e S b ) )
65 62 64 imbi12d 
 |-  ( g = ( dom s " { a } ) -> ( ( ( g C_ B /\ g =/= (/) ) -> E. b e. g A. e e. g -. e S b ) <-> ( ( ( dom s " { a } ) C_ B /\ ( dom s " { a } ) =/= (/) ) -> E. b e. ( dom s " { a } ) A. e e. ( dom s " { a } ) -. e S b ) ) )
66 59 65 spcv 
 |-  ( A. g ( ( g C_ B /\ g =/= (/) ) -> E. b e. g A. e e. g -. e S b ) -> ( ( ( dom s " { a } ) C_ B /\ ( dom s " { a } ) =/= (/) ) -> E. b e. ( dom s " { a } ) A. e e. ( dom s " { a } ) -. e S b ) )
67 58 66 syl 
 |-  ( ph -> ( ( ( dom s " { a } ) C_ B /\ ( dom s " { a } ) =/= (/) ) -> E. b e. ( dom s " { a } ) A. e e. ( dom s " { a } ) -. e S b ) )
68 67 ad2antrr 
 |-  ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) -> ( ( ( dom s " { a } ) C_ B /\ ( dom s " { a } ) =/= (/) ) -> E. b e. ( dom s " { a } ) A. e e. ( dom s " { a } ) -. e S b ) )
69 50 56 68 mp2and 
 |-  ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) -> E. b e. ( dom s " { a } ) A. e e. ( dom s " { a } ) -. e S b )
70 imassrn 
 |-  ( s " { <. a , b >. } ) C_ ran s
71 rnss 
 |-  ( s C_ ( ( A X. B ) X. C ) -> ran s C_ ran ( ( A X. B ) X. C ) )
72 71 ad2antrl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ran s C_ ran ( ( A X. B ) X. C ) )
73 rnxpss 
 |-  ran ( ( A X. B ) X. C ) C_ C
74 72 73 sstrdi 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ran s C_ C )
75 70 74 sstrid 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ( s " { <. a , b >. } ) C_ C )
76 75 ad2antrr 
 |-  ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) -> ( s " { <. a , b >. } ) C_ C )
77 simprl 
 |-  ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) -> b e. ( dom s " { a } ) )
78 vex 
 |-  a e. _V
79 vex 
 |-  b e. _V
80 78 79 elimasn 
 |-  ( b e. ( dom s " { a } ) <-> <. a , b >. e. dom s )
81 77 80 sylib 
 |-  ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) -> <. a , b >. e. dom s )
82 imadisj 
 |-  ( ( s " { <. a , b >. } ) = (/) <-> ( dom s i^i { <. a , b >. } ) = (/) )
83 disjsn 
 |-  ( ( dom s i^i { <. a , b >. } ) = (/) <-> -. <. a , b >. e. dom s )
84 82 83 bitri 
 |-  ( ( s " { <. a , b >. } ) = (/) <-> -. <. a , b >. e. dom s )
85 84 necon2abii 
 |-  ( <. a , b >. e. dom s <-> ( s " { <. a , b >. } ) =/= (/) )
86 81 85 sylib 
 |-  ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) -> ( s " { <. a , b >. } ) =/= (/) )
87 df-fr 
 |-  ( T Fr C <-> A. g ( ( g C_ C /\ g =/= (/) ) -> E. c e. g A. f e. g -. f T c ) )
88 4 87 sylib 
 |-  ( ph -> A. g ( ( g C_ C /\ g =/= (/) ) -> E. c e. g A. f e. g -. f T c ) )
89 32 imaex 
 |-  ( s " { <. a , b >. } ) e. _V
90 sseq1 
 |-  ( g = ( s " { <. a , b >. } ) -> ( g C_ C <-> ( s " { <. a , b >. } ) C_ C ) )
91 neeq1 
 |-  ( g = ( s " { <. a , b >. } ) -> ( g =/= (/) <-> ( s " { <. a , b >. } ) =/= (/) ) )
92 90 91 anbi12d 
 |-  ( g = ( s " { <. a , b >. } ) -> ( ( g C_ C /\ g =/= (/) ) <-> ( ( s " { <. a , b >. } ) C_ C /\ ( s " { <. a , b >. } ) =/= (/) ) ) )
93 raleq 
 |-  ( g = ( s " { <. a , b >. } ) -> ( A. f e. g -. f T c <-> A. f e. ( s " { <. a , b >. } ) -. f T c ) )
94 93 rexeqbi1dv 
 |-  ( g = ( s " { <. a , b >. } ) -> ( E. c e. g A. f e. g -. f T c <-> E. c e. ( s " { <. a , b >. } ) A. f e. ( s " { <. a , b >. } ) -. f T c ) )
95 92 94 imbi12d 
 |-  ( g = ( s " { <. a , b >. } ) -> ( ( ( g C_ C /\ g =/= (/) ) -> E. c e. g A. f e. g -. f T c ) <-> ( ( ( s " { <. a , b >. } ) C_ C /\ ( s " { <. a , b >. } ) =/= (/) ) -> E. c e. ( s " { <. a , b >. } ) A. f e. ( s " { <. a , b >. } ) -. f T c ) ) )
96 89 95 spcv 
 |-  ( A. g ( ( g C_ C /\ g =/= (/) ) -> E. c e. g A. f e. g -. f T c ) -> ( ( ( s " { <. a , b >. } ) C_ C /\ ( s " { <. a , b >. } ) =/= (/) ) -> E. c e. ( s " { <. a , b >. } ) A. f e. ( s " { <. a , b >. } ) -. f T c ) )
97 88 96 syl 
 |-  ( ph -> ( ( ( s " { <. a , b >. } ) C_ C /\ ( s " { <. a , b >. } ) =/= (/) ) -> E. c e. ( s " { <. a , b >. } ) A. f e. ( s " { <. a , b >. } ) -. f T c ) )
98 97 ad3antrrr 
 |-  ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) -> ( ( ( s " { <. a , b >. } ) C_ C /\ ( s " { <. a , b >. } ) =/= (/) ) -> E. c e. ( s " { <. a , b >. } ) A. f e. ( s " { <. a , b >. } ) -. f T c ) )
99 76 86 98 mp2and 
 |-  ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) -> E. c e. ( s " { <. a , b >. } ) A. f e. ( s " { <. a , b >. } ) -. f T c )
100 simprl 
 |-  ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) -> c e. ( s " { <. a , b >. } ) )
101 opex 
 |-  <. a , b >. e. _V
102 vex 
 |-  c e. _V
103 101 102 elimasn 
 |-  ( c e. ( s " { <. a , b >. } ) <-> <. <. a , b >. , c >. e. s )
104 100 103 sylib 
 |-  ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) -> <. <. a , b >. , c >. e. s )
105 simplrl 
 |-  ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) -> s C_ ( ( A X. B ) X. C ) )
106 105 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) -> s C_ ( ( A X. B ) X. C ) )
107 elxpxpss 
 |-  ( ( s C_ ( ( A X. B ) X. C ) /\ q e. s ) -> E. g E. h E. i q = <. <. g , h >. , i >. )
108 106 107 sylan 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ q e. s ) -> E. g E. h E. i q = <. <. g , h >. , i >. )
109 df-ne 
 |-  ( i =/= c <-> -. i = c )
110 109 con2bii 
 |-  ( i = c <-> -. i =/= c )
111 110 biimpi 
 |-  ( i = c -> -. i =/= c )
112 111 adantl 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) /\ i = c ) -> -. i =/= c )
113 112 intnand 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) /\ i = c ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ i =/= c ) )
114 breq1 
 |-  ( f = i -> ( f T c <-> i T c ) )
115 114 notbid 
 |-  ( f = i -> ( -. f T c <-> -. i T c ) )
116 simplrr 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) -> A. f e. ( s " { <. a , b >. } ) -. f T c )
117 116 adantr 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) /\ i =/= c ) -> A. f e. ( s " { <. a , b >. } ) -. f T c )
118 simplr 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) /\ i =/= c ) -> <. <. a , b >. , i >. e. s )
119 vex 
 |-  i e. _V
120 101 119 elimasn 
 |-  ( i e. ( s " { <. a , b >. } ) <-> <. <. a , b >. , i >. e. s )
121 118 120 sylibr 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) /\ i =/= c ) -> i e. ( s " { <. a , b >. } ) )
122 115 117 121 rspcdva 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) /\ i =/= c ) -> -. i T c )
123 simpr 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) /\ i =/= c ) -> i =/= c )
124 123 neneqd 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) /\ i =/= c ) -> -. i = c )
125 ioran 
 |-  ( -. ( i T c \/ i = c ) <-> ( -. i T c /\ -. i = c ) )
126 122 124 125 sylanbrc 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) /\ i =/= c ) -> -. ( i T c \/ i = c ) )
127 126 intn3an3d 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) /\ i =/= c ) -> -. ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) )
128 127 intnanrd 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) /\ i =/= c ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ i =/= c ) )
129 113 128 pm2.61dane 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ i =/= c ) )
130 opeq2 
 |-  ( h = b -> <. a , h >. = <. a , b >. )
131 130 opeq1d 
 |-  ( h = b -> <. <. a , h >. , i >. = <. <. a , b >. , i >. )
132 131 eleq1d 
 |-  ( h = b -> ( <. <. a , h >. , i >. e. s <-> <. <. a , b >. , i >. e. s ) )
133 132 anbi2d 
 |-  ( h = b -> ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) <-> ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) ) )
134 neeq1 
 |-  ( h = b -> ( h =/= b <-> b =/= b ) )
135 134 orbi1d 
 |-  ( h = b -> ( ( h =/= b \/ i =/= c ) <-> ( b =/= b \/ i =/= c ) ) )
136 neirr 
 |-  -. b =/= b
137 orel1 
 |-  ( -. b =/= b -> ( ( b =/= b \/ i =/= c ) -> i =/= c ) )
138 136 137 ax-mp 
 |-  ( ( b =/= b \/ i =/= c ) -> i =/= c )
139 olc 
 |-  ( i =/= c -> ( b =/= b \/ i =/= c ) )
140 138 139 impbii 
 |-  ( ( b =/= b \/ i =/= c ) <-> i =/= c )
141 135 140 bitrdi 
 |-  ( h = b -> ( ( h =/= b \/ i =/= c ) <-> i =/= c ) )
142 141 anbi2d 
 |-  ( h = b -> ( ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( h =/= b \/ i =/= c ) ) <-> ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ i =/= c ) ) )
143 142 notbid 
 |-  ( h = b -> ( -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( h =/= b \/ i =/= c ) ) <-> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ i =/= c ) ) )
144 133 143 imbi12d 
 |-  ( h = b -> ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( h =/= b \/ i =/= c ) ) ) <-> ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , b >. , i >. e. s ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ i =/= c ) ) ) )
145 129 144 mpbiri 
 |-  ( h = b -> ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( h =/= b \/ i =/= c ) ) ) )
146 145 impcom 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) /\ h = b ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( h =/= b \/ i =/= c ) ) )
147 breq1 
 |-  ( e = h -> ( e S b <-> h S b ) )
148 147 notbid 
 |-  ( e = h -> ( -. e S b <-> -. h S b ) )
149 simplrr 
 |-  ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) -> A. e e. ( dom s " { a } ) -. e S b )
150 149 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) /\ h =/= b ) -> A. e e. ( dom s " { a } ) -. e S b )
151 opex 
 |-  <. a , h >. e. _V
152 151 119 opeldm 
 |-  ( <. <. a , h >. , i >. e. s -> <. a , h >. e. dom s )
153 152 adantl 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) -> <. a , h >. e. dom s )
154 153 adantr 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) /\ h =/= b ) -> <. a , h >. e. dom s )
155 vex 
 |-  h e. _V
156 78 155 elimasn 
 |-  ( h e. ( dom s " { a } ) <-> <. a , h >. e. dom s )
157 154 156 sylibr 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) /\ h =/= b ) -> h e. ( dom s " { a } ) )
158 148 150 157 rspcdva 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) /\ h =/= b ) -> -. h S b )
159 simpr 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) /\ h =/= b ) -> h =/= b )
160 159 neneqd 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) /\ h =/= b ) -> -. h = b )
161 ioran 
 |-  ( -. ( h S b \/ h = b ) <-> ( -. h S b /\ -. h = b ) )
162 158 160 161 sylanbrc 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) /\ h =/= b ) -> -. ( h S b \/ h = b ) )
163 162 intn3an2d 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) /\ h =/= b ) -> -. ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) )
164 163 intnanrd 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) /\ h =/= b ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( h =/= b \/ i =/= c ) ) )
165 146 164 pm2.61dane 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( h =/= b \/ i =/= c ) ) )
166 opeq1 
 |-  ( g = a -> <. g , h >. = <. a , h >. )
167 166 opeq1d 
 |-  ( g = a -> <. <. g , h >. , i >. = <. <. a , h >. , i >. )
168 167 eleq1d 
 |-  ( g = a -> ( <. <. g , h >. , i >. e. s <-> <. <. a , h >. , i >. e. s ) )
169 168 anbi2d 
 |-  ( g = a -> ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) <-> ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) ) )
170 3orass 
 |-  ( ( g =/= a \/ h =/= b \/ i =/= c ) <-> ( g =/= a \/ ( h =/= b \/ i =/= c ) ) )
171 neeq1 
 |-  ( g = a -> ( g =/= a <-> a =/= a ) )
172 171 orbi1d 
 |-  ( g = a -> ( ( g =/= a \/ ( h =/= b \/ i =/= c ) ) <-> ( a =/= a \/ ( h =/= b \/ i =/= c ) ) ) )
173 170 172 syl5bb 
 |-  ( g = a -> ( ( g =/= a \/ h =/= b \/ i =/= c ) <-> ( a =/= a \/ ( h =/= b \/ i =/= c ) ) ) )
174 neirr 
 |-  -. a =/= a
175 orel1 
 |-  ( -. a =/= a -> ( ( a =/= a \/ ( h =/= b \/ i =/= c ) ) -> ( h =/= b \/ i =/= c ) ) )
176 174 175 ax-mp 
 |-  ( ( a =/= a \/ ( h =/= b \/ i =/= c ) ) -> ( h =/= b \/ i =/= c ) )
177 olc 
 |-  ( ( h =/= b \/ i =/= c ) -> ( a =/= a \/ ( h =/= b \/ i =/= c ) ) )
178 176 177 impbii 
 |-  ( ( a =/= a \/ ( h =/= b \/ i =/= c ) ) <-> ( h =/= b \/ i =/= c ) )
179 173 178 bitrdi 
 |-  ( g = a -> ( ( g =/= a \/ h =/= b \/ i =/= c ) <-> ( h =/= b \/ i =/= c ) ) )
180 179 anbi2d 
 |-  ( g = a -> ( ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( g =/= a \/ h =/= b \/ i =/= c ) ) <-> ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( h =/= b \/ i =/= c ) ) ) )
181 180 notbid 
 |-  ( g = a -> ( -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( g =/= a \/ h =/= b \/ i =/= c ) ) <-> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( h =/= b \/ i =/= c ) ) ) )
182 169 181 imbi12d 
 |-  ( g = a -> ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( g =/= a \/ h =/= b \/ i =/= c ) ) ) <-> ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. a , h >. , i >. e. s ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( h =/= b \/ i =/= c ) ) ) ) )
183 165 182 mpbiri 
 |-  ( g = a -> ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( g =/= a \/ h =/= b \/ i =/= c ) ) ) )
184 183 impcom 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) /\ g = a ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( g =/= a \/ h =/= b \/ i =/= c ) ) )
185 breq1 
 |-  ( d = g -> ( d R a <-> g R a ) )
186 185 notbid 
 |-  ( d = g -> ( -. d R a <-> -. g R a ) )
187 simplrr 
 |-  ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) -> A. d e. dom dom s -. d R a )
188 187 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) /\ g =/= a ) -> A. d e. dom dom s -. d R a )
189 opex 
 |-  <. g , h >. e. _V
190 189 119 opeldm 
 |-  ( <. <. g , h >. , i >. e. s -> <. g , h >. e. dom s )
191 190 adantl 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) -> <. g , h >. e. dom s )
192 vex 
 |-  g e. _V
193 192 155 opeldm 
 |-  ( <. g , h >. e. dom s -> g e. dom dom s )
194 191 193 syl 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) -> g e. dom dom s )
195 194 adantr 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) /\ g =/= a ) -> g e. dom dom s )
196 186 188 195 rspcdva 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) /\ g =/= a ) -> -. g R a )
197 simpr 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) /\ g =/= a ) -> g =/= a )
198 197 neneqd 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) /\ g =/= a ) -> -. g = a )
199 ioran 
 |-  ( -. ( g R a \/ g = a ) <-> ( -. g R a /\ -. g = a ) )
200 196 198 199 sylanbrc 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) /\ g =/= a ) -> -. ( g R a \/ g = a ) )
201 200 intn3an1d 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) /\ g =/= a ) -> -. ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) )
202 201 intnanrd 
 |-  ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) /\ g =/= a ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( g =/= a \/ h =/= b \/ i =/= c ) ) )
203 184 202 pm2.61dane 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( g =/= a \/ h =/= b \/ i =/= c ) ) )
204 203 intn3an3d 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) -> -. ( ( g e. A /\ h e. B /\ i e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( g =/= a \/ h =/= b \/ i =/= c ) ) ) )
205 eleq1 
 |-  ( q = <. <. g , h >. , i >. -> ( q e. s <-> <. <. g , h >. , i >. e. s ) )
206 205 anbi2d 
 |-  ( q = <. <. g , h >. , i >. -> ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ q e. s ) <-> ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) ) )
207 breq1 
 |-  ( q = <. <. g , h >. , i >. -> ( q U <. <. a , b >. , c >. <-> <. <. g , h >. , i >. U <. <. a , b >. , c >. ) )
208 1 xpord3lem 
 |-  ( <. <. g , h >. , i >. U <. <. a , b >. , c >. <-> ( ( g e. A /\ h e. B /\ i e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( g =/= a \/ h =/= b \/ i =/= c ) ) ) )
209 207 208 bitrdi 
 |-  ( q = <. <. g , h >. , i >. -> ( q U <. <. a , b >. , c >. <-> ( ( g e. A /\ h e. B /\ i e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( g =/= a \/ h =/= b \/ i =/= c ) ) ) ) )
210 209 notbid 
 |-  ( q = <. <. g , h >. , i >. -> ( -. q U <. <. a , b >. , c >. <-> -. ( ( g e. A /\ h e. B /\ i e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( g =/= a \/ h =/= b \/ i =/= c ) ) ) ) )
211 206 210 imbi12d 
 |-  ( q = <. <. g , h >. , i >. -> ( ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ q e. s ) -> -. q U <. <. a , b >. , c >. ) <-> ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ <. <. g , h >. , i >. e. s ) -> -. ( ( g e. A /\ h e. B /\ i e. C ) /\ ( a e. A /\ b e. B /\ c e. C ) /\ ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ ( g =/= a \/ h =/= b \/ i =/= c ) ) ) ) ) )
212 204 211 mpbiri 
 |-  ( q = <. <. g , h >. , i >. -> ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ q e. s ) -> -. q U <. <. a , b >. , c >. ) )
213 212 com12 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ q e. s ) -> ( q = <. <. g , h >. , i >. -> -. q U <. <. a , b >. , c >. ) )
214 213 exlimdv 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ q e. s ) -> ( E. i q = <. <. g , h >. , i >. -> -. q U <. <. a , b >. , c >. ) )
215 214 exlimdvv 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ q e. s ) -> ( E. g E. h E. i q = <. <. g , h >. , i >. -> -. q U <. <. a , b >. , c >. ) )
216 108 215 mpd 
 |-  ( ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) /\ q e. s ) -> -. q U <. <. a , b >. , c >. )
217 216 ralrimiva 
 |-  ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) -> A. q e. s -. q U <. <. a , b >. , c >. )
218 breq2 
 |-  ( p = <. <. a , b >. , c >. -> ( q U p <-> q U <. <. a , b >. , c >. ) )
219 218 notbid 
 |-  ( p = <. <. a , b >. , c >. -> ( -. q U p <-> -. q U <. <. a , b >. , c >. ) )
220 219 ralbidv 
 |-  ( p = <. <. a , b >. , c >. -> ( A. q e. s -. q U p <-> A. q e. s -. q U <. <. a , b >. , c >. ) )
221 220 rspcev 
 |-  ( ( <. <. a , b >. , c >. e. s /\ A. q e. s -. q U <. <. a , b >. , c >. ) -> E. p e. s A. q e. s -. q U p )
222 104 217 221 syl2anc 
 |-  ( ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) /\ ( c e. ( s " { <. a , b >. } ) /\ A. f e. ( s " { <. a , b >. } ) -. f T c ) ) -> E. p e. s A. q e. s -. q U p )
223 99 222 rexlimddv 
 |-  ( ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) /\ ( b e. ( dom s " { a } ) /\ A. e e. ( dom s " { a } ) -. e S b ) ) -> E. p e. s A. q e. s -. q U p )
224 69 223 rexlimddv 
 |-  ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) -> E. p e. s A. q e. s -. q U p )
225 43 224 rexlimddv 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> E. p e. s A. q e. s -. q U p )
226 225 ex 
 |-  ( ph -> ( ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) -> E. p e. s A. q e. s -. q U p ) )
227 226 alrimiv 
 |-  ( ph -> A. s ( ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) -> E. p e. s A. q e. s -. q U p ) )
228 df-fr 
 |-  ( U Fr ( ( A X. B ) X. C ) <-> A. s ( ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) -> E. p e. s A. q e. s -. q U p ) )
229 227 228 sylibr 
 |-  ( ph -> U Fr ( ( A X. B ) X. C ) )