Metamath Proof Explorer

Theorem ixpiunwdom

Description: Describe an onto function from the indexed cartesian product to the indexed union. Together with ixpssmapg this shows that U_ x e. A B and X_ x e. A B have closely linked cardinalities. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Assertion ixpiunwdom 
|- ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> U_ x e. A B ~<_* ( X_ x e. A B X. A ) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  f e. _V
2 1 elixp 
 |-  ( f e. X_ x e. A B <-> ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
3 2 simprbi 
 |-  ( f e. X_ x e. A B -> A. x e. A ( f ` x ) e. B )
4 ssiun2 
 |-  ( x e. A -> B C_ U_ x e. A B )
5 4 sseld 
 |-  ( x e. A -> ( ( f ` x ) e. B -> ( f ` x ) e. U_ x e. A B ) )
6 5 ralimia 
 |-  ( A. x e. A ( f ` x ) e. B -> A. x e. A ( f ` x ) e. U_ x e. A B )
7 3 6 syl 
 |-  ( f e. X_ x e. A B -> A. x e. A ( f ` x ) e. U_ x e. A B )
8 nfv 
 |-  F/ y ( f ` x ) e. U_ x e. A B
9 nfiu1 
 |-  F/_ x U_ x e. A B
10 9 nfel2 
 |-  F/ x ( f ` y ) e. U_ x e. A B
11 fveq2 
 |-  ( x = y -> ( f ` x ) = ( f ` y ) )
12 11 eleq1d 
 |-  ( x = y -> ( ( f ` x ) e. U_ x e. A B <-> ( f ` y ) e. U_ x e. A B ) )
13 8 10 12 cbvralw 
 |-  ( A. x e. A ( f ` x ) e. U_ x e. A B <-> A. y e. A ( f ` y ) e. U_ x e. A B )
14 7 13 sylib 
 |-  ( f e. X_ x e. A B -> A. y e. A ( f ` y ) e. U_ x e. A B )
15 14 adantl 
 |-  ( ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) /\ f e. X_ x e. A B ) -> A. y e. A ( f ` y ) e. U_ x e. A B )
16 15 ralrimiva 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> A. f e. X_ x e. A B A. y e. A ( f ` y ) e. U_ x e. A B )
17 eqid 
 |-  ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) = ( f e. X_ x e. A B , y e. A |-> ( f ` y ) )
18 17 fmpo 
 |-  ( A. f e. X_ x e. A B A. y e. A ( f ` y ) e. U_ x e. A B <-> ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) : ( X_ x e. A B X. A ) --> U_ x e. A B )
19 16 18 sylib 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) : ( X_ x e. A B X. A ) --> U_ x e. A B )
20 ixpssmap2g 
 |-  ( U_ x e. A B e. W -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
21 20 3ad2ant2 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
22 ovex 
 |-  ( U_ x e. A B ^m A ) e. _V
23 22 ssex 
 |-  ( X_ x e. A B C_ ( U_ x e. A B ^m A ) -> X_ x e. A B e. _V )
24 21 23 syl 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> X_ x e. A B e. _V )
25 simp1 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> A e. V )
26 24 25 xpexd 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> ( X_ x e. A B X. A ) e. _V )
27 19 26 fexd 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) e. _V )
28 19 ffnd 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) Fn ( X_ x e. A B X. A ) )
29 dffn4 
 |-  ( ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) Fn ( X_ x e. A B X. A ) <-> ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) : ( X_ x e. A B X. A ) -onto-> ran ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) )
30 28 29 sylib 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) : ( X_ x e. A B X. A ) -onto-> ran ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) )
31 n0 
 |-  ( X_ x e. A B =/= (/) <-> E. g g e. X_ x e. A B )
32 eliun 
 |-  ( z e. U_ x e. A B <-> E. x e. A z e. B )
33 nfixp1 
 |-  F/_ x X_ x e. A B
34 33 nfel2 
 |-  F/ x g e. X_ x e. A B
35 nfv 
 |-  F/ x E. y e. A z = ( f ` y )
36 33 35 nfrexw 
 |-  F/ x E. f e. X_ x e. A B E. y e. A z = ( f ` y )
37 simplrr 
 |-  ( ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) /\ k e. A ) -> z e. B )
38 iftrue 
 |-  ( k = x -> if ( k = x , z , ( g ` k ) ) = z )
