Metamath Proof Explorer

Theorem frxp3

Description: Give well-foundedness over a triple Cartesian 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 2 adantr 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> R Fr A )
6 dmss 
 |-  ( s C_ ( ( A X. B ) X. C ) -> dom s C_ dom ( ( A X. B ) X. C ) )
7 6 ad2antrl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> dom s C_ dom ( ( A X. B ) X. C ) )
8 dmxpss 
 |-  dom ( ( A X. B ) X. C ) C_ ( A X. B )
9 7 8 sstrdi 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> dom s C_ ( A X. B ) )
10 dmss 
 |-  ( dom s C_ ( A X. B ) -> dom dom s C_ dom ( A X. B ) )
11 9 10 syl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> dom dom s C_ dom ( A X. B ) )
12 dmxpss 
 |-  dom ( A X. B ) C_ A
13 11 12 sstrdi 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> dom dom s C_ A )
14 vex 
 |-  s e. _V
15 14 dmex 
 |-  dom s e. _V
16 15 dmex 
 |-  dom dom s e. _V
17 16 a1i 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> dom dom s e. _V )
18 relxp 
 |-  Rel ( ( A X. B ) X. C )
19 relss 
 |-  ( s C_ ( ( A X. B ) X. C ) -> ( Rel ( ( A X. B ) X. C ) -> Rel s ) )
20 18 19 mpi 
 |-  ( s C_ ( ( A X. B ) X. C ) -> Rel s )
21 20 adantl 
 |-  ( ( ph /\ s C_ ( ( A X. B ) X. C ) ) -> Rel s )
22 reldm0 
 |-  ( Rel s -> ( s = (/) <-> dom s = (/) ) )
23 21 22 syl 
 |-  ( ( ph /\ s C_ ( ( A X. B ) X. C ) ) -> ( s = (/) <-> dom s = (/) ) )
24 relxp 
 |-  Rel ( A X. B )
25 relss 
 |-  ( dom ( ( A X. B ) X. C ) C_ ( A X. B ) -> ( Rel ( A X. B ) -> Rel dom ( ( A X. B ) X. C ) ) )
26 8 24 25 mp2 
 |-  Rel dom ( ( A X. B ) X. C )
27 relss 
 |-  ( dom s C_ dom ( ( A X. B ) X. C ) -> ( Rel dom ( ( A X. B ) X. C ) -> Rel dom s ) )
28 6 26 27 mpisyl 
 |-  ( s C_ ( ( A X. B ) X. C ) -> Rel dom s )
29 28 adantl 
 |-  ( ( ph /\ s C_ ( ( A X. B ) X. C ) ) -> Rel dom s )
30 reldm0 
 |-  ( Rel dom s -> ( dom s = (/) <-> dom dom s = (/) ) )
31 29 30 syl 
 |-  ( ( ph /\ s C_ ( ( A X. B ) X. C ) ) -> ( dom s = (/) <-> dom dom s = (/) ) )
32 23 31 bitrd 
 |-  ( ( ph /\ s C_ ( ( A X. B ) X. C ) ) -> ( s = (/) <-> dom dom s = (/) ) )
33 32 necon3bid 
 |-  ( ( ph /\ s C_ ( ( A X. B ) X. C ) ) -> ( s =/= (/) <-> dom dom s =/= (/) ) )
34 33 biimpa 
 |-  ( ( ( ph /\ s C_ ( ( A X. B ) X. C ) ) /\ s =/= (/) ) -> dom dom s =/= (/) )
35 34 anasss 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> dom dom s =/= (/) )
36 5 13 17 35 frd 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> E. a e. dom dom s A. d e. dom dom s -. d R a )
37 3 ad2antrr 
 |-  ( ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) /\ ( a e. dom dom s /\ A. d e. dom dom s -. d R a ) ) -> S Fr B )
38 imassrn 
 |-  ( dom s " { a } ) C_ ran dom s
39 rnss 
 |-  ( dom s C_ ( A X. B ) -> ran dom s C_ ran ( A X. B ) )
40 9 39 syl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ran dom s C_ ran ( A X. B ) )
41 rnxpss 
 |-  ran ( A X. B ) C_ B
