unxpwdom2 - Metamath Proof Explorer

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

Theorem unxpwdom2 7799

Description: Lemma for unxpwdom 7800. (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 7354	. 2
2		bren 7315	. . 3
3		ssdif0 3734	. . . . . 6 $\$
4		dmxpid 5055	. . . . . . . . . . . . . 14
5		f1ofo 5645	. . . . . . . . . . . . . . . . 17
6		forn 5620	. . . . . . . . . . . . . . . . 17
7	5, 6	syl 16	. . . . . . . . . . . . . . . 16
8		vex 2973	. . . . . . . . . . . . . . . . 17
9	8	rnex 6511	. . . . . . . . . . . . . . . 16
10	7, 9	syl6eqelr 2530	. . . . . . . . . . . . . . 15
11		dmexg 6508	. . . . . . . . . . . . . . 15
12	10, 11	syl 16	. . . . . . . . . . . . . 14
13	4, 12	syl5eqelr 2526	. . . . . . . . . . . . 13
14		imassrn 5177	. . . . . . . . . . . . . 14
15		f1stres 6597	. . . . . . . . . . . . . . . 16
16		f1of 5638	. . . . . . . . . . . . . . . 16
17		fco 5565	. . . . . . . . . . . . . . . 16 $/\$
18	15, 16, 17	sylancr 658	. . . . . . . . . . . . . . 15
19		frn 5562	. . . . . . . . . . . . . . 15
20	18, 19	syl 16	. . . . . . . . . . . . . 14
21	14, 20	syl5ss 3364	. . . . . . . . . . . . 13
22	13, 21	ssexd 4436	. . . . . . . . . . . 12
23	22	adantr 462	. . . . . . . . . . 11 $/\$
24		simpr 458	. . . . . . . . . . 11 $/\$
25		ssdomg 7351	. . . . . . . . . . 11
26	23, 24, 25	sylc 60	. . . . . . . . . 10 $/\$
27		domwdom 7785	. . . . . . . . . 10 ^*
28	26, 27	syl 16	. . . . . . . . 9 $/\$ ^*
29		ffun 5558	. . . . . . . . . . . 12
30	18, 29	syl 16	. . . . . . . . . . 11
31		ssun1 3516	. . . . . . . . . . . 12
32		f1odm 5642	. . . . . . . . . . . . 13
33	8	dmex 6510	. . . . . . . . . . . . 13
34	32, 33	syl6eqelr 2530	. . . . . . . . . . . 12
35		ssexg 4435	. . . . . . . . . . . 12 $/\$
36	31, 34, 35	sylancr 658	. . . . . . . . . . 11
37		wdomima2g 7797	. . . . . . . . . . 11 $/\$ $/\$ ^*
38	30, 36, 22, 37	syl3anc 1213	. . . . . . . . . 10 ^*
39	38	adantr 462	. . . . . . . . 9 $/\$ ^*
40		wdomtr 7786	. . . . . . . . 9 ^* $/\$ ^* ^*
41	28, 39, 40	syl2anc 656	. . . . . . . 8 $/\$ ^*
42	41	orcd 392	. . . . . . 7 $/\$ ^* $\/$
43	42	ex 434	. . . . . 6 ^* $\/$
44	3, 43	syl5bir 218	. . . . 5 $\$ ^* $\/$
45		n0 3643	. . . . . 6 $\$ $\$
46		ssun2 3517	. . . . . . . . . . . . 13
47		ssexg 4435	. . . . . . . . . . . . 13 $/\$
48	46, 34, 47	sylancr 658	. . . . . . . . . . . 12
49	48	adantr 462	. . . . . . . . . . 11 $/\$ $\$
50		f1ofn 5639	. . . . . . . . . . . . . . 15
51		elpreima 5820	. . . . . . . . . . . . . . 15 $/\$
52	50, 51	syl 16	. . . . . . . . . . . . . 14 $/\$
53	52	adantr 462	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
54		elun 3494	. . . . . . . . . . . . . . . 16 $\/$
55		df-or 370	. . . . . . . . . . . . . . . 16 $\/$
56	54, 55	bitri 249	. . . . . . . . . . . . . . 15
57		eldifn 3476	. . . . . . . . . . . . . . . . . . 19 $\$
58	57	ad2antlr 721	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$
59	16	ad2antrr 720	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
60		simprr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
61	31, 60	sseldi 3351	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
62		fvco3 5765	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
63	59, 61, 62	syl2anc 656	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
64		eldifi 3475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
65	64	adantl 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$
66	65	snssd 4015	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$
67		xpss1 4944	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68	66, 67	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$
69	68	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $/\$
70		simprl 750	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $/\$
71	69, 70	sseldd 3354	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $/\$
72		fvres 5701	. . . . . . . . . . . . . . . . . . . . . . . 24
73	71, 72	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
74		xp1st 6605	. . . . . . . . . . . . . . . . . . . . . . . 24
75	70, 74	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
76	73, 75	eqeltrd 2515	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
77		elsni 3899	. . . . . . . . . . . . . . . . . . . . . 22
78	76, 77	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
79	63, 78	eqtrd 2473	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $/\$
80		ffn 5556	. . . . . . . . . . . . . . . . . . . . . . 23
81	18, 80	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
82	81	ad2antrr 720	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
83	31	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
84		fnfvima 5952	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
85	82, 83, 60, 84	syl3anc 1213	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $/\$
86	79, 85	eqeltrrd 2516	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $/\$
87	86	expr 612	. . . . . . . . . . . . . . . . . 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	imp3a 431	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
93	53, 92	sylbid 215	. . . . . . . . . . . 12 $/\$ $\$
94	93	ssrdv 3359	. . . . . . . . . . 11 $/\$ $\$
95		ssdomg 7351	. . . . . . . . . . 11
96	49, 94, 95	sylc 60	. . . . . . . . . 10 $/\$ $\$
97		f1ocnv 5650	. . . . . . . . . . . . . . 15
98		f1of1 5637	. . . . . . . . . . . . . . 15
99	97, 98	syl 16	. . . . . . . . . . . . . 14
100	99	adantr 462	. . . . . . . . . . . . 13 $/\$ $\$
101	34	adantr 462	. . . . . . . . . . . . 13 $/\$ $\$
102		snex 4530	. . . . . . . . . . . . . 14
103	13	adantr 462	. . . . . . . . . . . . . 14 $/\$ $\$
104		xpexg 6506	. . . . . . . . . . . . . 14 $/\$
105	102, 103, 104	sylancr 658	. . . . . . . . . . . . 13 $/\$ $\$
106		f1imaen2g 7366	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
107	100, 101, 68, 105, 106	syl22anc 1214	. . . . . . . . . . . 12 $/\$ $\$
108		vex 2973	. . . . . . . . . . . . 13
109		xpsnen2g 7400	. . . . . . . . . . . . 13 $/\$
110	108, 103, 109	sylancr 658	. . . . . . . . . . . 12 $/\$ $\$
111		entr 7357	. . . . . . . . . . . 12 $/\$
112	107, 110, 111	syl2anc 656	. . . . . . . . . . 11 $/\$ $\$
113		domen1 7449	. . . . . . . . . . 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 1695	. . . . . 6 $\$ ^* $\/$
119	45, 118	syl5bi 217	. . . . 5 $\$ ^* $\/$
120	44, 119	pm2.61dne 2686	. . . 4 ^* $\/$
121	120	exlimiv 1693	. . 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 1364

wex 1591

wcel 1761

wne 2604

cvv 2970 $\$ cdif 3322

cun 3323

wss 3325

c0 3634

csn 3874 class class class wbr 4289

cxp 4834

ccnv 4835

cdm 4836

crn 4837

cres 4838

cima 4839

ccom 4840

wfun 5409

wfn 5410

wf 5411

wf1 5412

wfo 5413

wf1o 5414

cfv 5415

c1st 6574

cen 7303

cdom 7304

^* cwdom 7768

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2263 df-mo 2264 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-ral 2718 df-rex 2719 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-id 4632 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-1st 6576 df-2nd 6577 df-er 7097 df-en 7307 df-dom 7308 df-sdom 7309 df-wdom 7770

This theorem is referenced by: unxpwdom 7800 ttac 29294

W3C validator