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 )

Metamath Proof Explorer

Theorem unfilem1

Proof