unxpwdom2 - Metamath Proof Explorer

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

Theorem unxpwdom2 8090

Description: Lemma for unxpwdom 8091. (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 7605	. 2
2		bren 7565	. . 3
3		ssdif0 3791	. . . . . 6 $\$
4		dmxpid 5032	. . . . . . . . . . . . . 14
5		f1ofo 5804	. . . . . . . . . . . . . . . . 17
6		forn 5779	. . . . . . . . . . . . . . . . 17
7	5, 6	syl 17	. . . . . . . . . . . . . . . 16
8		vex 3016	. . . . . . . . . . . . . . . . 17
9	8	rnex 6715	. . . . . . . . . . . . . . . 16
10	7, 9	syl6eqelr 2539	. . . . . . . . . . . . . . 15
11		dmexg 6712	. . . . . . . . . . . . . . 15
12	10, 11	syl 17	. . . . . . . . . . . . . 14
13	4, 12	syl5eqelr 2535	. . . . . . . . . . . . 13
14		imassrn 5157	. . . . . . . . . . . . . 14
15		f1stres 6803	. . . . . . . . . . . . . . . 16
16		f1of 5797	. . . . . . . . . . . . . . . 16
17		fco 5722	. . . . . . . . . . . . . . . 16 $/\$
18	15, 16, 17	sylancr 674	. . . . . . . . . . . . . . 15
19		frn 5718	. . . . . . . . . . . . . . 15
20	18, 19	syl 17	. . . . . . . . . . . . . 14
21	14, 20	syl5ss 3411	. . . . . . . . . . . . 13
22	13, 21	ssexd 4522	. . . . . . . . . . . 12
23	22	adantr 471	. . . . . . . . . . 11 $/\$
24		simpr 467	. . . . . . . . . . 11 $/\$
25		ssdomg 7602	. . . . . . . . . . 11
26	23, 24, 25	sylc 62	. . . . . . . . . 10 $/\$
27		domwdom 8076	. . . . . . . . . 10 ^*
28	26, 27	syl 17	. . . . . . . . 9 $/\$ ^*
29		ffun 5714	. . . . . . . . . . . 12
30	18, 29	syl 17	. . . . . . . . . . 11
31		ssun1 3565	. . . . . . . . . . . 12
32		f1odm 5801	. . . . . . . . . . . . 13
33	8	dmex 6714	. . . . . . . . . . . . 13
34	32, 33	syl6eqelr 2539	. . . . . . . . . . . 12
35		ssexg 4521	. . . . . . . . . . . 12 $/\$
36	31, 34, 35	sylancr 674	. . . . . . . . . . 11
37		wdomima2g 8088	. . . . . . . . . . 11 $/\$ $/\$ ^*
38	30, 36, 22, 37	syl3anc 1271	. . . . . . . . . 10 ^*
39	38	adantr 471	. . . . . . . . 9 $/\$ ^*
40		wdomtr 8077	. . . . . . . . 9 ^* $/\$ ^* ^*
41	28, 39, 40	syl2anc 671	. . . . . . . 8 $/\$ ^*
42	41	orcd 398	. . . . . . 7 $/\$ ^* $\/$
43	42	ex 440	. . . . . 6 ^* $\/$
44	3, 43	syl5bir 226	. . . . 5 $\$ ^* $\/$
45		n0 3709	. . . . . 6 $\$ $\$
46		ssun2 3566	. . . . . . . . . . . . 13
47		ssexg 4521	. . . . . . . . . . . . 13 $/\$
48	46, 34, 47	sylancr 674	. . . . . . . . . . . 12
49	48	adantr 471	. . . . . . . . . . 11 $/\$ $\$
50		f1ofn 5798	. . . . . . . . . . . . . . 15
51		elpreima 5986	. . . . . . . . . . . . . . 15 $/\$
52	50, 51	syl 17	. . . . . . . . . . . . . 14 $/\$
53	52	adantr 471	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
54		elun 3542	. . . . . . . . . . . . . . . 16 $\/$
55		df-or 376	. . . . . . . . . . . . . . . 16 $\/$
56	54, 55	bitri 257	. . . . . . . . . . . . . . 15
57		eldifn 3524	. . . . . . . . . . . . . . . . . . 19 $\$
58	57	ad2antlr 738	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$
59	16	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
60		simprr 771	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
61	31, 60	sseldi 3398	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
62		fvco3 5926	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
63	59, 61, 62	syl2anc 671	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
64		eldifi 3523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
65	64	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$
66	65	snssd 4086	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$
67		xpss1 4921	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68	66, 67	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$
69	68	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $/\$
70		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $/\$
71	69, 70	sseldd 3401	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $/\$
72		fvres 5862	. . . . . . . . . . . . . . . . . . . . . . . 24
73	71, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
74		xp1st 6811	. . . . . . . . . . . . . . . . . . . . . . . 24
75	70, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$
76	73, 75	eqeltrd 2530	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$
77		elsni 3961	. . . . . . . . . . . . . . . . . . . . . 22
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
79	63, 78	eqtrd 2486	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $/\$
80		ffn 5711	. . . . . . . . . . . . . . . . . . . . . . 23
81	18, 80	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
82	81	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
83	31	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $/\$
84		fnfvima 6129	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
85	82, 83, 60, 84	syl3anc 1271	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $/\$
86	79, 85	eqeltrrd 2531	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $/\$
87	86	expr 624	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$
88	58, 87	mtod 182	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$
89	88	ex 440	. . . . . . . . . . . . . . . 16 $/\$ $\$
90	89	imim1d 78	. . . . . . . . . . . . . . 15 $/\$ $\$
91	56, 90	syl5bi 225	. . . . . . . . . . . . . 14 $/\$ $\$
92	91	impd 437	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
93	53, 92	sylbid 223	. . . . . . . . . . . 12 $/\$ $\$
94	93	ssrdv 3406	. . . . . . . . . . 11 $/\$ $\$
95		ssdomg 7602	. . . . . . . . . . 11
96	49, 94, 95	sylc 62	. . . . . . . . . 10 $/\$ $\$
97		f1ocnv 5809	. . . . . . . . . . . . . . 15
98		f1of1 5796	. . . . . . . . . . . . . . 15
99	97, 98	syl 17	. . . . . . . . . . . . . 14
100	99	adantr 471	. . . . . . . . . . . . 13 $/\$ $\$
101	34	adantr 471	. . . . . . . . . . . . 13 $/\$ $\$
102		snex 4614	. . . . . . . . . . . . . 14
103	13	adantr 471	. . . . . . . . . . . . . 14 $/\$ $\$
104		xpexg 6581	. . . . . . . . . . . . . 14 $/\$
105	102, 103, 104	sylancr 674	. . . . . . . . . . . . 13 $/\$ $\$
106		f1imaen2g 7617	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
107	100, 101, 68, 105, 106	syl22anc 1272	. . . . . . . . . . . 12 $/\$ $\$
108		vex 3016	. . . . . . . . . . . . 13
109		xpsnen2g 7652	. . . . . . . . . . . . 13 $/\$
110	108, 103, 109	sylancr 674	. . . . . . . . . . . 12 $/\$ $\$
111		entr 7608	. . . . . . . . . . . 12 $/\$
112	107, 110, 111	syl2anc 671	. . . . . . . . . . 11 $/\$ $\$
113		domen1 7701	. . . . . . . . . . 11
114	112, 113	syl 17	. . . . . . . . . 10 $/\$ $\$
115	96, 114	mpbid 215	. . . . . . . . 9 $/\$ $\$
116	115	olcd 399	. . . . . . . 8 $/\$ $\$ ^* $\/$
117	116	ex 440	. . . . . . 7 $\$ ^* $\/$
118	117	exlimdv 1783	. . . . . 6 $\$ ^* $\/$
119	45, 118	syl5bi 225	. . . . 5 $\$ ^* $\/$
120	44, 119	pm2.61dne 2710	. . . 4 ^* $\/$
121	120	exlimiv 1780	. . 3 ^* $\/$
122	2, 121	sylbi 200	. 2 ^* $\/$
123	1, 122	syl 17	1 ^* $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 374 $/\$ wa 375

wceq 1448

wex 1667

wcel 1891

wne 2622

cvv 3013 $\$ cdif 3369

cun 3370

wss 3372

c0 3699

csn 3936 class class class wbr 4374

cxp 4810

ccnv 4811

cdm 4812

crn 4813

cres 4814

cima 4815

ccom 4816

wfun 5555

wfn 5556

wf 5557

wf1 5558

wfo 5559

wf1o 5560

cfv 5561

c1st 6779

cen 7553

cdom 7554

^* cwdom 8059

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-8 1893 ax-9 1900 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 ax-sep 4497 ax-nul 4506 ax-pow 4554 ax-pr 4612 ax-un 6571

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 988 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-eu 2304 df-mo 2305 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3015 df-sbc 3236 df-csb 3332 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-nul 3700 df-if 3850 df-pw 3921 df-sn 3937 df-pr 3939 df-op 3943 df-uni 4169 df-int 4205 df-iun 4250 df-br 4375 df-opab 4434 df-mpt 4435 df-id 4727 df-xp 4818 df-rel 4819 df-cnv 4820 df-co 4821 df-dm 4822 df-rn 4823 df-res 4824 df-ima 4825 df-iota 5525 df-fun 5563 df-fn 5564 df-f 5565 df-f1 5566 df-fo 5567 df-f1o 5568 df-fv 5569 df-1st 6781 df-2nd 6782 df-er 7350 df-en 7557 df-dom 7558 df-sdom 7559 df-wdom 8061

This theorem is referenced by: unxpwdom 8091 ttac 35893

W3C validator