39 csbeq1a 
 |-  ( x = k -> B = [_ k / x ]_ B )
40 39 equcoms 
 |-  ( k = x -> B = [_ k / x ]_ B )
41 40 eqcomd 
 |-  ( k = x -> [_ k / x ]_ B = B )
42 38 41 eleq12d 
 |-  ( k = x -> ( if ( k = x , z , ( g ` k ) ) e. [_ k / x ]_ B <-> z e. B ) )
43 37 42 syl5ibrcom 
 |-  ( ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) /\ k e. A ) -> ( k = x -> if ( k = x , z , ( g ` k ) ) e. [_ k / x ]_ B ) )
44 vex 
 |-  g e. _V
45 44 elixp 
 |-  ( g e. X_ x e. A B <-> ( g Fn A /\ A. x e. A ( g ` x ) e. B ) )
46 45 simprbi 
 |-  ( g e. X_ x e. A B -> A. x e. A ( g ` x ) e. B )
47 46 adantr 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> A. x e. A ( g ` x ) e. B )
48 nfv 
 |-  F/ k ( g ` x ) e. B
49 nfcsb1v 
 |-  F/_ x [_ k / x ]_ B
50 49 nfel2 
 |-  F/ x ( g ` k ) e. [_ k / x ]_ B
51 fveq2 
 |-  ( x = k -> ( g ` x ) = ( g ` k ) )
52 51 39 eleq12d 
 |-  ( x = k -> ( ( g ` x ) e. B <-> ( g ` k ) e. [_ k / x ]_ B ) )
53 48 50 52 cbvralw 
 |-  ( A. x e. A ( g ` x ) e. B <-> A. k e. A ( g ` k ) e. [_ k / x ]_ B )
54 47 53 sylib 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> A. k e. A ( g ` k ) e. [_ k / x ]_ B )
55 54 r19.21bi 
 |-  ( ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) /\ k e. A ) -> ( g ` k ) e. [_ k / x ]_ B )
56 iffalse 
 |-  ( -. k = x -> if ( k = x , z , ( g ` k ) ) = ( g ` k ) )
57 56 eleq1d 
 |-  ( -. k = x -> ( if ( k = x , z , ( g ` k ) ) e. [_ k / x ]_ B <-> ( g ` k ) e. [_ k / x ]_ B ) )
58 55 57 syl5ibrcom 
 |-  ( ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) /\ k e. A ) -> ( -. k = x -> if ( k = x , z , ( g ` k ) ) e. [_ k / x ]_ B ) )
59 43 58 pm2.61d 
 |-  ( ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) /\ k e. A ) -> if ( k = x , z , ( g ` k ) ) e. [_ k / x ]_ B )
60 59 ralrimiva 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> A. k e. A if ( k = x , z , ( g ` k ) ) e. [_ k / x ]_ B )
61 ixpfn 
 |-  ( g e. X_ x e. A B -> g Fn A )
62 61 adantr 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> g Fn A )
63 62 fndmd 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> dom g = A )
64 44 dmex 
 |-  dom g e. _V
65 63 64 eqeltrrdi 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> A e. _V )
66 mptelixpg 
 |-  ( A e. _V -> ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) e. X_ k e. A [_ k / x ]_ B <-> A. k e. A if ( k = x , z , ( g ` k ) ) e. [_ k / x ]_ B ) )
67 65 66 syl 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) e. X_ k e. A [_ k / x ]_ B <-> A. k e. A if ( k = x , z , ( g ` k ) ) e. [_ k / x ]_ B ) )
68 60 67 mpbird 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) e. X_ k e. A [_ k / x ]_ B )
69 nfcv 
 |-  F/_ k B
70 69 49 39 cbvixp 
 |-  X_ x e. A B = X_ k e. A [_ k / x ]_ B
