unxpwdom2 - Metamath Proof Explorer

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

Theorem unxpwdom2 8112

Description: Lemma for unxpwdom 8113. (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 7628	. 2
2		bren 7589	. . 3
3		ssdif0 3853	. . . . . 6 $\$
4		dmxpid 5073	. . . . . . . . . . . . . 14
5		f1ofo 5838	. . . . . . . . . . . . . . . . 17
6		forn 5813	. . . . . . . . . . . . . . . . 17
7	5, 6	syl 17	. . . . . . . . . . . . . . . 16
8		vex 3083	. . . . . . . . . . . . . . . . 17
9	8	rnex 6741	. . . . . . . . . . . . . . . 16
10	7, 9	syl6eqelr 2516	. . . . . . . . . . . . . . 15
11		dmexg 6738	. . . . . . . . . . . . . . 15
12	10, 11	syl 17	. . . . . . . . . . . . . 14
13	4, 12	syl5eqelr 2512	. . . . . . . . . . . . 13
14		imassrn 5198	. . . . . . . . . . . . . 14
15		f1stres 6829	. . . . . . . . . . . . . . . 16
16		f1of 5831	. . . . . . . . . . . . . . . 16
17		fco 5756	. . . . . . . . . . . . . . . 16 $/\$
18	15, 16, 17	sylancr 667	. . . . . . . . . . . . . . 15
19		frn 5752	. . . . . . . . . . . . . . 15
20	18, 19	syl 17	. . . . . . . . . . . . . 14
21	14, 20	syl5ss 3475	. . . . . . . . . . . . 13
22	13, 21	ssexd 4571	. . . . . . . . . . . 12
23	22	adantr 466	. . . . . . . . . . 11 $/\$
24		simpr 462	. . . . . . . . . . 11 $/\$
25		ssdomg 7625	. . . . . . . . . . 11
26	23, 24, 25	sylc 62	. . . . . . . . . 10 $/\$
27		domwdom 8098	. . . . . . . . . 10 ^*
28	26, 27	syl 17	. . . . . . . . 9 $/\$ ^*
29		ffun 5748	. . . . . . . . . . . 12
30	18, 29	syl 17	. . . . . . . . . . 11
31		ssun1 3629	. . . . . . . . . . . 12
32		f1odm 5835	. . . . . . . . . . . . 13
33	8	dmex 6740	. . . . . . . . . . . . 13
34	32, 33	syl6eqelr 2516	. . . . . . . . . . . 12
35		ssexg 4570	. . . . . . . . . . . 12 $/\$
36	31, 34, 35	sylancr 667	. . . . . . . . . . 11
37		wdomima2g 8110	. . . . . . . . . . 11 $/\$ $/\$ ^*
38	30, 36, 22, 37	syl3anc 1264	. . . . . . . . . 10 ^*
39	38	adantr 466	. . . . . . . . 9 $/\$ ^*
40		wdomtr 8099	. . . . . . . . 9 ^* $/\$ ^* ^*
41	28, 39, 40	syl2anc 665	. . . . . . . 8 $/\$ ^*
42	41	orcd 393	. . . . . . 7 $/\$ ^* $\/$
43	42	ex 435	. . . . . 6 ^* $\/$
44	3, 43	syl5bir 221	. . . . 5 $\$ ^* $\/$
45		n0 3771	. . . . . 6 $\$ $\$
46		ssun2 3630	. . . . . . . . . . . . 13
47		ssexg 4570	. . . . . . . . . . . . 13 $/\$
48	46, 34, 47	sylancr 667	. . . . . . . . . . . 12
49	48	adantr 466	. . . . . . . . . . 11 $/\$ $\$
50		f1ofn 5832	. . . . . . . . . . . . . . 15
51		elpreima 6017	. . . . . . . . . . . . . . 15 $/\$
52	50, 51	syl 17	. . . . . . . . . . . . . 14 $/\$
53	52	adantr 466	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
54		elun 3606	. . . . . . . . . . . . . . . 16 $\/$
55		df-or 371	. . . . . . . . . . . . . . . 16 $\/$
56	54, 55	bitri 252	. . . . . . . . . . . . . . 15
57		eldifn 3588	. . . . . . . . . . . . . . . . . . 19 $\$
58	57	ad2antlr 731	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$
59	16	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
60		simprr 764	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
61	31, 60	sseldi 3462	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
62		fvco3 5958	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
63	59, 61, 62	syl2anc 665	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
64		eldifi 3587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
65	64	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$
66	65	snssd 4145	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$
67		xpss1 4962	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68	66, 67	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$
69	68	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $/\$
70		simprl 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $/\$
71	69, 70	sseldd 3465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $/\$
72		fvres 5895	. . . . . . . . . . . . . . . . . . . . . . . 24
73	71, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
74		xp1st 6837	. . . . . . . . . . . . . . . . . . . . . . . 24
75	70, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
76	73, 75	eqeltrd 2507	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
77		elsni 4023	. . . . . . . . . . . . . . . . . . . . . 22
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
79	63, 78	eqtrd 2463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $/\$
80		ffn 5746	. . . . . . . . . . . . . . . . . . . . . . 23
81	18, 80	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
82	81	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
83	31	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
84		fnfvima 6158	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
85	82, 83, 60, 84	syl3anc 1264	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $/\$
86	79, 85	eqeltrrd 2508	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $/\$
87	86	expr 618	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$
88	58, 87	mtod 180	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$
89	88	ex 435	. . . . . . . . . . . . . . . 16 $/\$ $\$
90	89	imim1d 78	. . . . . . . . . . . . . . 15 $/\$ $\$
91	56, 90	syl5bi 220	. . . . . . . . . . . . . 14 $/\$ $\$
92	91	impd 432	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
93	53, 92	sylbid 218	. . . . . . . . . . . 12 $/\$ $\$
94	93	ssrdv 3470	. . . . . . . . . . 11 $/\$ $\$
95		ssdomg 7625	. . . . . . . . . . 11
96	49, 94, 95	sylc 62	. . . . . . . . . 10 $/\$ $\$
97		f1ocnv 5843	. . . . . . . . . . . . . . 15
98		f1of1 5830	. . . . . . . . . . . . . . 15
99	97, 98	syl 17	. . . . . . . . . . . . . 14
100	99	adantr 466	. . . . . . . . . . . . 13 $/\$ $\$
101	34	adantr 466	. . . . . . . . . . . . 13 $/\$ $\$
102		snex 4662	. . . . . . . . . . . . . 14
103	13	adantr 466	. . . . . . . . . . . . . 14 $/\$ $\$
104		xpexg 6607	. . . . . . . . . . . . . 14 $/\$
105	102, 103, 104	sylancr 667	. . . . . . . . . . . . 13 $/\$ $\$
106		f1imaen2g 7640	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
107	100, 101, 68, 105, 106	syl22anc 1265	. . . . . . . . . . . 12 $/\$ $\$
108		vex 3083	. . . . . . . . . . . . 13
109		xpsnen2g 7674	. . . . . . . . . . . . 13 $/\$
110	108, 103, 109	sylancr 667	. . . . . . . . . . . 12 $/\$ $\$
111		entr 7631	. . . . . . . . . . . 12 $/\$
112	107, 110, 111	syl2anc 665	. . . . . . . . . . 11 $/\$ $\$
113		domen1 7723	. . . . . . . . . . 11
114	112, 113	syl 17	. . . . . . . . . 10 $/\$ $\$
115	96, 114	mpbid 213	. . . . . . . . 9 $/\$ $\$
116	115	olcd 394	. . . . . . . 8 $/\$ $\$ ^* $\/$
117	116	ex 435	. . . . . . 7 $\$ ^* $\/$
118	117	exlimdv 1772	. . . . . 6 $\$ ^* $\/$
119	45, 118	syl5bi 220	. . . . 5 $\$ ^* $\/$
120	44, 119	pm2.61dne 2737	. . . 4 ^* $\/$
121	120	exlimiv 1770	. . 3 ^* $\/$
122	2, 121	sylbi 198	. 2 ^* $\/$
123	1, 122	syl 17	1 ^* $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370

wceq 1437

wex 1657

wcel 1872

wne 2614

cvv 3080 $\$ cdif 3433

cun 3434

wss 3436

c0 3761

csn 3998 class class class wbr 4423

cxp 4851

ccnv 4852

cdm 4853

crn 4854

cres 4855

cima 4856

ccom 4857

wfun 5595

wfn 5596

wf 5597

wf1 5598

wfo 5599

wf1o 5600

cfv 5601

c1st 6805

cen 7577

cdom 7578

^* cwdom 8081

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6597

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-ral 2776 df-rex 2777 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-op 4005 df-uni 4220 df-int 4256 df-iun 4301 df-br 4424 df-opab 4483 df-mpt 4484 df-id 4768 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-1st 6807 df-2nd 6808 df-er 7374 df-en 7581 df-dom 7582 df-sdom 7583 df-wdom 8083

This theorem is referenced by: unxpwdom 8113 ttac 35861

W3C validator