Metamath Proof Explorer

Theorem unxpdomlem3

Description: Lemma for unxpdom . (Contributed by Mario Carneiro, 13-Jan-2013) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Hypotheses unxpdomlem1.1 
|- F = ( x e. ( a u. b ) |-> G )
unxpdomlem1.2 
|- G = if ( x e. a , <. x , if ( x = m , t , s ) >. , <. if ( x = t , n , m ) , x >. )
Assertion unxpdomlem3 
|- ( ( 1o ~< a /\ 1o ~< b ) -> ( a u. b ) ~<_ ( a X. b ) )

Proof

Step Hyp Ref Expression
1 unxpdomlem1.1 
 |-  F = ( x e. ( a u. b ) |-> G )
2 unxpdomlem1.2 
 |-  G = if ( x e. a , <. x , if ( x = m , t , s ) >. , <. if ( x = t , n , m ) , x >. )
3 1sdom 
 |-  ( a e. _V -> ( 1o ~< a <-> E. m e. a E. n e. a -. m = n ) )
4 3 elv 
 |-  ( 1o ~< a <-> E. m e. a E. n e. a -. m = n )
5 1sdom 
 |-  ( b e. _V -> ( 1o ~< b <-> E. s e. b E. t e. b -. s = t ) )
6 5 elv 
 |-  ( 1o ~< b <-> E. s e. b E. t e. b -. s = t )
7 reeanv 
 |-  ( E. m e. a E. s e. b ( E. n e. a -. m = n /\ E. t e. b -. s = t ) <-> ( E. m e. a E. n e. a -. m = n /\ E. s e. b E. t e. b -. s = t ) )
8 reeanv 
 |-  ( E. n e. a E. t e. b ( -. m = n /\ -. s = t ) <-> ( E. n e. a -. m = n /\ E. t e. b -. s = t ) )
9 vex 
 |-  a e. _V
10 vex 
 |-  b e. _V
11 9 10 unex 
 |-  ( a u. b ) e. _V
12 9 10 xpex 
 |-  ( a X. b ) e. _V
13 simpr 
 |-  ( ( ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) /\ x e. ( a u. b ) ) /\ x e. a ) -> x e. a )
14 simp2r 
 |-  ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) -> t e. b )
15 simp1r 
 |-  ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) -> s e. b )
16 14 15 ifcld 
 |-  ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) -> if ( x = m , t , s ) e. b )
17 16 ad2antrr 
 |-  ( ( ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) /\ x e. ( a u. b ) ) /\ x e. a ) -> if ( x = m , t , s ) e. b )
18 13 17 opelxpd 
 |-  ( ( ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) /\ x e. ( a u. b ) ) /\ x e. a ) -> <. x , if ( x = m , t , s ) >. e. ( a X. b ) )
19 simp2l 
 |-  ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) -> n e. a )
20 simp1l 
 |-  ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) -> m e. a )
21 19 20 ifcld 
 |-  ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) -> if ( x = t , n , m ) e. a )
22 21 ad2antrr 
 |-  ( ( ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) /\ x e. ( a u. b ) ) /\ -. x e. a ) -> if ( x = t , n , m ) e. a )
23 simpr 
 |-  ( ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) /\ x e. ( a u. b ) ) -> x e. ( a u. b ) )
24 elun 
 |-  ( x e. ( a u. b ) <-> ( x e. a \/ x e. b ) )
25 23 24 sylib 
 |-  ( ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) /\ x e. ( a u. b ) ) -> ( x e. a \/ x e. b ) )
26 25 orcanai 
 |-  ( ( ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) /\ x e. ( a u. b ) ) /\ -. x e. a ) -> x e. b )
27 22 26 opelxpd 
 |-  ( ( ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) /\ x e. ( a u. b ) ) /\ -. x e. a ) -> <. if ( x = t , n , m ) , x >. e. ( a X. b ) )
28 18 27 ifclda 
 |-  ( ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) /\ x e. ( a u. b ) ) -> if ( x e. a , <. x , if ( x = m , t , s ) >. , <. if ( x = t , n , m ) , x >. ) e. ( a X. b ) )
