marypha1lem - Metamath Proof Explorer

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

Theorem marypha1lem 8339

Description: Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.)

**Assertion**
Ref	Expression
marypha1lem

Distinct variable group:

Proof of Theorem marypha1lem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpeq1 5128	. . . . 5
2	1	pweqd 4163	. . . 4
3		pweq 4161	. . . . . 6
4	3	raleqdv 3144	. . . . 5
5		f1eq2 6097	. . . . . 6
6	5	rexbidv 3052	. . . . 5
7	4, 6	imbi12d 334	. . . 4
8	2, 7	raleqbidv 3152	. . 3
9	8	imbi2d 330	. 2
10		xpeq1 5128	. . . . 5
11	10	pweqd 4163	. . . 4
12		pweq 4161	. . . . . 6
13	12	raleqdv 3144	. . . . 5
14		f1eq2 6097	. . . . . 6
15	14	rexbidv 3052	. . . . 5
16	13, 15	imbi12d 334	. . . 4
17	11, 16	raleqbidv 3152	. . 3
18	17	imbi2d 330	. 2
19		bi2.04 376	. . . . 5
20	19	albii 1747	. . . 4
21		19.21v 1868	. . . 4
22	20, 21	bitri 264	. . 3
23		0elpw 4834	. . . . . . . . . . . . 13
24		f10 6169	. . . . . . . . . . . . 13
25		f1eq1 6096	. . . . . . . . . . . . . 14
26	25	rspcev 3309	. . . . . . . . . . . . 13 $/\$
27	23, 24, 26	mp2an 708	. . . . . . . . . . . 12
28		f1eq2 6097	. . . . . . . . . . . . 13
29	28	rexbidv 3052	. . . . . . . . . . . 12
30	27, 29	mpbiri 248	. . . . . . . . . . 11
31	30	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		n0 3931	. . . . . . . . . . 11
33		snelpwi 4912	. . . . . . . . . . . . . . . . . . 19
34		id 22	. . . . . . . . . . . . . . . . . . . . . . 23
35		imaeq2 5462	. . . . . . . . . . . . . . . . . . . . . . 23
36	34, 35	breq12d 4666	. . . . . . . . . . . . . . . . . . . . . 22
37	36	rspcva 3307	. . . . . . . . . . . . . . . . . . . . 21 $/\$
38		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . 25
39	38	snnz 4309	. . . . . . . . . . . . . . . . . . . . . . . 24
40		snex 4908	. . . . . . . . . . . . . . . . . . . . . . . . 25
41	40	0sdom 8091	. . . . . . . . . . . . . . . . . . . . . . . 24
42	39, 41	mpbir 221	. . . . . . . . . . . . . . . . . . . . . . 23
43		sdomdomtr 8093	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
44	42, 43	mpan 706	. . . . . . . . . . . . . . . . . . . . . 22
45		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . 24
46	45	imaex 7104	. . . . . . . . . . . . . . . . . . . . . . 23
47	46	0sdom 8091	. . . . . . . . . . . . . . . . . . . . . 22
48	44, 47	sylib 208	. . . . . . . . . . . . . . . . . . . . 21
49	37, 48	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
50	49	expcom 451	. . . . . . . . . . . . . . . . . . 19
51	33, 50	syl5 34	. . . . . . . . . . . . . . . . . 18
52	51	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
53	52	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54	53	impr 649	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		n0 3931	. . . . . . . . . . . . . . 15
56	54, 55	sylib 208	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	45	imaex 7104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
58	57	difexi 4809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
59	58	0dom 8090	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
60		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
61	59, 60	mpbiri 248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$
63		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
64		elpwi 4168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$
65	64	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $\$ $/\$ $\$
66		difsnpss 4338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$
67	66	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$
68	67	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $\$ $/\$ $\$
69	65, 68	sspsstrd 3715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $\$ $/\$
70		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $\$ $/\$
71	69, 70	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
72		psseq1 3694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
73		neeq1 2856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
74	72, 73	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
75		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
76		imaeq2 5462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
77	75, 76	breq12d 4666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
78	74, 77	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
79	78	spv 2260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
80	63, 71, 79	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $\$ $/\$
81		domdifsn 8043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $/\$ $\$
83	82	expr 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$
84	62, 83	pm2.61dne 2880	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$
85	84	adantlrr 757	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $\$ $\$
86	85	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
87		df-ss 3588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
88	64, 87	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
89	88	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
90	89	ineq1d 3813	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$ $\$ $\$
91	90	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
92		indif2 3870	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
93		imassrn 5477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
94		elpwi 4168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
95		rnss 5354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
96		rnxpss 5566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
97	95, 96	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
98	94, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
99	93, 98	syl5ss 3614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
100		df-ss 3588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
101	99, 100	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
102	101	difeq1d 3727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
103	102	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$
104	92, 103	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$
105	104	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
106	91, 105	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
107	86, 106	breqtrrd 4681	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
108	107	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
109		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25
110		imainrect 5575	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $\$ $\$
111		imaeq2 5462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $\$ $\$
112	110, 111	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
113	109, 112	breq12d 4666	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$
114	113	cbvralv 3171	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$ $\$ $\$
115	108, 114	sylib 208	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
116	115	adantllr 755	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
117		inss2 3834	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$
118		difss 3737	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
119		xpss2 5229	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$
121	117, 120	sstri 3612	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$
122	45	inex1 4799	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
123	122	elpw 4164	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$ $\$ $\$
124	121, 123	mpbir 221	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$
125		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	67	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$
127	126	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
128		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . 25
129	128	difexi 4809	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
130		psseq1 3694	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
131		xpeq1 5128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
132	131	pweqd 4163	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
133		pweq 4161	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
134	133	raleqdv 3144	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
135		f1eq2 6097	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
136	135	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
137	134, 136	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $\$
138	132, 137	raleqbidv 3152	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
139	130, 138	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$ $\$
140	129, 139	spcv 3299	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$
141	125, 127, 140	sylc 65	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
142		imaeq1 5461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $\$ $\$
143	142	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
144	143	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$ $\$ $\$
145		pweq 4161	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
146	145	rexeqdv 3145	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$ $\$ $\$
147	144, 146	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
148	147	rspcva 3307	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
149	124, 141, 148	sylancr 695	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
150	116, 149	mpd 15	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
151		f1eq1 6096	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
152	151	cbvrexv 3172	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $\$ $\$ $\$
153	150, 152	sylib 208	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
154		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
155	38, 154	elimasn 5490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
156	155	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
157	156	snssd 4340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
158	157	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $\$
159		elpwi 4168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $\$ $\$
160		inss1 3833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
161	159, 160	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
162	161	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $\$
163	158, 162	unssd 3789	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $\$
164	45	elpw2 4828	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
165	163, 164	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$
166	165	ad2ant2lr 784	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
167	38, 154	f1osn 6176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
168	167	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$ $/\$ $\$
169		f1f1orn 6148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
170	169	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$ $/\$ $\$ $\$
171		disjdif 4040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$ $/\$ $\$ $\$
173		incom 3805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
174	159, 117	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$ $\$ $\$
175		rnss 5354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$ $\$ $\$ $\$
176		rnxpss 5566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$ $\$ $\$
177	175, 176	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$ $\$
178	174, 177	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$ $\$
179		incom 3805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$
180		disjdif 4040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$
181	179, 180	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$
182		ssdisj 4026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $/\$ $\$
183	178, 181, 182	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
184	173, 183	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
185	184	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$ $/\$ $\$
186		f1oun 6156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\$ $/\$ $\$ $/\$ $\$
187	168, 170, 172, 185, 186	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$ $/\$ $\$ $\$
188	187	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
189		snssi 4339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
190	189	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
191		undif 4049	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
192	190, 191	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$
193		f1oeq2 6128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
194	192, 193	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$
195	194	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
196	188, 195	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
197		f1of1 6136	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
198		ssv 3625	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
199		f1ss 6106	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
200	197, 198, 199	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
201	196, 200	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
202		f1eq1 6096	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
203	202	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
204	166, 201, 203	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
205	204	rexlimdvaa 3032	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $\$ $\$
206	205	ex 450	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $\$ $\$
207	206	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
208	207	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
209	208	impr 649	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
210	209	adantllr 755	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
211	153, 210	mpd 15	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
212	211	expr 643	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
213	212	expd 452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
214	213	impr 649	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
215	214	exlimdv 1861	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
216	56, 215	mpd 15	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
217	216	expr 643	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
218	217	exlimdv 1861	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
219	32, 218	syl5bi 232	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
220	31, 219	pm2.61dne 2880	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
221		exanali 1786	. . . . . . . . . 10 $/\$ $/\$ $/\$
222		simprll 802	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
223		pssss 3702	. . . . . . . . . . . . . . . . . . . 20
224	222, 223	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
225		sspwb 4917	. . . . . . . . . . . . . . . . . . 19
226	224, 225	sylib 208	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
227		simplrr 801	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
228		ssralv 3666	. . . . . . . . . . . . . . . . . 18
229	226, 227, 228	sylc 65	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
230		elpwi 4168	. . . . . . . . . . . . . . . . . . . . 21
231		resima2 5432	. . . . . . . . . . . . . . . . . . . . 21
232	230, 231	syl 17	. . . . . . . . . . . . . . . . . . . 20
233	232	eqcomd 2628	. . . . . . . . . . . . . . . . . . 19
234	233	breq2d 4665	. . . . . . . . . . . . . . . . . 18
235	234	ralbiia 2979	. . . . . . . . . . . . . . . . 17
236	229, 235	sylib 208	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
237		simplrl 800	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
238		ssres 5424	. . . . . . . . . . . . . . . . . . . . 21
239		df-res 5126	. . . . . . . . . . . . . . . . . . . . . 22
240		inxp 5254	. . . . . . . . . . . . . . . . . . . . . . 23
241		inss2 3834	. . . . . . . . . . . . . . . . . . . . . . . 24
242		inss1 3833	. . . . . . . . . . . . . . . . . . . . . . . 24
243		xpss12 5225	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
244	241, 242, 243	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . 23
245	240, 244	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . . 22
246	239, 245	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . 21
247	238, 246	syl6ss 3615	. . . . . . . . . . . . . . . . . . . 20
248	94, 247	syl 17	. . . . . . . . . . . . . . . . . . 19
249	45	resex 5443	. . . . . . . . . . . . . . . . . . . 20
250	249	elpw 4164	. . . . . . . . . . . . . . . . . . 19
251	248, 250	sylibr 224	. . . . . . . . . . . . . . . . . 18
252	237, 251	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
253		simpllr 799	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
254		psseq1 3694	. . . . . . . . . . . . . . . . . . . 20
255		xpeq1 5128	. . . . . . . . . . . . . . . . . . . . . 22
256	255	pweqd 4163	. . . . . . . . . . . . . . . . . . . . 21
257		pweq 4161	. . . . . . . . . . . . . . . . . . . . . . 23
258	257	raleqdv 3144	. . . . . . . . . . . . . . . . . . . . . 22
259		f1eq2 6097	. . . . . . . . . . . . . . . . . . . . . . 23
260	259	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . 22
261	258, 260	imbi12d 334	. . . . . . . . . . . . . . . . . . . . 21
262	256, 261	raleqbidv 3152	. . . . . . . . . . . . . . . . . . . 20
263	254, 262	imbi12d 334	. . . . . . . . . . . . . . . . . . 19
264	263	spv 2260	. . . . . . . . . . . . . . . . . 18
265	253, 222, 264	sylc 65	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
266		imaeq1 5461	. . . . . . . . . . . . . . . . . . . . 21
267	266	breq2d 4665	. . . . . . . . . . . . . . . . . . . 20
268	267	ralbidv 2986	. . . . . . . . . . . . . . . . . . 19
269		pweq 4161	. . . . . . . . . . . . . . . . . . . 20
270	269	rexeqdv 3145	. . . . . . . . . . . . . . . . . . 19
271	268, 270	imbi12d 334	. . . . . . . . . . . . . . . . . 18
272	271	rspcva 3307	. . . . . . . . . . . . . . . . 17 $/\$
273	252, 265, 272	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
274	236, 273	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
275		f1eq1 6096	. . . . . . . . . . . . . . . 16
276	275	cbvrexv 3172	. . . . . . . . . . . . . . 15
277	274, 276	sylib 208	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
278	223	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
279	278	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
280		elpwi 4168	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
281		difss 3737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
282	280, 281	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
283	282	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
284	279, 283	unssd 3789	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
285	128	elpw2 4828	. . . . . . . . . . . . . . . . . . . . . . . . 25
286	284, 285	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
287		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
288	287	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
289		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26
290		imaeq2 5462	. . . . . . . . . . . . . . . . . . . . . . . . . 26
291	289, 290	breq12d 4666	. . . . . . . . . . . . . . . . . . . . . . . . 25
292	291	rspcva 3307	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
293	286, 288, 292	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
294		imaundi 5545	. . . . . . . . . . . . . . . . . . . . . . . 24
295		undif2 4044	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
296	294, 295	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
297	293, 296	syl6breq 4694	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
298		simp-4l 806	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
299	298, 279	ssfid 8183	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
300		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
301	300	elpw 4164	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
302	279, 301	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
303		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
304		imaeq2 5462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
305	303, 304	breq12d 4666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
306	305	rspcva 3307	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
307	302, 288, 306	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
308		simplrr 801	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
309		bren2 7986	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
310	307, 308, 309	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
311	310	ensymd 8007	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
312		incom 3805	. . . . . . . . . . . . . . . . . . . . . . . . . 26
313		ssdifin0 4050	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
314	312, 313	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
315	280, 314	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
316	315	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
317		disjdif 4040	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
318	317	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
319		domunfican 8233	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$ $\$ $\$
320	299, 311, 316, 318, 319	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
321	297, 320	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
322	101	difeq1d 3727	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
323	322	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$
324	323	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
325	321, 324	breqtrrd 4681	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
326		df-ss 3588	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
327	280, 326	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
328	327	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
329	328	ineq1d 3813	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$ $\$
330		indif2 3870	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
331	329, 330	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$ $\$
332	331	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
333	325, 332	breqtrrd 4681	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
334	333	ralrimiva 2966	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
335		imainrect 5575	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$ $\$
336		imaeq2 5462	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$ $\$
337	335, 336	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $\$
338	109, 337	breq12d 4666	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $\$
339	338	cbvralv 3171	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$ $\$ $\$ $\$
340	334, 339	sylib 208	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
341	340	adantllr 755	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
342		inss2 3834	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $\$
343		difss 3737	. . . . . . . . . . . . . . . . . . . 20 $\$
344		xpss2 5229	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $\$
345	343, 344	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
346	342, 345	sstri 3612	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
347	45	inex1 4799	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
348	347	elpw 4164	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$ $\$ $\$ $\$
349	346, 348	mpbir 221	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
350		incom 3805	. . . . . . . . . . . . . . . . . . . . . . 23
351		df-ss 3588	. . . . . . . . . . . . . . . . . . . . . . . 24
352	223, 351	sylib 208	. . . . . . . . . . . . . . . . . . . . . . 23
353	350, 352	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . 22
354	353	neeq1d 2853	. . . . . . . . . . . . . . . . . . . . 21
355	354	biimpar 502	. . . . . . . . . . . . . . . . . . . 20 $/\$
356		disj4 4025	. . . . . . . . . . . . . . . . . . . . . 22 $\$
357	356	bicomi 214	. . . . . . . . . . . . . . . . . . . . 21 $\$
358	357	necon1abii 2842	. . . . . . . . . . . . . . . . . . . 20 $\$
359	355, 358	sylib 208	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
360	359	ad2antrl 764	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
361	128	difexi 4809	. . . . . . . . . . . . . . . . . . 19 $\$
362		psseq1 3694	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
363		xpeq1 5128	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
364	363	pweqd 4163	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
365		pweq 4161	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
366	365	raleqdv 3144	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
367		f1eq2 6097	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
368	367	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
369	366, 368	imbi12d 334	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$
370	364, 369	raleqbidv 3152	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $\$
371	362, 370	imbi12d 334	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $\$ $\$
372	361, 371	spcv 3299	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$ $\$
373	253, 360, 372	sylc 65	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
374		imaeq1 5461	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$ $\$
375	374	breq2d 4665	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $\$
376	375	ralbidv 2986	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $\$ $\$ $\$
377		pweq 4161	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $\$
378	377	rexeqdv 3145	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $\$ $\$ $\$
379	376, 378	imbi12d 334	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
380	379	rspcva 3307	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
381	349, 373, 380	sylancr 695	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
382	341, 381	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
383		f1eq1 6096	. . . . . . . . . . . . . . . 16 $\$ $\$
384	383	cbvrexv 3172	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$ $\$ $\$
385	382, 384	sylib 208	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
386		elpwi 4168	. . . . . . . . . . . . . . . . . . . . . . 23
387		resss 5422	. . . . . . . . . . . . . . . . . . . . . . 23
388	386, 387	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . 22
389	388	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
390	389	ad2antlr 763	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
391		elpwi 4168	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$ $\$
392		inss1 3833	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
393	391, 392	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
394	393	ad2antrl 764	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
395	390, 394	unssd 3789	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
396	45	elpw2 4828	. . . . . . . . . . . . . . . . . . 19
397	395, 396	sylibr 224	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
398		f1f1orn 6148	. . . . . . . . . . . . . . . . . . . . . . . 24
399	398	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
400	399	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
401		f1f1orn 6148	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
402	401	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
403		disjdif 4040	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
404	403	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
405		rnss 5354	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
406	386, 405	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
407		df-ima 5127	. . . . . . . . . . . . . . . . . . . . . . . . . 26
408	406, 407	syl6sseqr 3652	. . . . . . . . . . . . . . . . . . . . . . . . 25
409	408	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
410	409	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
411		incom 3805	. . . . . . . . . . . . . . . . . . . . . . . 24
412	391, 342	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$ $\$ $\$
413		rnss 5354	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$ $\$ $\$
414	412, 413	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$ $\$ $\$
415		rnxpss 5566	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$ $\$
416	414, 415	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $\$
417	416	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
418		incom 3805	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
419		disjdif 4040	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
420	418, 419	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
421		ssdisj 4026	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$
422	417, 420, 421	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
423	411, 422	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
424		ssdisj 4026	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
425	410, 423, 424	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
426		f1oun 6156	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $\$ $/\$ $\$
427	400, 402, 404, 425, 426	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
428		undif 4049	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
429	428	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
430	429	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$
431	430	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
432		f1oeq2 6128	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
433	431, 432	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
434	427, 433	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
435		f1of1 6136	. . . . . . . . . . . . . . . . . . . 20
436	434, 435	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
437		ssv 3625	. . . . . . . . . . . . . . . . . . 19
438		f1ss 6106	. . . . . . . . . . . . . . . . . . 19 $/\$
439	436, 437, 438	sylancl 694	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
440		f1eq1 6096	. . . . . . . . . . . . . . . . . . 19
441	440	rspcev 3309	. . . . . . . . . . . . . . . . . 18 $/\$
442	397, 439, 441	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
443	442	rexlimdvaa 3032	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $\$ $\$
444	443	rexlimdvaa 3032	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$ $\$
445	237, 224, 444	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
446	277, 385, 445	mp2d 49	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
447	446	ex 450	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
448	447	exlimdv 1861	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
449	448	imp 445	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
450	221, 449	sylan2br 493	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
451	220, 450	pm2.61dan 832	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
452	451	exp32 631	. . . . . . 7 $/\$ $/\$
453	452	ralrimiv 2965	. . . . . 6 $/\$ $/\$
454		imaeq1 5461	. . . . . . . . . 10
455	454	breq2d 4665	. . . . . . . . 9
456	455	ralbidv 2986	. . . . . . . 8
457		pweq 4161	. . . . . . . . 9
458	457	rexeqdv 3145	. . . . . . . 8
459	456, 458	imbi12d 334	. . . . . . 7
460	459	cbvralv 3171	. . . . . 6
461	453, 460	sylib 208	. . . . 5 $/\$ $/\$
462	461	exp31 630	. . . 4
463	462	a2d 29	. . 3
464	22, 463	syl5bi 232	. 2
465	9, 18, 464	findcard3 8203	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384

wal 1481

wceq 1483

wex 1704

wcel 1990

wne 2794

wral 2912

wrex 2913

cvv 3200 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

wpss 3575

c0 3915

cpw 4158

csn 4177

cop 4183 class class class wbr 4653

cxp 5112

crn 5115

cres 5116

cima 5117

wf1 5885

wf1o 5887

cen 7952

cdom 7953

csdm 7954

cfn 7955

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-om 7066 df-1o 7560 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959

This theorem is referenced by: marypha1 8340

W3C validator