unfilem3 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem unfilem3 4696

Description: Lemma for proving that the union of two finite sets is finite.

**Assertion**
Ref	Expression
unfilem3	$/\$

**Proof of Theorem unfilem3**
Step	Hyp	Ref	Expression
1		f1oeq1 3792	. . . 4 $/\$ $/\$
2	1	cla4egv 1909	. . 3 $/\$ $/\$
3		opreq1 4026	. . . . . . . . . . 11
4	3	eqeq2d 1529	. . . . . . . . . 10
5	4	anbi2d 619	. . . . . . . . 9 $/\$ $/\$
6	5	opabbidv 2744	. . . . . . . 8 $/\$ $/\$
7		f1oeq1 3792	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
8	6, 7	syl 10	. . . . . . 7 $/\$ $/\$
9		opreq1 4026	. . . . . . . . . 10
10	9	difeq1d 2210	. . . . . . . . 9
11		difeq2 2206	. . . . . . . . 9
12	10, 11	eqtrd 1550	. . . . . . . 8
13		f1oeq3 3794	. . . . . . . 8 $/\$ $/\$
14	12, 13	syl 10	. . . . . . 7 $/\$ $/\$
15	8, 14	bitrd 531	. . . . . 6 $/\$ $/\$
16		eleq2 1578	. . . . . . . . . 10
17	16	anbi1d 620	. . . . . . . . 9 $/\$ $/\$
18	17	opabbidv 2744	. . . . . . . 8 $/\$ $/\$
19		f1oeq1 3792	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
20	18, 19	syl 10	. . . . . . 7 $/\$ $/\$
21		f1oeq2 3793	. . . . . . 7 $/\$ $/\$
22		opreq2 4027	. . . . . . . . 9
23	22	difeq1d 2210	. . . . . . . 8
24		f1oeq3 3794	. . . . . . . 8 $/\$ $/\$
25	23, 24	syl 10	. . . . . . 7 $/\$ $/\$
26	20, 21, 25	3bitrd 547	. . . . . 6 $/\$ $/\$
27		peano1 3237	. . . . . . . 8
28	27	elimel 2451	. . . . . . 7
29	27	elimel 2451	. . . . . . 7
30		eqid 1518	. . . . . . 7 $/\$ $/\$
31	28, 29, 30	unfilem2 4695	. . . . . 6 $/\$
32	15, 26, 31	dedth2h 2441	. . . . 5 $/\$ $/\$
33		f1ofn 3798	. . . . 5 $/\$ $/\$
34	32, 33	syl 10	. . . 4 $/\$ $/\$
35		fnex 3713	. . . 4 $/\$ $/\$ $/\$
36	34, 35	sylancom 478	. . 3 $/\$ $/\$
37	2, 36, 32	sylc 68	. 2 $/\$
38		oprex 4041	. . . 4
39		difexg 2796	. . . 4
40	38, 39	ax-mp 7	. . 3
41	40	bren 4518	. 2
42	37, 41	sylibr 198	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 3

wb 144 $/\$ wa 221

wceq 992

wcel 994

wex 1016

cvv 1857

cdif 2096

c0 2332

cif 2415 class class class wbr 2692

copab 2740

com 3218

wfn 3258

wf1o 3262 (class class class)co 4021

coa 4266

cen 4505

This theorem is referenced by: unfi 4697

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 998 ax-gen 999 ax-8 1000 ax-9 1001 ax-10 1002 ax-11 1003 ax-12 1004 ax-13 1005 ax-14 1006 ax-17 1007 ax-4 1009 ax-5o 1011 ax-6o 1014 ax-9o 1159 ax-10o 1177 ax-16 1247 ax-11o 1255 ax-ext 1500 ax-rep 2767 ax-sep 2777 ax-nul 2784 ax-pow 2818 ax-pr 2855 ax-un 3089

This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 782 df-3an 783 df-ex 1017 df-sb 1209 df-eu 1421 df-mo 1422 df-clab 1506 df-cleq 1511 df-clel 1514 df-ne 1630 df-ral 1695 df-rex 1696 df-reu 1697 df-rab 1698 df-v 1858 df-sbc 1987 df-csb 2052 df-dif 2101 df-un 2102 df-in 2103 df-ss 2105 df-nul 2333 df-if 2416 df-pw 2459 df-sn 2470 df-pr 2471 df-tp 2473 df-op 2474 df-uni 2570 df-int 2601 df-iun 2635 df-br 2693 df-opab 2741 df-tr 2755 df-eprel 2910 df-id 2913 df-po 2918 df-so 2929 df-fr 2947 df-we 2962 df-ord 2978 df-on 2979 df-lim 2980 df-suc 2981 df-om 3219 df-xp 3265 df-rel 3266 df-cnv 3267 df-co 3268 df-dm 3269 df-rn 3270 df-res 3271 df-ima 3272 df-fun 3273 df-fn 3274 df-f 3275 df-f1 3276 df-fo 3277 df-f1o 3278 df-fv 3279 df-opr 4023 df-oprab 4024 df-rdg 4233 df-oadd 4271 df-en 4509