unxpwdom2 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > unxpwdom2		Structured version Unicode version

Theorem unxpwdom2 8032

Description: Lemma for unxpwdom 8033. (Contributed by Mario Carneiro, 15-May-2015.)

**Assertion**
Ref	Expression
unxpwdom2	^* $\/$

Proof of Theorem unxpwdom2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ensym 7583	. 2
2		bren 7544	. . 3
3		ssdif0 3888	. . . . . 6 $\$
4		dmxpid 5232	. . . . . . . . . . . . . 14
5		f1ofo 5829	. . . . . . . . . . . . . . . . 17
6		forn 5804	. . . . . . . . . . . . . . . . 17
7	5, 6	syl 16	. . . . . . . . . . . . . . . 16
8		vex 3112	. . . . . . . . . . . . . . . . 17
9	8	rnex 6733	. . . . . . . . . . . . . . . 16
10	7, 9	syl6eqelr 2554	. . . . . . . . . . . . . . 15
11		dmexg 6730	. . . . . . . . . . . . . . 15
12	10, 11	syl 16	. . . . . . . . . . . . . 14
13	4, 12	syl5eqelr 2550	. . . . . . . . . . . . 13
14		imassrn 5358	. . . . . . . . . . . . . 14
15		f1stres 6821	. . . . . . . . . . . . . . . 16
16		f1of 5822	. . . . . . . . . . . . . . . 16
17		fco 5747	. . . . . . . . . . . . . . . 16 $/\$
18	15, 16, 17	sylancr 663	. . . . . . . . . . . . . . 15
19		frn 5743	. . . . . . . . . . . . . . 15
20	18, 19	syl 16	. . . . . . . . . . . . . 14
21	14, 20	syl5ss 3510	. . . . . . . . . . . . 13
22	13, 21	ssexd 4603	. . . . . . . . . . . 12
23	22	adantr 465	. . . . . . . . . . 11 $/\$
24		simpr 461	. . . . . . . . . . 11 $/\$
25		ssdomg 7580	. . . . . . . . . . 11
26	23, 24, 25	sylc 60	. . . . . . . . . 10 $/\$
27		domwdom 8018	. . . . . . . . . 10 ^*
28	26, 27	syl 16	. . . . . . . . 9 $/\$ ^*
29		ffun 5739	. . . . . . . . . . . 12
30	18, 29	syl 16	. . . . . . . . . . 11
31		ssun1 3663	. . . . . . . . . . . 12
32		f1odm 5826	. . . . . . . . . . . . 13
33	8	dmex 6732	. . . . . . . . . . . . 13
34	32, 33	syl6eqelr 2554	. . . . . . . . . . . 12
35		ssexg 4602	. . . . . . . . . . . 12 $/\$
36	31, 34, 35	sylancr 663	. . . . . . . . . . 11
37		wdomima2g 8030	. . . . . . . . . . 11 $/\$ $/\$ ^*
38	30, 36, 22, 37	syl3anc 1228	. . . . . . . . . 10 ^*
39	38	adantr 465	. . . . . . . . 9 $/\$ ^*
40		wdomtr 8019	. . . . . . . . 9 ^* $/\$ ^* ^*
41	28, 39, 40	syl2anc 661	. . . . . . . 8 $/\$ ^*
42	41	orcd 392	. . . . . . 7 $/\$ ^* $\/$
43	42	ex 434	. . . . . 6 ^* $\/$
44	3, 43	syl5bir 218	. . . . 5 $\$ ^* $\/$
45		n0 3803	. . . . . 6 $\$ $\$
46		ssun2 3664	. . . . . . . . . . . . 13
47		ssexg 4602	. . . . . . . . . . . . 13 $/\$
48	46, 34, 47	sylancr 663	. . . . . . . . . . . 12
49	48	adantr 465	. . . . . . . . . . 11 $/\$ $\$
50		f1ofn 5823	. . . . . . . . . . . . . . 15
51		elpreima 6008	. . . . . . . . . . . . . . 15 $/\$
52	50, 51	syl 16	. . . . . . . . . . . . . 14 $/\$
53	52	adantr 465	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
54		elun 3641	. . . . . . . . . . . . . . . 16 $\/$
55		df-or 370	. . . . . . . . . . . . . . . 16 $\/$
56	54, 55	bitri 249	. . . . . . . . . . . . . . 15
57		eldifn 3623	. . . . . . . . . . . . . . . . . . 19 $\$
58	57	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$
59	16	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
60		simprr 757	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
61	31, 60	sseldi 3497	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
62		fvco3 5950	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
63	59, 61, 62	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
64		eldifi 3622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
65	64	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$
66	65	snssd 4177	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$
67		xpss1 5120	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68	66, 67	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$
69	68	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $/\$
70		simprl 756	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $/\$
71	69, 70	sseldd 3500	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $/\$
72		fvres 5886	. . . . . . . . . . . . . . . . . . . . . . . 24
73	71, 72	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
74		xp1st 6829	. . . . . . . . . . . . . . . . . . . . . . . 24
75	70, 74	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
76	73, 75	eqeltrd 2545	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
77		elsni 4057	. . . . . . . . . . . . . . . . . . . . . 22
78	76, 77	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
79	63, 78	eqtrd 2498	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $/\$
80		ffn 5737	. . . . . . . . . . . . . . . . . . . . . . 23
81	18, 80	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
82	81	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
83	31	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
84		fnfvima 6151	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
85	82, 83, 60, 84	syl3anc 1228	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $/\$
86	79, 85	eqeltrrd 2546	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $/\$
87	86	expr 615	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$
88	58, 87	mtod 177	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$
89	88	ex 434	. . . . . . . . . . . . . . . 16 $/\$ $\$
90	89	imim1d 75	. . . . . . . . . . . . . . 15 $/\$ $\$
91	56, 90	syl5bi 217	. . . . . . . . . . . . . 14 $/\$ $\$
92	91	impd 431	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
93	53, 92	sylbid 215	. . . . . . . . . . . 12 $/\$ $\$
94	93	ssrdv 3505	. . . . . . . . . . 11 $/\$ $\$
95		ssdomg 7580	. . . . . . . . . . 11
96	49, 94, 95	sylc 60	. . . . . . . . . 10 $/\$ $\$
97		f1ocnv 5834	. . . . . . . . . . . . . . 15
98		f1of1 5821	. . . . . . . . . . . . . . 15
99	97, 98	syl 16	. . . . . . . . . . . . . 14
100	99	adantr 465	. . . . . . . . . . . . 13 $/\$ $\$
101	34	adantr 465	. . . . . . . . . . . . 13 $/\$ $\$
102		snex 4697	. . . . . . . . . . . . . 14
103	13	adantr 465	. . . . . . . . . . . . . 14 $/\$ $\$
104		xpexg 6601	. . . . . . . . . . . . . 14 $/\$
105	102, 103, 104	sylancr 663	. . . . . . . . . . . . 13 $/\$ $\$
106		f1imaen2g 7595	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
107	100, 101, 68, 105, 106	syl22anc 1229	. . . . . . . . . . . 12 $/\$ $\$
108		vex 3112	. . . . . . . . . . . . 13
109		xpsnen2g 7629	. . . . . . . . . . . . 13 $/\$
110	108, 103, 109	sylancr 663	. . . . . . . . . . . 12 $/\$ $\$
111		entr 7586	. . . . . . . . . . . 12 $/\$
112	107, 110, 111	syl2anc 661	. . . . . . . . . . 11 $/\$ $\$
113		domen1 7678	. . . . . . . . . . 11
114	112, 113	syl 16	. . . . . . . . . 10 $/\$ $\$
115	96, 114	mpbid 210	. . . . . . . . 9 $/\$ $\$
116	115	olcd 393	. . . . . . . 8 $/\$ $\$ ^* $\/$
117	116	ex 434	. . . . . . 7 $\$ ^* $\/$
118	117	exlimdv 1725	. . . . . 6 $\$ ^* $\/$
119	45, 118	syl5bi 217	. . . . 5 $\$ ^* $\/$
120	44, 119	pm2.61dne 2774	. . . 4 ^* $\/$
121	120	exlimiv 1723	. . 3 ^* $\/$
122	2, 121	sylbi 195	. 2 ^* $\/$
123	1, 122	syl 16	1 ^* $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369

wceq 1395

wex 1613

wcel 1819

wne 2652

cvv 3109 $\$ cdif 3468

cun 3469

wss 3471

c0 3793

csn 4032 class class class wbr 4456

cxp 5006

ccnv 5007

cdm 5008

crn 5009

cres 5010

cima 5011

ccom 5012

wfun 5588

wfn 5589

wf 5590

wf1 5591

wfo 5592

wf1o 5593

cfv 5594

c1st 6797

cen 7532

cdom 7533

^* cwdom 8001

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-id 4804 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-1st 6799 df-2nd 6800 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-wdom 8003

This theorem is referenced by: unxpwdom 8033 ttac 31161

W3C validator