unxpwdom2 - Metamath Proof Explorer

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

Theorem unxpwdom2 8014

Description: Lemma for unxpwdom 8015. (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 7564	. 2
2		bren 7525	. . 3
3		ssdif0 3885	. . . . . 6 $\$
4		dmxpid 5222	. . . . . . . . . . . . . 14
5		f1ofo 5823	. . . . . . . . . . . . . . . . 17
6		forn 5798	. . . . . . . . . . . . . . . . 17
7	5, 6	syl 16	. . . . . . . . . . . . . . . 16
8		vex 3116	. . . . . . . . . . . . . . . . 17
9	8	rnex 6718	. . . . . . . . . . . . . . . 16
10	7, 9	syl6eqelr 2564	. . . . . . . . . . . . . . 15
11		dmexg 6715	. . . . . . . . . . . . . . 15
12	10, 11	syl 16	. . . . . . . . . . . . . 14
13	4, 12	syl5eqelr 2560	. . . . . . . . . . . . 13
14		imassrn 5348	. . . . . . . . . . . . . 14
15		f1stres 6806	. . . . . . . . . . . . . . . 16
16		f1of 5816	. . . . . . . . . . . . . . . 16
17		fco 5741	. . . . . . . . . . . . . . . 16 $/\$
18	15, 16, 17	sylancr 663	. . . . . . . . . . . . . . 15
19		frn 5737	. . . . . . . . . . . . . . 15
20	18, 19	syl 16	. . . . . . . . . . . . . 14
21	14, 20	syl5ss 3515	. . . . . . . . . . . . 13
22	13, 21	ssexd 4594	. . . . . . . . . . . 12
23	22	adantr 465	. . . . . . . . . . 11 $/\$
24		simpr 461	. . . . . . . . . . 11 $/\$
25		ssdomg 7561	. . . . . . . . . . 11
26	23, 24, 25	sylc 60	. . . . . . . . . 10 $/\$
27		domwdom 8000	. . . . . . . . . 10 ^*
28	26, 27	syl 16	. . . . . . . . 9 $/\$ ^*
29		ffun 5733	. . . . . . . . . . . 12
30	18, 29	syl 16	. . . . . . . . . . 11
31		ssun1 3667	. . . . . . . . . . . 12
32		f1odm 5820	. . . . . . . . . . . . 13
33	8	dmex 6717	. . . . . . . . . . . . 13
34	32, 33	syl6eqelr 2564	. . . . . . . . . . . 12
35		ssexg 4593	. . . . . . . . . . . 12 $/\$
36	31, 34, 35	sylancr 663	. . . . . . . . . . 11
37		wdomima2g 8012	. . . . . . . . . . 11 $/\$ $/\$ ^*
38	30, 36, 22, 37	syl3anc 1228	. . . . . . . . . 10 ^*
39	38	adantr 465	. . . . . . . . 9 $/\$ ^*
40		wdomtr 8001	. . . . . . . . 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 3794	. . . . . 6 $\$ $\$
46		ssun2 3668	. . . . . . . . . . . . 13
47		ssexg 4593	. . . . . . . . . . . . 13 $/\$
48	46, 34, 47	sylancr 663	. . . . . . . . . . . 12
49	48	adantr 465	. . . . . . . . . . 11 $/\$ $\$
50		f1ofn 5817	. . . . . . . . . . . . . . 15
51		elpreima 6001	. . . . . . . . . . . . . . 15 $/\$
52	50, 51	syl 16	. . . . . . . . . . . . . 14 $/\$
53	52	adantr 465	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
54		elun 3645	. . . . . . . . . . . . . . . 16 $\/$
55		df-or 370	. . . . . . . . . . . . . . . 16 $\/$
56	54, 55	bitri 249	. . . . . . . . . . . . . . 15
57		eldifn 3627	. . . . . . . . . . . . . . . . . . 19 $\$
58	57	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$
59	16	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
60		simprr 756	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
61	31, 60	sseldi 3502	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
62		fvco3 5944	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
63	59, 61, 62	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
64		eldifi 3626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
65	64	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$
66	65	snssd 4172	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$
67		xpss1 5111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68	66, 67	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$
69	68	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $/\$
70		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $/\$
71	69, 70	sseldd 3505	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $/\$
72		fvres 5880	. . . . . . . . . . . . . . . . . . . . . . . 24
73	71, 72	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
74		xp1st 6814	. . . . . . . . . . . . . . . . . . . . . . . 24
75	70, 74	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
76	73, 75	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
77		elsni 4052	. . . . . . . . . . . . . . . . . . . . . 22
78	76, 77	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
79	63, 78	eqtrd 2508	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $/\$
80		ffn 5731	. . . . . . . . . . . . . . . . . . . . . . 23
81	18, 80	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
82	81	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
83	31	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
84		fnfvima 6138	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
85	82, 83, 60, 84	syl3anc 1228	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $/\$
86	79, 85	eqeltrrd 2556	. . . . . . . . . . . . . . . . . . 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 3510	. . . . . . . . . . 11 $/\$ $\$
95		ssdomg 7561	. . . . . . . . . . 11
96	49, 94, 95	sylc 60	. . . . . . . . . 10 $/\$ $\$
97		f1ocnv 5828	. . . . . . . . . . . . . . 15
98		f1of1 5815	. . . . . . . . . . . . . . 15
99	97, 98	syl 16	. . . . . . . . . . . . . 14
100	99	adantr 465	. . . . . . . . . . . . 13 $/\$ $\$
101	34	adantr 465	. . . . . . . . . . . . 13 $/\$ $\$
102		snex 4688	. . . . . . . . . . . . . 14
103	13	adantr 465	. . . . . . . . . . . . . 14 $/\$ $\$
104		xpexg 6586	. . . . . . . . . . . . . 14 $/\$
105	102, 103, 104	sylancr 663	. . . . . . . . . . . . 13 $/\$ $\$
106		f1imaen2g 7576	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
107	100, 101, 68, 105, 106	syl22anc 1229	. . . . . . . . . . . 12 $/\$ $\$
108		vex 3116	. . . . . . . . . . . . 13
109		xpsnen2g 7610	. . . . . . . . . . . . 13 $/\$
110	108, 103, 109	sylancr 663	. . . . . . . . . . . 12 $/\$ $\$
111		entr 7567	. . . . . . . . . . . 12 $/\$
112	107, 110, 111	syl2anc 661	. . . . . . . . . . 11 $/\$ $\$
113		domen1 7659	. . . . . . . . . . 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 1700	. . . . . 6 $\$ ^* $\/$
119	45, 118	syl5bi 217	. . . . 5 $\$ ^* $\/$
120	44, 119	pm2.61dne 2784	. . . 4 ^* $\/$
121	120	exlimiv 1698	. . 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 1379

wex 1596

wcel 1767

wne 2662

cvv 3113 $\$ cdif 3473

cun 3474

wss 3476

c0 3785

csn 4027 class class class wbr 4447

cxp 4997

ccnv 4998

cdm 4999

crn 5000

cres 5001

cima 5002

ccom 5003

wfun 5582

wfn 5583

wf 5584

wf1 5585

wfo 5586

wf1o 5587

cfv 5588

c1st 6782

cen 7513

cdom 7514

^* cwdom 7983

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-id 4795 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-1st 6784 df-2nd 6785 df-er 7311 df-en 7517 df-dom 7518 df-sdom 7519 df-wdom 7985

This theorem is referenced by: unxpwdom 8015 ttac 30610

W3C validator