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 simp2 
 |-  ( ( A e. V /\ U_ x e. A B e. W /\ X_ x e. A B =/= (/) ) -> U_ x e. A B e. W )
28 fex2 
 |-  ( ( ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) : ( X_ x e. A B X. A ) --> U_ x e. A B /\ ( X_ x e. A B X. A ) e. _V /\ U_ x e. A B e. W ) -> ( f e. X_ x e. A B , y e. A |-> ( f ` y ) ) e. _V )
29 19 26 27 28 syl3anc 
 |-  ( ( 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 )
30 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 ) )
31 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 ) ) )
32 30 31 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 ) ) )
33 n0 
 |-  ( X_ x e. A B =/= (/) <-> E. g g e. X_ x e. A B )
34 eliun 
 |-  ( z e. U_ x e. A B <-> E. x e. A z e. B )
35 nfixp1 
 |-  F/_ x X_ x e. A B
36 35 nfel2 
 |-  F/ x g e. X_ x e. A B
37 nfv 
 |-  F/ x E. y e. A z = ( f ` y )
38 35 37 nfrex 
 |-  F/ x E. f e. X_ x e. A B E. y e. A z = ( f ` y )
39 simplrr 
 |-  ( ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) /\ k e. A ) -> z e. B )
40 iftrue 
 |-  ( k = x -> if ( k = x , z , ( g ` k ) ) = z )
41 csbeq1a 
 |-  ( x = k -> B = [_ k / x ]_ B )
42 41 equcoms 
 |-  ( k = x -> B = [_ k / x ]_ B )
43 42 eqcomd 
 |-  ( k = x -> [_ k / x ]_ B = B )
44 40 43 eleq12d 
 |-  ( k = x -> ( if ( k = x , z , ( g ` k ) ) e. [_ k / x ]_ B <-> z e. B ) )
45 39 44 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 ) )
46 vex 
 |-  g e. _V
47 46 elixp 
 |-  ( g e. X_ x e. A B <-> ( g Fn A /\ A. x e. A ( g ` x ) e. B ) )
48 47 simprbi 
 |-  ( g e. X_ x e. A B -> A. x e. A ( g ` x ) e. B )
49 48 adantr 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> A. x e. A ( g ` x ) e. B )
50 nfv 
 |-  F/ k ( g ` x ) e. B
51 nfcsb1v 
 |-  F/_ x [_ k / x ]_ B
52 51 nfel2 
 |-  F/ x ( g ` k ) e. [_ k / x ]_ B
53 fveq2 
 |-  ( x = k -> ( g ` x ) = ( g ` k ) )
54 53 41 eleq12d 
 |-  ( x = k -> ( ( g ` x ) e. B <-> ( g ` k ) e. [_ k / x ]_ B ) )
55 50 52 54 cbvralw 
 |-  ( A. x e. A ( g ` x ) e. B <-> A. k e. A ( g ` k ) e. [_ k / x ]_ B )
56 49 55 sylib 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> A. k e. A ( g ` k ) e. [_ k / x ]_ B )
57 56 r19.21bi 
 |-  ( ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) /\ k e. A ) -> ( g ` k ) e. [_ k / x ]_ B )
58 iffalse 
 |-  ( -. k = x -> if ( k = x , z , ( g ` k ) ) = ( g ` k ) )
59 58 eleq1d 
 |-  ( -. k = x -> ( if ( k = x , z , ( g ` k ) ) e. [_ k / x ]_ B <-> ( g ` k ) e. [_ k / x ]_ B ) )
60 57 59 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 ) )
61 45 60 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 )
62 61 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 )
63 ixpfn 
 |-  ( g e. X_ x e. A B -> g Fn A )
64 63 adantr 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> g Fn A )
65 64 fndmd 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> dom g = A )
66 46 dmex 
 |-  dom g e. _V
67 65 66 eqeltrrdi 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> A e. _V )
68 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 ) )
69 67 68 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 ) )
70 62 69 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 )
71 nfcv 
 |-  F/_ k B
72 71 51 41 cbvixp 
 |-  X_ x e. A B = X_ k e. A [_ k / x ]_ B
73 70 72 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 )
74 simprl 
 |-  ( ( g e. X_ x e. A B /\ ( x e. A /\ z e. B ) ) -> x e. A )
75 eqid 
 |-  ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) = ( k e. A |-> if ( k = x , z , ( g ` k ) ) )
76 vex 
 |-  z e. _V
77 40 75 76 fvmpt 
 |-  ( x e. A -> ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` x ) = z )
78 77 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 )
79 78 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 ) )
80 fveq1 
 |-  ( f = ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) -> ( f ` y ) = ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` y ) )
81 80 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 ) ) )
82 fveq2 
 |-  ( y = x -> ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` y ) = ( ( k e. A |-> if ( k = x , z , ( g ` k ) ) ) ` x ) )
83 82 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 ) ) )
84 81 83 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 ) )
85 73 74 79 84 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 ) )
86 85 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 ) ) ) )
87 36 38 86 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 ) ) )
88 34 87 syl5bi 
 |-  ( 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 ) ) )
89 88 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 ) ) )
90 33 89 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 ) ) )
91 90 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 ) ) )
92 91 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 ) ) )
93 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 ) ) )
94 92 93 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 ) } )
95 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 ) }
96 94 95 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 ) ) )
97 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 )
98 96 97 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 ) ) )
99 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 ) ) ) )
100 98 99 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 ) ) ) )
101 32 100 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 )
102 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 ) )
103 29 101 102 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 ) )