unxpwdom2 - Metamath Proof Explorer

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

Theorem unxpwdom2 7803

Description: Lemma for unxpwdom 7804. (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 7358	. 2
2		bren 7319	. . 3
3		ssdif0 3737	. . . . . 6 $\$
4		dmxpid 5059	. . . . . . . . . . . . . 14
5		f1ofo 5648	. . . . . . . . . . . . . . . . 17
6		forn 5623	. . . . . . . . . . . . . . . . 17
7	5, 6	syl 16	. . . . . . . . . . . . . . . 16
8		vex 2975	. . . . . . . . . . . . . . . . 17
9	8	rnex 6512	. . . . . . . . . . . . . . . 16
10	7, 9	syl6eqelr 2532	. . . . . . . . . . . . . . 15
11		dmexg 6509	. . . . . . . . . . . . . . 15
12	10, 11	syl 16	. . . . . . . . . . . . . 14
13	4, 12	syl5eqelr 2528	. . . . . . . . . . . . 13
14		imassrn 5180	. . . . . . . . . . . . . 14
15		f1stres 6598	. . . . . . . . . . . . . . . 16
16		f1of 5641	. . . . . . . . . . . . . . . 16
17		fco 5568	. . . . . . . . . . . . . . . 16 $/\$
18	15, 16, 17	sylancr 663	. . . . . . . . . . . . . . 15
19		frn 5565	. . . . . . . . . . . . . . 15
20	18, 19	syl 16	. . . . . . . . . . . . . 14
21	14, 20	syl5ss 3367	. . . . . . . . . . . . 13
22	13, 21	ssexd 4439	. . . . . . . . . . . 12
23	22	adantr 465	. . . . . . . . . . 11 $/\$
24		simpr 461	. . . . . . . . . . 11 $/\$
25		ssdomg 7355	. . . . . . . . . . 11
26	23, 24, 25	sylc 60	. . . . . . . . . 10 $/\$
27		domwdom 7789	. . . . . . . . . 10 ^*
28	26, 27	syl 16	. . . . . . . . 9 $/\$ ^*
29		ffun 5561	. . . . . . . . . . . 12
30	18, 29	syl 16	. . . . . . . . . . 11
31		ssun1 3519	. . . . . . . . . . . 12
32		f1odm 5645	. . . . . . . . . . . . 13
33	8	dmex 6511	. . . . . . . . . . . . 13
34	32, 33	syl6eqelr 2532	. . . . . . . . . . . 12
35		ssexg 4438	. . . . . . . . . . . 12 $/\$
36	31, 34, 35	sylancr 663	. . . . . . . . . . 11
37		wdomima2g 7801	. . . . . . . . . . 11 $/\$ $/\$ ^*
38	30, 36, 22, 37	syl3anc 1218	. . . . . . . . . 10 ^*
39	38	adantr 465	. . . . . . . . 9 $/\$ ^*
40		wdomtr 7790	. . . . . . . . 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 3646	. . . . . 6 $\$ $\$
46		ssun2 3520	. . . . . . . . . . . . 13
47		ssexg 4438	. . . . . . . . . . . . 13 $/\$
48	46, 34, 47	sylancr 663	. . . . . . . . . . . 12
49	48	adantr 465	. . . . . . . . . . 11 $/\$ $\$
50		f1ofn 5642	. . . . . . . . . . . . . . 15
51		elpreima 5823	. . . . . . . . . . . . . . 15 $/\$
52	50, 51	syl 16	. . . . . . . . . . . . . 14 $/\$
53	52	adantr 465	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
54		elun 3497	. . . . . . . . . . . . . . . 16 $\/$
55		df-or 370	. . . . . . . . . . . . . . . 16 $\/$
56	54, 55	bitri 249	. . . . . . . . . . . . . . 15
57		eldifn 3479	. . . . . . . . . . . . . . . . . . 19 $\$
58	57	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$
59	16	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
60		simprr 756	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
61	31, 60	sseldi 3354	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
62		fvco3 5768	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
63	59, 61, 62	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
64		eldifi 3478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
65	64	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$
66	65	snssd 4018	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$
67		xpss1 4948	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68	66, 67	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$
69	68	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $/\$
70		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $/\$
71	69, 70	sseldd 3357	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $/\$
72		fvres 5704	. . . . . . . . . . . . . . . . . . . . . . . 24
73	71, 72	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
74		xp1st 6606	. . . . . . . . . . . . . . . . . . . . . . . 24
75	70, 74	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
76	73, 75	eqeltrd 2517	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
77		elsni 3902	. . . . . . . . . . . . . . . . . . . . . 22
78	76, 77	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
79	63, 78	eqtrd 2475	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $/\$
80		ffn 5559	. . . . . . . . . . . . . . . . . . . . . . 23
81	18, 80	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
82	81	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
83	31	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
84		fnfvima 5955	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
85	82, 83, 60, 84	syl3anc 1218	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $/\$
86	79, 85	eqeltrrd 2518	. . . . . . . . . . . . . . . . . . 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 3362	. . . . . . . . . . 11 $/\$ $\$
95		ssdomg 7355	. . . . . . . . . . 11
96	49, 94, 95	sylc 60	. . . . . . . . . 10 $/\$ $\$
97		f1ocnv 5653	. . . . . . . . . . . . . . 15
98		f1of1 5640	. . . . . . . . . . . . . . 15
99	97, 98	syl 16	. . . . . . . . . . . . . 14
100	99	adantr 465	. . . . . . . . . . . . 13 $/\$ $\$
101	34	adantr 465	. . . . . . . . . . . . 13 $/\$ $\$
102		snex 4533	. . . . . . . . . . . . . 14
103	13	adantr 465	. . . . . . . . . . . . . 14 $/\$ $\$
104		xpexg 6507	. . . . . . . . . . . . . 14 $/\$
105	102, 103, 104	sylancr 663	. . . . . . . . . . . . 13 $/\$ $\$
106		f1imaen2g 7370	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
107	100, 101, 68, 105, 106	syl22anc 1219	. . . . . . . . . . . 12 $/\$ $\$
108		vex 2975	. . . . . . . . . . . . 13
109		xpsnen2g 7404	. . . . . . . . . . . . 13 $/\$
110	108, 103, 109	sylancr 663	. . . . . . . . . . . 12 $/\$ $\$
111		entr 7361	. . . . . . . . . . . 12 $/\$
112	107, 110, 111	syl2anc 661	. . . . . . . . . . 11 $/\$ $\$
113		domen1 7453	. . . . . . . . . . 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 1690	. . . . . 6 $\$ ^* $\/$
119	45, 118	syl5bi 217	. . . . 5 $\$ ^* $\/$
120	44, 119	pm2.61dne 2688	. . . 4 ^* $\/$
121	120	exlimiv 1688	. . 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 1369

wex 1586

wcel 1756

wne 2606

cvv 2972 $\$ cdif 3325

cun 3326

wss 3328

c0 3637

csn 3877 class class class wbr 4292

cxp 4838

ccnv 4839

cdm 4840

crn 4841

cres 4842

cima 4843

ccom 4844

wfun 5412

wfn 5413

wf 5414

wf1 5415

wfo 5416

wf1o 5417

cfv 5418

c1st 6575

cen 7307

cdom 7308

^* cwdom 7772

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-ral 2720 df-rex 2721 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-op 3884 df-uni 4092 df-int 4129 df-iun 4173 df-br 4293 df-opab 4351 df-mpt 4352 df-id 4636 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-1st 6577 df-2nd 6578 df-er 7101 df-en 7311 df-dom 7312 df-sdom 7313 df-wdom 7774

This theorem is referenced by: unxpwdom 7804 ttac 29385

W3C validator