29 2 28 eqeltrid 
 |-  ( ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) /\ x e. ( a u. b ) ) -> G e. ( a X. b ) )
30 29 1 fmptd 
 |-  ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) -> F : ( a u. b ) --> ( a X. b ) )
31 1 2 unxpdomlem1 
 |-  ( z e. ( a u. b ) -> ( F ` z ) = if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) )
32 31 ad2antrl 
 |-  ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) -> ( F ` z ) = if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) )
33 iftrue 
 |-  ( z e. a -> if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) = <. z , if ( z = m , t , s ) >. )
34 33 adantr 
 |-  ( ( z e. a /\ w e. a ) -> if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) = <. z , if ( z = m , t , s ) >. )
35 32 34 sylan9eq 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( z e. a /\ w e. a ) ) -> ( F ` z ) = <. z , if ( z = m , t , s ) >. )
36 1 2 unxpdomlem1 
 |-  ( w e. ( a u. b ) -> ( F ` w ) = if ( w e. a , <. w , if ( w = m , t , s ) >. , <. if ( w = t , n , m ) , w >. ) )
37 36 ad2antll 
 |-  ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) -> ( F ` w ) = if ( w e. a , <. w , if ( w = m , t , s ) >. , <. if ( w = t , n , m ) , w >. ) )
38 iftrue 
 |-  ( w e. a -> if ( w e. a , <. w , if ( w = m , t , s ) >. , <. if ( w = t , n , m ) , w >. ) = <. w , if ( w = m , t , s ) >. )
39 38 adantl 
 |-  ( ( z e. a /\ w e. a ) -> if ( w e. a , <. w , if ( w = m , t , s ) >. , <. if ( w = t , n , m ) , w >. ) = <. w , if ( w = m , t , s ) >. )
40 37 39 sylan9eq 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( z e. a /\ w e. a ) ) -> ( F ` w ) = <. w , if ( w = m , t , s ) >. )
41 35 40 eqeq12d 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( z e. a /\ w e. a ) ) -> ( ( F ` z ) = ( F ` w ) <-> <. z , if ( z = m , t , s ) >. = <. w , if ( w = m , t , s ) >. ) )
42 vex 
 |-  z e. _V
43 vex 
 |-  t e. _V
44 vex 
 |-  s e. _V
45 43 44 ifex 
 |-  if ( z = m , t , s ) e. _V
46 42 45 opth1 
 |-  ( <. z , if ( z = m , t , s ) >. = <. w , if ( w = m , t , s ) >. -> z = w )
47 41 46 syl6bi 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( z e. a /\ w e. a ) ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) )
48 simprr 
 |-  ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) -> w e. ( a u. b ) )
49 simpll 
 |-  ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) -> -. m = n )
50 simplr 
 |-  ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) -> -. s = t )
51 1 2 48 49 50 unxpdomlem2 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( z e. a /\ -. w e. a ) ) -> -. ( F ` z ) = ( F ` w ) )
52 51 pm2.21d 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( z e. a /\ -. w e. a ) ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) )
53 eqcom 
 |-  ( ( F ` z ) = ( F ` w ) <-> ( F ` w ) = ( F ` z ) )
54 simprl 
 |-  ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) -> z e. ( a u. b ) )
55 1 2 54 49 50 unxpdomlem2 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( w e. a /\ -. z e. a ) ) -> -. ( F ` w ) = ( F ` z ) )
56 55 ancom2s 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( -. z e. a /\ w e. a ) ) -> -. ( F ` w ) = ( F ` z ) )
57 56 pm2.21d 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( -. z e. a /\ w e. a ) ) -> ( ( F ` w ) = ( F ` z ) -> z = w ) )
58 53 57 syl5bi 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( -. z e. a /\ w e. a ) ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) )
59 iffalse 
 |-  ( -. z e. a -> if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) = <. if ( z = t , n , m ) , z >. )
60 59 adantr 
 |-  ( ( -. z e. a /\ -. w e. a ) -> if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) = <. if ( z = t , n , m ) , z >. )
