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 )