71 68 70 eleqtrrdi 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) e. X_ x e. A B )
72 simprl 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> x e. A )
73 eqid 
 |-  ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) = ( k e. A |-> if ( k = x , z , ( g ` k ) ) )
74 vex 
 |-  z e. _V
75 38 73 74 fvmpt 
 |-  ( x e. A -> ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` x ) = z )
76 75 ad2antrl 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` x ) = z )
77 76 eqcomd 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> z = ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` x ) )
78 fveq1 
 |-  ( f = ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) -> ( f ` y ) = ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` y ) )
79 78 eqeq2d 
 |-  ( f = ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) -> ( z = ( f ` y ) <-> z = ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` y ) ) )
80 fveq2 
 |-  ( y = x -> ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` y ) = ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` x ) )
81 80 eqeq2d 
 |-  ( y = x -> ( z = ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` y ) <-> z = ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` x ) ) )
82 79 81 rspc2ev 
 |-  ( ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) e. X_ x e. A B /\ x e. A /\ z = ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` x ) ) -> E. f e. X_ x e. A B E. y e. A z = ( f ` y ) )
83 71 72 77 82 syl3anc 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> E. f e. X_ x e. A B E. y e. A z = ( f ` y ) )
84 83 exp32 
 |-  ( g e. X_ x e. A B -> ( x e. A -> ( z e. B -> E. f e. X_ x e. A B E. y e. A z = ( f ` y ) ) ) )
85 34 36 84 rexlimd 
 |-  ( g e. X_ x e. A B -> ( E. x e. A z e. B -> E. f e. X_ x e. A B E. y e. A z = ( f ` y ) ) )
86 32 85 biimtrid 
 |-  ( g e. X_ x e. A B -> ( z e. U_ x e. A B -> E. f e. X_ x e. A B E. y e. A z = ( f ` y ) ) )
87 86 exlimiv 
 |-  ( E. g g e. X_ x e. A B -> ( z e. U_ x e. A B -> E. f e. X_ x e. A B E. y e. A z = ( f ` y ) ) )
88 31 87 sylbi 
 |-  ( X_ x e. A B =/= (/) -> ( z e. U_ x e. A B -> E. f e. X_ x e. A B E. y e. A z = ( f ` y ) ) )
89 88 3ad2ant3 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> ( z e. U_ x e. A B -> E. f e. X_ x e. A B E. y e. A z = ( f ` y ) ) )
90 89 alrimiv 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> A. z ( z e. U_ x e. A B -> E. f e. X_ x e. A B E. y e. A z = ( f ` y ) ) )
91 ssab 
 |-  ( U_ x e. A B C_ { z | E. f e. X_ x e. A B E. y e. A z = ( f ` y ) } <-> A. z ( z e. U_ x e. A B -> E. f e. X_ x e. A B E. y e. A z = ( f ` y ) ) )
92 90 91 sylibr 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> U_ x e. A B C_ { z | E. f e. X_ x e. A B E. y e. A z = ( f ` y ) } )
93 17 rnmpo 
 |-  ran ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) = { z | E. f e. X_ x e. A B E. y e. A z = ( f ` y ) }
94 92 93 sseqtrrdi 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> U_ x e. A B C_ ran ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) )
95 19 frnd 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> ran ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) C_ U_ x e. A B )
96 94 95 eqssd 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> U_ x e. A B = ran ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) )
97 foeq3 
 |-  ( U_ x e. A B = ran ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) -> ( ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) : ( X_ x e. A B X. A ) -onto-> U_ x e. A B <-> ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) : ( X_ x e. A B X. A ) -onto-> ran ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) ) )
98 96 97 syl 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> ( ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) : ( X_ x e. A B X. A ) -onto-> U_ x e. A B <-> ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) : ( X_ x e. A B X. A ) -onto-> ran ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) ) )
99 30 98 mpbird 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) : ( X_ x e. A B X. A ) -onto-> U_ x e. A B )
100 fowdom 
 |-  ( ( ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) e. _V /\ ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) : ( X_ x e. A B X. A ) -onto-> U_ x e. A B ) -> U_ x e. A B ~<_* ( X_ x e. A B X. A ) )
101 27 99 100 syl2anc 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> U_ x e. A B ~<_* ( X_ x e. A B X. A ) )