Metamath Proof Explorer

Theorem unfilem2

Description: Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 10-Nov-2002) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses unfilem1.1 
|- A e. _om
unfilem1.2 
|- B e. _om
unfilem1.3 
|- F = ( x e. B |-> ( A +o x ) )
Assertion unfilem2 
|- F : B -1-1-onto-> ( ( A +o B ) \ A )

Proof

Step Hyp Ref Expression
1 unfilem1.1 
 |-  A e. _om
2 unfilem1.2 
 |-  B e. _om
3 unfilem1.3 
 |-  F = ( x e. B |-> ( A +o x ) )
4 ovex 
 |-  ( A +o x ) e. _V
5 4 3 fnmpti 
 |-  F Fn B
6 1 2 3 unfilem1 
 |-  ran F = ( ( A +o B ) \ A )
7 df-fo 
 |-  ( F : B -onto-> ( ( A +o B ) \ A ) <-> ( F Fn B /\ ran F = ( ( A +o B ) \ A ) ) )
8 5 6 7 mpbir2an 
 |-  F : B -onto-> ( ( A +o B ) \ A )
9 fof 
 |-  ( F : B -onto-> ( ( A +o B ) \ A ) -> F : B --> ( ( A +o B ) \ A ) )
10 8 9 ax-mp 
 |-  F : B --> ( ( A +o B ) \ A )
11 oveq2 
 |-  ( x = z -> ( A +o x ) = ( A +o z ) )
12 ovex 
 |-  ( A +o z ) e. _V
13 11 3 12 fvmpt 
 |-  ( z e. B -> ( F ` z ) = ( A +o z ) )
14 oveq2 
 |-  ( x = w -> ( A +o x ) = ( A +o w ) )
15 ovex 
 |-  ( A +o w ) e. _V
16 14 3 15 fvmpt 
 |-  ( w e. B -> ( F ` w ) = ( A +o w ) )
17 13 16 eqeqan12d 
 |-  ( ( z e. B /\ w e. B ) -> ( ( F ` z ) = ( F ` w ) <-> ( A +o z ) = ( A +o w ) ) )
18 elnn 
 |-  ( ( z e. B /\ B e. _om ) -> z e. _om )
19 2 18 mpan2 
 |-  ( z e. B -> z e. _om )
20 elnn 
 |-  ( ( w e. B /\ B e. _om ) -> w e. _om )
21 2 20 mpan2 
 |-  ( w e. B -> w e. _om )
22 nnacan 
 |-  ( ( A e. _om /\ z e. _om /\ w e. _om ) -> ( ( A +o z ) = ( A +o w ) <-> z = w ) )
23 1 19 21 22 mp3an3an 
 |-  ( ( z e. B /\ w e. B ) -> ( ( A +o z ) = ( A +o w ) <-> z = w ) )
24 17 23 bitrd 
 |-  ( ( z e. B /\ w e. B ) -> ( ( F ` z ) = ( F ` w ) <-> z = w ) )
25 24 biimpd 
 |-  ( ( z e. B /\ w e. B ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) )
26 25 rgen2 
 |-  A. z e. B A. w e. B ( ( F ` z ) = ( F ` w ) -> z = w )
27 dff13 
 |-  ( F : B -1-1-> ( ( A +o B ) \ A ) <-> ( F : B --> ( ( A +o B ) \ A ) /\ A. z e. B A. w e. B ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
28 10 26 27 mpbir2an 
 |-  F : B -1-1-> ( ( A +o B ) \ A )
29 df-f1o 
 |-  ( F : B -1-1-onto-> ( ( A +o B ) \ A ) <-> ( F : B -1-1-> ( ( A +o B ) \ A ) /\ F : B -onto-> ( ( A +o B ) \ A ) ) )
30 28 8 29 mpbir2an 
 |-  F : B -1-1-onto-> ( ( A +o B ) \ A )