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