Metamath Proof Explorer

Theorem iunfo

Description: Existence of an onto function from a disjoint union to a union. (Contributed by Mario Carneiro, 24-Jun-2013) (Revised by Mario Carneiro, 18-Jan-2014)

Ref Expression
Hypothesis iunfo.1 
|- T = U_ x e. A ( { x } X. B )
Assertion iunfo 
|- ( 2nd |` T ) : T -onto-> U_ x e. A B

Proof

Step Hyp Ref Expression
1 iunfo.1 
 |-  T = U_ x e. A ( { x } X. B )
2 fo2nd 
 |-  2nd : _V -onto-> _V
3 fof 
 |-  ( 2nd : _V -onto-> _V -> 2nd : _V --> _V )
4 ffn 
 |-  ( 2nd : _V --> _V -> 2nd Fn _V )
5 2 3 4 mp2b 
 |-  2nd Fn _V
6 ssv 
 |-  T C_ _V
7 fnssres 
 |-  ( ( 2nd Fn _V /\ T C_ _V ) -> ( 2nd |` T ) Fn T )
8 5 6 7 mp2an 
 |-  ( 2nd |` T ) Fn T
9 df-ima 
 |-  ( 2nd " T ) = ran ( 2nd |` T )
10 1 eleq2i 
 |-  ( z e. T <-> z e. U_ x e. A ( { x } X. B ) )
11 eliun 
 |-  ( z e. U_ x e. A ( { x } X. B ) <-> E. x e. A z e. ( { x } X. B ) )
12 10 11 bitri 
 |-  ( z e. T <-> E. x e. A z e. ( { x } X. B ) )
13 xp2nd 
 |-  ( z e. ( { x } X. B ) -> ( 2nd ` z ) e. B )
14 eleq1 
 |-  ( ( 2nd ` z ) = y -> ( ( 2nd ` z ) e. B <-> y e. B ) )
15 13 14 syl5ib 
 |-  ( ( 2nd ` z ) = y -> ( z e. ( { x } X. B ) -> y e. B ) )
16 15 reximdv 
 |-  ( ( 2nd ` z ) = y -> ( E. x e. A z e. ( { x } X. B ) -> E. x e. A y e. B ) )
17 12 16 syl5bi 
 |-  ( ( 2nd ` z ) = y -> ( z e. T -> E. x e. A y e. B ) )
18 17 impcom 
 |-  ( ( z e. T /\ ( 2nd ` z ) = y ) -> E. x e. A y e. B )
19 18 rexlimiva 
 |-  ( E. z e. T ( 2nd ` z ) = y -> E. x e. A y e. B )
20 nfiu1 
 |-  F/_ x U_ x e. A ( { x } X. B )
21 1 20 nfcxfr 
 |-  F/_ x T
22 nfv 
 |-  F/ x ( 2nd ` z ) = y
23 21 22 nfrex 
 |-  F/ x E. z e. T ( 2nd ` z ) = y
24 ssiun2 
 |-  ( x e. A -> ( { x } X. B ) C_ U_ x e. A ( { x } X. B ) )
25 24 adantr 
 |-  ( ( x e. A /\ y e. B ) -> ( { x } X. B ) C_ U_ x e. A ( { x } X. B ) )
26 simpr 
 |-  ( ( x e. A /\ y e. B ) -> y e. B )
27 vsnid 
 |-  x e. { x }
28 opelxp 
 |-  ( <. x , y >. e. ( { x } X. B ) <-> ( x e. { x } /\ y e. B ) )
29 27 28 mpbiran 
 |-  ( <. x , y >. e. ( { x } X. B ) <-> y e. B )
30 26 29 sylibr 
 |-  ( ( x e. A /\ y e. B ) -> <. x , y >. e. ( { x } X. B ) )
31 25 30 sseldd 
 |-  ( ( x e. A /\ y e. B ) -> <. x , y >. e. U_ x e. A ( { x } X. B ) )
32 31 1 eleqtrrdi 
 |-  ( ( x e. A /\ y e. B ) -> <. x , y >. e. T )
33 vex 
 |-  x e. _V
34 vex 
 |-  y e. _V
35 33 34 op2nd 
 |-  ( 2nd ` <. x , y >. ) = y
36 fveqeq2 
 |-  ( z = <. x , y >. -> ( ( 2nd ` z ) = y <-> ( 2nd ` <. x , y >. ) = y ) )
37 36 rspcev 
 |-  ( ( <. x , y >. e. T /\ ( 2nd ` <. x , y >. ) = y ) -> E. z e. T ( 2nd ` z ) = y )
38 32 35 37 sylancl 
 |-  ( ( x e. A /\ y e. B ) -> E. z e. T ( 2nd ` z ) = y )
39 38 ex 
 |-  ( x e. A -> ( y e. B -> E. z e. T ( 2nd ` z ) = y ) )
40 23 39 rexlimi 
 |-  ( E. x e. A y e. B -> E. z e. T ( 2nd ` z ) = y )
41 19 40 impbii 
 |-  ( E. z e. T ( 2nd ` z ) = y <-> E. x e. A y e. B )
42 fvelimab 
 |-  ( ( 2nd Fn _V /\ T C_ _V ) -> ( y e. ( 2nd " T ) <-> E. z e. T ( 2nd ` z ) = y ) )
43 5 6 42 mp2an 
 |-  ( y e. ( 2nd " T ) <-> E. z e. T ( 2nd ` z ) = y )
44 eliun 
 |-  ( y e. U_ x e. A B <-> E. x e. A y e. B )
45 41 43 44 3bitr4i 
 |-  ( y e. ( 2nd " T ) <-> y e. U_ x e. A B )
46 45 eqriv 
 |-  ( 2nd " T ) = U_ x e. A B
47 9 46 eqtr3i 
 |-  ran ( 2nd |` T ) = U_ x e. A B
48 df-fo 
 |-  ( ( 2nd |` T ) : T -onto-> U_ x e. A B <-> ( ( 2nd |` T ) Fn T /\ ran ( 2nd |` T ) = U_ x e. A B ) )
49 8 47 48 mpbir2an 
 |-  ( 2nd |` T ) : T -onto-> U_ x e. A B