61 32 60 sylan9eq 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( -. z e. a /\ -. w e. a ) ) -> ( F ` z ) = <. if ( z = t , n , m ) , z >. )
62 iffalse 
 |-  ( -. w e. a -> if ( w e. a , <. w , if ( w = m , t , s ) >. , <. if ( w = t , n , m ) , w >. ) = <. if ( w = t , n , m ) , w >. )
63 62 adantl 
 |-  ( ( -. z e. a /\ -. w e. a ) -> if ( w e. a , <. w , if ( w = m , t , s ) >. , <. if ( w = t , n , m ) , w >. ) = <. if ( w = t , n , m ) , w >. )
64 37 63 sylan9eq 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( -. z e. a /\ -. w e. a ) ) -> ( F ` w ) = <. if ( w = t , n , m ) , w >. )
65 61 64 eqeq12d 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( -. z e. a /\ -. w e. a ) ) -> ( ( F ` z ) = ( F ` w ) <-> <. if ( z = t , n , m ) , z >. = <. if ( w = t , n , m ) , w >. ) )
66 vex 
 |-  n e. _V
67 vex 
 |-  m e. _V
68 66 67 ifex 
 |-  if ( z = t , n , m ) e. _V
69 68 42 opth 
 |-  ( <. if ( z = t , n , m ) , z >. = <. if ( w = t , n , m ) , w >. <-> ( if ( z = t , n , m ) = if ( w = t , n , m ) /\ z = w ) )
70 69 simprbi 
 |-  ( <. if ( z = t , n , m ) , z >. = <. if ( w = t , n , m ) , w >. -> z = w )
71 65 70 syl6bi 
 |-  ( ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) /\ ( -. z e. a /\ -. w e. a ) ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) )
72 47 52 58 71 4casesdan 
 |-  ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) )
73 72 ralrimivva 
 |-  ( ( -. m = n /\ -. s = t ) -> A. z e. ( a u. b ) A. w e. ( a u. b ) ( ( F ` z ) = ( F ` w ) -> z = w ) )
74 73 3ad2ant3 
 |-  ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) -> A. z e. ( a u. b ) A. w e. ( a u. b ) ( ( F ` z ) = ( F ` w ) -> z = w ) )
75 dff13 
 |-  ( F : ( a u. b ) -1-1-> ( a X. b ) <-> ( F : ( a u. b ) --> ( a X. b ) /\ A. z e. ( a u. b ) A. w e. ( a u. b ) ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
76 30 74 75 sylanbrc 
 |-  ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) -> F : ( a u. b ) -1-1-> ( a X. b ) )
77 f1dom2g 
 |-  ( ( ( a u. b ) e. _V /\ ( a X. b ) e. _V /\ F : ( a u. b ) -1-1-> ( a X. b ) ) -> ( a u. b ) ~<_ ( a X. b ) )
78 11 12 76 77 mp3an12i 
 |-  ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) -> ( a u. b ) ~<_ ( a X. b ) )
79 78 3expia 
 |-  ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) ) -> ( ( -. m = n /\ -. s = t ) -> ( a u. b ) ~<_ ( a X. b ) ) )
80 79 rexlimdvva 
 |-  ( ( m e. a /\ s e. b ) -> ( E. n e. a E. t e. b ( -. m = n /\ -. s = t ) -> ( a u. b ) ~<_ ( a X. b ) ) )
81 8 80 syl5bir 
 |-  ( ( m e. a /\ s e. b ) -> ( ( E. n e. a -. m = n /\ E. t e. b -. s = t ) -> ( a u. b ) ~<_ ( a X. b ) ) )
82 81 rexlimivv 
 |-  ( E. m e. a E. s e. b ( E. n e. a -. m = n /\ E. t e. b -. s = t ) -> ( a u. b ) ~<_ ( a X. b ) )
83 7 82 sylbir 
 |-  ( ( E. m e. a E. n e. a -. m = n /\ E. s e. b E. t e. b -. s = t ) -> ( a u. b ) ~<_ ( a X. b ) )
84 4 6 83 syl2anb 
 |-  ( ( 1o ~< a /\ 1o ~< b ) -> ( a u. b ) ~<_ ( a X. b ) )