42 40 41 sstrdi 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ran dom s C_ B )
43 38 42 sstrid 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ( dom s " { a } ) C_ B )
44 43 adantr 
 |-  ( ( ( 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 )
45 15 imaex 
 |-  ( dom s " { a } ) e. _V
46 45 a1i 
 |-  ( ( ( 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 } ) e. _V )
47 imadisj 
 |-  ( ( dom s " { a } ) = (/) <-> ( dom dom s i^i { a } ) = (/) )
48 disjsn 
 |-  ( ( dom dom s i^i { a } ) = (/) <-> -. a e. dom dom s )
49 47 48 bitri 
 |-  ( ( dom s " { a } ) = (/) <-> -. a e. dom dom s )
50 49 necon2abii 
 |-  ( a e. dom dom s <-> ( dom s " { a } ) =/= (/) )
51 50 biimpi 
 |-  ( a e. dom dom s -> ( dom s " { a } ) =/= (/) )
52 51 ad2antrl 
 |-  ( ( ( 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 } ) =/= (/) )
53 37 44 46 52 frd 
 |-  ( ( ( 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 )
54 4 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 ) ) -> T Fr C )
55 imassrn 
 |-  ( s " { <. a , b >. } ) C_ ran s
56 rnss 
 |-  ( s C_ ( ( A X. B ) X. C ) -> ran s C_ ran ( ( A X. B ) X. C ) )
57 56 ad2antrl 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ran s C_ ran ( ( A X. B ) X. C ) )
58 rnxpss 
 |-  ran ( ( A X. B ) X. C ) C_ C
59 57 58 sstrdi 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ran s C_ C )
60 55 59 sstrid 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> ( s " { <. a , b >. } ) C_ C )
61 60 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 )
62 14 imaex 
 |-  ( s " { <. a , b >. } ) e. _V
63 62 a1i 
 |-  ( ( ( ( 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 >. } ) e. _V )
64 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 } ) )
65 vex 
 |-  a e. _V
66 vex 
 |-  b e. _V
67 65 66 elimasn 
 |-  ( b e. ( dom s " { a } ) <-> <. a , b >. e. dom s )
68 64 67 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 )
69 imadisj 
 |-  ( ( s " { <. a , b >. } ) = (/) <-> ( dom s i^i { <. a , b >. } ) = (/) )
70 disjsn 
 |-  ( ( dom s i^i { <. a , b >. } ) = (/) <-> -. <. a , b >. e. dom s )
71 69 70 bitri 
 |-  ( ( s " { <. a , b >. } ) = (/) <-> -. <. a , b >. e. dom s )
72 71 necon2abii 
 |-  ( <. a , b >. e. dom s <-> ( s " { <. a , b >. } ) =/= (/) )
73 68 72 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 >. } ) =/= (/) )
74 54 61 63 73 frd 
 |-  ( ( ( ( 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 )
75 df-ot 
 |-  <. a , b , c >. = <. <. a , b >. , c >.
76 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 >. } ) )
77 opex 
 |-  <. a , b >. e. _V
78 vex 
 |-  c e. _V
79 77 78 elimasn 
 |-  ( c e. ( s " { <. a , b >. } ) <-> <. <. a , b >. , c >. e. s )
80 76 79 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 )
81 75 80 eqeltrid 
 |-  ( ( ( ( ( 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 )
82 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 ) )
83 82 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 ) )
84 el2xpss 
 |-  ( ( q e. s /\ s C_ ( ( A X. B ) X. C ) ) -> E. g E. h E. i q = <. g , h , i >. )
85 84 ancoms 
 |-  ( ( s C_ ( ( A X. B ) X. C ) /\ q e. s ) -> E. g E. h E. i q = <. g , h , i >. )
86 83 85 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 >. )
87 df-ne 
 |-  ( i =/= c <-> -. i = c )
88 87 con2bii 
 |-  ( i = c <-> -. i =/= c )
89 88 biimpi 
 |-  ( i = c -> -. i =/= c )
90 89 intnand 
 |-  ( i = c -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ i =/= c ) )
91 90 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 ) -> -. ( ( ( g R a \/ g = a ) /\ ( h S b \/ h = b ) /\ ( i T c \/ i = c ) ) /\ i =/= c ) )
92 breq1 
 |-  ( f = i -> ( f T c <-> i T c ) )
93 92 notbid 
 |-  ( f = i -> ( -. f T c <-> -. i T c ) )
94 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 )
95 94 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 )
96 df-ot 
 |-  <. a , b , i >. = <. <. a , b >. , i >.
97 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 )
98 96 97 eqeltrrid 
 |-  ( ( ( ( ( ( ( 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 )
99 vex 
 |-  i e. _V
100 77 99 elimasn 
 |-  ( i e. ( s " { <. a , b >. } ) <-> <. <. a , b >. , i >. e. s )
101 98 100 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 >. } ) )
102 93 95 101 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 )
103 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 )
104 103 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 )
105 ioran 
 |-  ( -. ( i T c \/ i = c ) <-> ( -. i T c /\ -. i = c ) )
106 102 104 105 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 ) )
107 106 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 ) ) )
108 107 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 ) )
109 91 108 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 ) )
110 oteq2 
 |-  ( h = b -> <. a , h , i >. = <. a , b , i >. )
