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 ) )