Metamath Proof Explorer

Theorem unfilem3

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

Ref Expression
Assertion unfilem3 
|- ( ( A e. _om /\ B e. _om ) -> B ~~ ( ( A +o B ) \ A ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( A = if ( A e. _om , A , (/) ) -> ( A +o B ) = ( if ( A e. _om , A , (/) ) +o B ) )
2 id 
 |-  ( A = if ( A e. _om , A , (/) ) -> A = if ( A e. _om , A , (/) ) )
3 1 2 difeq12d 
 |-  ( A = if ( A e. _om , A , (/) ) -> ( ( A +o B ) \ A ) = ( ( if ( A e. _om , A , (/) ) +o B ) \ if ( A e. _om , A , (/) ) ) )
4 3 breq2d 
 |-  ( A = if ( A e. _om , A , (/) ) -> ( B ~~ ( ( A +o B ) \ A ) <-> B ~~ ( ( if ( A e. _om , A , (/) ) +o B ) \ if ( A e. _om , A , (/) ) ) ) )
5 id 
 |-  ( B = if ( B e. _om , B , (/) ) -> B = if ( B e. _om , B , (/) ) )
6 oveq2 
 |-  ( B = if ( B e. _om , B , (/) ) -> ( if ( A e. _om , A , (/) ) +o B ) = ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) )
7 6 difeq1d 
 |-  ( B = if ( B e. _om , B , (/) ) -> ( ( if ( A e. _om , A , (/) ) +o B ) \ if ( A e. _om , A , (/) ) ) = ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) \ if ( A e. _om , A , (/) ) ) )
8 5 7 breq12d 
 |-  ( B = if ( B e. _om , B , (/) ) -> ( B ~~ ( ( if ( A e. _om , A , (/) ) +o B ) \ if ( A e. _om , A , (/) ) ) <-> if ( B e. _om , B , (/) ) ~~ ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) \ if ( A e. _om , A , (/) ) ) ) )
9 peano1 
 |-  (/) e. _om
10 9 elimel 
 |-  if ( B e. _om , B , (/) ) e. _om
11 ovex 
 |-  ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) e. _V
12 11 difexi 
 |-  ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) \ if ( A e. _om , A , (/) ) ) e. _V
13 9 elimel 
 |-  if ( A e. _om , A , (/) ) e. _om
14 eqid 
 |-  ( x e. if ( B e. _om , B , (/) ) |-> ( if ( A e. _om , A , (/) ) +o x ) ) = ( x e. if ( B e. _om , B , (/) ) |-> ( if ( A e. _om , A , (/) ) +o x ) )
15 13 10 14 unfilem2 
 |-  ( x e. if ( B e. _om , B , (/) ) |-> ( if ( A e. _om , A , (/) ) +o x ) ) : if ( B e. _om , B , (/) ) -1-1-onto-> ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) \ if ( A e. _om , A , (/) ) )
16 f1oen2g 
 |-  ( ( if ( B e. _om , B , (/) ) e. _om /\ ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) \ if ( A e. _om , A , (/) ) ) e. _V /\ ( x e. if ( B e. _om , B , (/) ) |-> ( if ( A e. _om , A , (/) ) +o x ) ) : if ( B e. _om , B , (/) ) -1-1-onto-> ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) \ if ( A e. _om , A , (/) ) ) ) -> if ( B e. _om , B , (/) ) ~~ ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) \ if ( A e. _om , A , (/) ) ) )
17 10 12 15 16 mp3an 
 |-  if ( B e. _om , B , (/) ) ~~ ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) \ if ( A e. _om , A , (/) ) )
18 4 8 17 dedth2h 
 |-  ( ( A e. _om /\ B e. _om ) -> B ~~ ( ( A +o B ) \ A ) )