111 110 eleq1d 
 |-  ( h = b -> ( <. a , h , i >. e. s <-> <. a , b , i >. e. s ) )
112 111 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 ) ) )
113 neeq1 
 |-  ( h = b -> ( h =/= b <-> b =/= b ) )
114 113 orbi1d 
 |-  ( h = b -> ( ( h =/= b \/ i =/= c ) <-> ( b =/= b \/ i =/= c ) ) )
115 neirr 
 |-  -. b =/= b
116 orel1 
 |-  ( -. b =/= b -> ( ( b =/= b \/ i =/= c ) -> i =/= c ) )
117 115 116 ax-mp 
 |-  ( ( b =/= b \/ i =/= c ) -> i =/= c )
118 olc 
 |-  ( i =/= c -> ( b =/= b \/ i =/= c ) )
119 117 118 impbii 
 |-  ( ( b =/= b \/ i =/= c ) <-> i =/= c )
120 114 119 bitrdi 
 |-  ( h = b -> ( ( h =/= b \/ i =/= c ) <-> i =/= c ) )
121 120 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 ) ) )
122 121 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 ) ) )
123 112 122 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 ) ) ) )
124 109 123 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 ) ) ) )
125 124 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 ) ) )
126 breq1 
 |-  ( e = h -> ( e S b <-> h S b ) )
127 126 notbid 
 |-  ( e = h -> ( -. e S b <-> -. h S b ) )
128 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 )
129 128 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 )
130 df-ot 
 |-  <. a , h , i >. = <. <. a , h >. , i >.
131 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 , h , i >. e. s ) /\ h =/= b ) -> <. a , h , i >. e. s )
132 130 131 eqeltrrid 
 |-  ( ( ( ( ( ( ( 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 >. , i >. e. s )
133 opex 
 |-  <. a , h >. e. _V
134 133 99 opeldm 
 |-  ( <. <. a , h >. , i >. e. s -> <. a , h >. e. dom s )
135 132 134 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 ) ) /\ <. a , h , i >. e. s ) /\ h =/= b ) -> <. a , h >. e. dom s )
136 vex 
 |-  h e. _V
137 65 136 elimasn 
 |-  ( h e. ( dom s " { a } ) <-> <. a , h >. e. dom s )
138 135 137 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 } ) )
139 127 129 138 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 )
140 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 )
141 140 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 )
142 ioran 
 |-  ( -. ( h S b \/ h = b ) <-> ( -. h S b /\ -. h = b ) )
143 139 141 142 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 ) )
144 143 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 ) ) )
145 144 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 ) ) )
146 125 145 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 ) ) )
147 oteq1 
 |-  ( g = a -> <. g , h , i >. = <. a , h , i >. )
148 147 eleq1d 
 |-  ( g = a -> ( <. g , h , i >. e. s <-> <. a , h , i >. e. s ) )
149 148 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 ) ) )
150 neeq1 
 |-  ( g = a -> ( g =/= a <-> a =/= a ) )
151 biidd 
 |-  ( g = a -> ( h =/= b <-> h =/= b ) )
152 biidd 
 |-  ( g = a -> ( i =/= c <-> i =/= c ) )
153 150 151 152 3orbi123d 
 |-  ( g = a -> ( ( g =/= a \/ h =/= b \/ i =/= c ) <-> ( a =/= a \/ h =/= b \/ i =/= c ) ) )
154 3orass 
 |-  ( ( a =/= a \/ h =/= b \/ i =/= c ) <-> ( a =/= a \/ ( h =/= b \/ i =/= c ) ) )
155 neirr 
 |-  -. a =/= a
