This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 elun 
 |-  ( x e. ( a u. b ) <-> ( x e. a \/ x e. b ) )
24 23 bilani 
 |-  ( ( ( ( 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 ) )
25 24 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 )
26 22 25 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 ) )
27 18 26 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 ) )
28 2 27 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 ) )
29 28 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 ) )
30 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 >. ) )
31 30 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 >. ) )
32 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 ) >. )
33 32 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 ) >. )
34 31 33 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 ) >. )
35 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 >. ) )
36 35 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 >. ) )
37 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 ) >. )
38 37 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 ) >. )
39 36 38 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 ) >. )
40 34 39 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 ) >. ) )
41 vex 
 |-  z e. _V
42 vex 
 |-  t e. _V
43 vex 
 |-  s e. _V
44 42 43 ifex 
 |-  if ( z = m , t , s ) e. _V
45 41 44 opth1 
 |-  ( <. z , if ( z = m , t , s ) >. = <. w , if ( w = m , t , s ) >. -> z = w )
46 40 45 biimtrdi 
 |-  ( ( ( ( -. 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 ) )
47 simprr 
 |-  ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) -> w e. ( a u. b ) )
48 simpll 
 |-  ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) -> -. m = n )
49 simplr 
 |-  ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) -> -. s = t )
50 1 2 47 48 49 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 ) )
51 50 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 ) )
52 eqcom 
 |-  ( ( F ` z ) = ( F ` w ) <-> ( F ` w ) = ( F ` z ) )
53 simprl 
 |-  ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) -> z e. ( a u. b ) )
54 1 2 53 48 49 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 ) )
55 54 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 ) )
56 55 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 ) )
57 52 56 biimtrid 
 |-  ( ( ( ( -. 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 ) )
58 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 >. )
59 58 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 >. )
60 31 59 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 >. )
61 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 >. )
62 61 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 >. )
63 36 62 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 >. )
64 60 63 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 >. ) )
65 vex 
 |-  n e. _V
66 vex 
 |-  m e. _V
67 65 66 ifex 
 |-  if ( z = t , n , m ) e. _V
68 67 41 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 ) )
69 68 simprbi 
 |-  ( <. if ( z = t , n , m ) , z >. = <. if ( w = t , n , m ) , w >. -> z = w )
70 64 69 biimtrdi 
 |-  ( ( ( ( -. 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 ) )
71 46 51 57 70 4casesdan 
 |-  ( ( ( -. m = n /\ -. s = t ) /\ ( z e. ( a u. b ) /\ w e. ( a u. b ) ) ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) )
72 71 ralrimivva 
 |-  ( ( -. m = n /\ -. s = t ) -> A. z e. ( a u. b ) A. w e. ( a u. b ) ( ( F ` z ) = ( F ` w ) -> z = w ) )
73 72 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 ) )
74 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 ) ) )
75 29 73 74 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 ) )
76 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 ) )
77 11 12 75 76 mp3an12i 
 |-  ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) /\ ( -. m = n /\ -. s = t ) ) -> ( a u. b ) ~<_ ( a X. b ) )
78 77 3expia 
 |-  ( ( ( m e. a /\ s e. b ) /\ ( n e. a /\ t e. b ) ) -> ( ( -. m = n /\ -. s = t ) -> ( a u. b ) ~<_ ( a X. b ) ) )
79 78 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 ) ) )
80 8 79 biimtrrid 
 |-  ( ( m e. a /\ s e. b ) -> ( ( E. n e. a -. m = n /\ E. t e. b -. s = t ) -> ( a u. b ) ~<_ ( a X. b ) ) )
81 80 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 ) )
82 7 81 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 ) )
83 4 6 82 syl2anb 
 |-  ( ( 1o ~< a /\ 1o ~< b ) -> ( a u. b ) ~<_ ( a X. b ) )