Metamath Proof Explorer


Theorem unfilem1

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 unfilem1
|- ran F = ( ( 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 elnn
 |-  ( ( x e. B /\ B e. _om ) -> x e. _om )
5 2 4 mpan2
 |-  ( x e. B -> x e. _om )
6 nnaord
 |-  ( ( x e. _om /\ B e. _om /\ A e. _om ) -> ( x e. B <-> ( A +o x ) e. ( A +o B ) ) )
7 2 1 6 mp3an23
 |-  ( x e. _om -> ( x e. B <-> ( A +o x ) e. ( A +o B ) ) )
8 5 7 syl
 |-  ( x e. B -> ( x e. B <-> ( A +o x ) e. ( A +o B ) ) )
9 8 ibi
 |-  ( x e. B -> ( A +o x ) e. ( A +o B ) )
10 nnaword1
 |-  ( ( A e. _om /\ x e. _om ) -> A C_ ( A +o x ) )
11 nnord
 |-  ( A e. _om -> Ord A )
12 nnacl
 |-  ( ( A e. _om /\ x e. _om ) -> ( A +o x ) e. _om )
13 nnord
 |-  ( ( A +o x ) e. _om -> Ord ( A +o x ) )
14 12 13 syl
 |-  ( ( A e. _om /\ x e. _om ) -> Ord ( A +o x ) )
15 ordtri1
 |-  ( ( Ord A /\ Ord ( A +o x ) ) -> ( A C_ ( A +o x ) <-> -. ( A +o x ) e. A ) )
16 11 14 15 syl2an2r
 |-  ( ( A e. _om /\ x e. _om ) -> ( A C_ ( A +o x ) <-> -. ( A +o x ) e. A ) )
17 10 16 mpbid
 |-  ( ( A e. _om /\ x e. _om ) -> -. ( A +o x ) e. A )
18 1 5 17 sylancr
 |-  ( x e. B -> -. ( A +o x ) e. A )
19 9 18 jca
 |-  ( x e. B -> ( ( A +o x ) e. ( A +o B ) /\ -. ( A +o x ) e. A ) )
20 eleq1
 |-  ( y = ( A +o x ) -> ( y e. ( A +o B ) <-> ( A +o x ) e. ( A +o B ) ) )
21 eleq1
 |-  ( y = ( A +o x ) -> ( y e. A <-> ( A +o x ) e. A ) )
22 21 notbid
 |-  ( y = ( A +o x ) -> ( -. y e. A <-> -. ( A +o x ) e. A ) )
23 20 22 anbi12d
 |-  ( y = ( A +o x ) -> ( ( y e. ( A +o B ) /\ -. y e. A ) <-> ( ( A +o x ) e. ( A +o B ) /\ -. ( A +o x ) e. A ) ) )
24 23 biimparc
 |-  ( ( ( ( A +o x ) e. ( A +o B ) /\ -. ( A +o x ) e. A ) /\ y = ( A +o x ) ) -> ( y e. ( A +o B ) /\ -. y e. A ) )
25 19 24 sylan
 |-  ( ( x e. B /\ y = ( A +o x ) ) -> ( y e. ( A +o B ) /\ -. y e. A ) )
26 25 rexlimiva
 |-  ( E. x e. B y = ( A +o x ) -> ( y e. ( A +o B ) /\ -. y e. A ) )
27 1 2 nnacli
 |-  ( A +o B ) e. _om
28 elnn
 |-  ( ( y e. ( A +o B ) /\ ( A +o B ) e. _om ) -> y e. _om )
29 27 28 mpan2
 |-  ( y e. ( A +o B ) -> y e. _om )
30 nnord
 |-  ( y e. _om -> Ord y )
31 ordtri1
 |-  ( ( Ord A /\ Ord y ) -> ( A C_ y <-> -. y e. A ) )
32 11 30 31 syl2an
 |-  ( ( A e. _om /\ y e. _om ) -> ( A C_ y <-> -. y e. A ) )
33 nnawordex
 |-  ( ( A e. _om /\ y e. _om ) -> ( A C_ y <-> E. x e. _om ( A +o x ) = y ) )
34 32 33 bitr3d
 |-  ( ( A e. _om /\ y e. _om ) -> ( -. y e. A <-> E. x e. _om ( A +o x ) = y ) )
35 1 29 34 sylancr
 |-  ( y e. ( A +o B ) -> ( -. y e. A <-> E. x e. _om ( A +o x ) = y ) )
36 eleq1
 |-  ( ( A +o x ) = y -> ( ( A +o x ) e. ( A +o B ) <-> y e. ( A +o B ) ) )
37 7 36 sylan9bb
 |-  ( ( x e. _om /\ ( A +o x ) = y ) -> ( x e. B <-> y e. ( A +o B ) ) )
38 37 biimprcd
 |-  ( y e. ( A +o B ) -> ( ( x e. _om /\ ( A +o x ) = y ) -> x e. B ) )
39 eqcom
 |-  ( ( A +o x ) = y <-> y = ( A +o x ) )
40 39 biimpi
 |-  ( ( A +o x ) = y -> y = ( A +o x ) )
41 40 adantl
 |-  ( ( x e. _om /\ ( A +o x ) = y ) -> y = ( A +o x ) )
42 38 41 jca2
 |-  ( y e. ( A +o B ) -> ( ( x e. _om /\ ( A +o x ) = y ) -> ( x e. B /\ y = ( A +o x ) ) ) )
43 42 reximdv2
 |-  ( y e. ( A +o B ) -> ( E. x e. _om ( A +o x ) = y -> E. x e. B y = ( A +o x ) ) )
44 35 43 sylbid
 |-  ( y e. ( A +o B ) -> ( -. y e. A -> E. x e. B y = ( A +o x ) ) )
45 44 imp
 |-  ( ( y e. ( A +o B ) /\ -. y e. A ) -> E. x e. B y = ( A +o x ) )
46 26 45 impbii
 |-  ( E. x e. B y = ( A +o x ) <-> ( y e. ( A +o B ) /\ -. y e. A ) )
47 ovex
 |-  ( A +o x ) e. _V
48 3 47 elrnmpti
 |-  ( y e. ran F <-> E. x e. B y = ( A +o x ) )
49 eldif
 |-  ( y e. ( ( A +o B ) \ A ) <-> ( y e. ( A +o B ) /\ -. y e. A ) )
50 46 48 49 3bitr4i
 |-  ( y e. ran F <-> y e. ( ( A +o B ) \ A ) )
51 50 eqriv
 |-  ran F = ( ( A +o B ) \ A )