156 orel1 
 |-  ( -. a =/= a -> ( ( a =/= a \/ ( h =/= b \/ i =/= c ) ) -> ( h =/= b \/ i =/= c ) ) )
157 155 156 ax-mp 
 |-  ( ( a =/= a \/ ( h =/= b \/ i =/= c ) ) -> ( h =/= b \/ i =/= c ) )
158 olc 
 |-  ( ( h =/= b \/ i =/= c ) -> ( a =/= a \/ ( h =/= b \/ i =/= c ) ) )
159 157 158 impbii 
 |-  ( ( a =/= a \/ ( h =/= b \/ i =/= c ) ) <-> ( h =/= b \/ i =/= c ) )
160 154 159 bitri 
 |-  ( ( a =/= a \/ h =/= b \/ i =/= c ) <-> ( h =/= b \/ i =/= c ) )
161 153 160 bitrdi 
 |-  ( g = a -> ( ( g =/= a \/ h =/= b \/ i =/= c ) <-> ( h =/= b \/ i =/= c ) ) )
162 161 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 ) ) ) )
163 162 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 ) ) ) )
164 149 163 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 ) ) ) ) )
165 146 164 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 ) ) ) )
166 165 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 ) ) )
167 breq1 
 |-  ( d = g -> ( d R a <-> g R a ) )
168 167 notbid 
 |-  ( d = g -> ( -. d R a <-> -. g R a ) )
169 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 )
170 169 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 )
171 df-ot 
 |-  <. g , h , i >. = <. <. g , h >. , i >.
172 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 ) ) /\ <. g , h , i >. e. s ) /\ g =/= a ) -> <. g , h , i >. e. s )
173 171 172 eqeltrrid 
 |-  ( ( ( ( ( ( ( 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 , h >. , i >. e. s )
174 opex 
 |-  <. g , h >. e. _V
175 174 99 opeldm 
 |-  ( <. <. g , h >. , i >. e. s -> <. g , h >. e. dom s )
176 vex 
 |-  g e. _V
177 176 136 opeldm 
 |-  ( <. g , h >. e. dom s -> g e. dom dom s )
178 173 175 177 3syl 
 |-  ( ( ( ( ( ( ( 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 )
179 168 170 178 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 )
180 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 )
181 180 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 )
182 ioran 
 |-  ( -. ( g R a \/ g = a ) <-> ( -. g R a /\ -. g = a ) )
183 179 181 182 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 ) )
184 183 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 ) ) )
185 184 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 ) ) )
186 166 185 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 ) ) )
187 186 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 ) ) ) )
188 eleq1 
 |-  ( q = <. g , h , i >. -> ( q e. s <-> <. g , h , i >. e. s ) )
189 188 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 ) ) )
190 breq1 
 |-  ( q = <. g , h , i >. -> ( q U <. a , b , c >. <-> <. g , h , i >. U <. a , b , c >. ) )
191 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 ) ) ) )
192 190 191 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 ) ) ) ) )
193 192 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 ) ) ) ) )
194 189 193 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 ) ) ) ) ) )
195 187 194 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 >. ) )
196 195 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 >. ) )
197 196 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 >. ) )
198 197 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 >. ) )
199 86 198 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 >. )
200 199 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 >. )
201 breq2 
 |-  ( p = <. a , b , c >. -> ( q U p <-> q U <. a , b , c >. ) )
202 201 notbid 
 |-  ( p = <. a , b , c >. -> ( -. q U p <-> -. q U <. a , b , c >. ) )
203 202 ralbidv 
 |-  ( p = <. a , b , c >. -> ( A. q e. s -. q U p <-> A. q e. s -. q U <. a , b , c >. ) )
204 203 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 )
205 81 200 204 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 )
206 74 205 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 )
207 53 206 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 )
208 36 207 rexlimddv 
 |-  ( ( ph /\ ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) ) -> E. p e. s A. q e. s -. q U p )
209 208 ex 
 |-  ( ph -> ( ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) -> E. p e. s A. q e. s -. q U p ) )
210 209 alrimiv 
 |-  ( ph -> A. s ( ( s C_ ( ( A X. B ) X. C ) /\ s =/= (/) ) -> E. p e. s A. q e. s -. q U p ) )
211 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 ) )
212 210 211 sylibr 
 |-  ( ph -> U Fr ( ( A X. B ) X. C ) )