marypha1lem - Metamath Proof Explorer

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

Theorem marypha1lem 7186

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 4703	. . . . 5
2	1	pweqd 3630	. . . 4
3		pweq 3628	. . . . . 6
4	3	raleqdv 2742	. . . . 5
5		f1eq2 5433	. . . . . 6
6	5	rexbidv 2564	. . . . 5
7	4, 6	imbi12d 311	. . . 4
8	2, 7	raleqbidv 2748	. . 3
9	8	imbi2d 307	. 2
10		xpeq1 4703	. . . . 5
11	10	pweqd 3630	. . . 4
12		pweq 3628	. . . . . 6
13	12	raleqdv 2742	. . . . 5
14		f1eq2 5433	. . . . . 6
15	14	rexbidv 2564	. . . . 5
16	13, 15	imbi12d 311	. . . 4
17	11, 16	raleqbidv 2748	. . 3
18	17	imbi2d 307	. 2
19		bi2.04 350	. . . . 5
20	19	albii 1553	. . . 4
21		19.21v 1831	. . . 4
22	20, 21	bitri 240	. . 3
23		0elpw 4180	. . . . . . . . . . . . 13
24		f10 5507	. . . . . . . . . . . . 13
25		f1eq1 5432	. . . . . . . . . . . . . 14
26	25	rspcev 2884	. . . . . . . . . . . . 13 $/\$
27	23, 24, 26	mp2an 653	. . . . . . . . . . . 12
28		f1eq2 5433	. . . . . . . . . . . . 13
29	28	rexbidv 2564	. . . . . . . . . . . 12
30	27, 29	mpbiri 224	. . . . . . . . . . 11
31	30	a1i 10	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		n0 3464	. . . . . . . . . . 11
33		snelpwi 4220	. . . . . . . . . . . . . . . . . . 19
34		id 19	. . . . . . . . . . . . . . . . . . . . . . 23
35		imaeq2 5008	. . . . . . . . . . . . . . . . . . . . . . 23
36	34, 35	breq12d 4036	. . . . . . . . . . . . . . . . . . . . . 22
37	36	rspcva 2882	. . . . . . . . . . . . . . . . . . . . 21 $/\$
38		vex 2791	. . . . . . . . . . . . . . . . . . . . . . . . 25
39	38	snnz 3744	. . . . . . . . . . . . . . . . . . . . . . . 24
40		snex 4216	. . . . . . . . . . . . . . . . . . . . . . . . 25
41	40	0sdom 6992	. . . . . . . . . . . . . . . . . . . . . . . 24
42	39, 41	mpbir 200	. . . . . . . . . . . . . . . . . . . . . . 23
43		sdomdomtr 6994	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
44	42, 43	mpan 651	. . . . . . . . . . . . . . . . . . . . . 22
45		vex 2791	. . . . . . . . . . . . . . . . . . . . . . . 24
46		imaexg 5026	. . . . . . . . . . . . . . . . . . . . . . . 24
47	45, 46	ax-mp 8	. . . . . . . . . . . . . . . . . . . . . . 23
48	47	0sdom 6992	. . . . . . . . . . . . . . . . . . . . . 22
49	44, 48	sylib 188	. . . . . . . . . . . . . . . . . . . . 21
50	37, 49	syl 15	. . . . . . . . . . . . . . . . . . . 20 $/\$
51	50	expcom 424	. . . . . . . . . . . . . . . . . . 19
52	33, 51	syl5 28	. . . . . . . . . . . . . . . . . 18
53	52	adantl 452	. . . . . . . . . . . . . . . . 17 $/\$
54	53	ad2antlr 707	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	54	impr 602	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		n0 3464	. . . . . . . . . . . . . . 15
57	55, 56	sylib 188	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		imaexg 5026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59		difexg 4162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
60	45, 58, 59	mp2b 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
61	60	0dom 6991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
62		breq1 4026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
63	61, 62	mpbiri 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
64	63	a1i 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$
65		simpll 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
66		elpwi 3633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$
67	66	ad2antrl 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $\$ $/\$ $\$
68		disjsn 3693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
69		disj4 3503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $\$
70	68, 69	bitr3i 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $\$
71	70	con4bii 288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$
72	71	biimpi 186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$
73	72	ad2antlr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $\$ $/\$ $\$
74		sspsstr 3281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $/\$ $\$
75	67, 73, 74	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $\$ $/\$
76		simprr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $\$ $/\$
77	75, 76	jca 518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
78		psseq1 3263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
79		neeq1 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
80	78, 79	anbi12d 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
81		id 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
82		imaeq2 5008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
83	81, 82	breq12d 4036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
84	80, 83	imbi12d 311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
85	84	spv 1938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
86	65, 77, 85	sylc 56	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $\$ $/\$
87		domdifsn 6945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
88	86, 87	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $/\$ $\$
89	88	expr 598	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$
90	64, 89	pm2.61dne 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$
91	90	adantlrr 701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $\$ $\$
92	91	adantll 694	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
93		df-ss 3166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
94	66, 93	sylib 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
95	94	imaeq2d 5012	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
96	95	ineq1d 3369	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$ $\$ $\$
97	96	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
98		indif2 3412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
99		imassrn 5025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
100		elpwi 3633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
101		rnss 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
102		rnxpss 5108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
103	101, 102	syl6ss 3191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
104	100, 103	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105	99, 104	syl5ss 3190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106		df-ss 3166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
107	105, 106	sylib 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
108	107	difeq1d 3293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
109	108	ad2antrl 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$
110	98, 109	syl5eq 2327	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$
111	110	ad2antrr 706	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
112	97, 111	eqtrd 2315	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
113	92, 112	breqtrrd 4049	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
114	113	ralrimiva 2626	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
115		id 19	. . . . . . . . . . . . . . . . . . . . . . . . 25
116		imainrect 5119	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $\$ $\$
117		imaeq2 5008	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $\$ $\$
118	116, 117	syl5eqr 2329	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
119	115, 118	breq12d 4036	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$
120	119	cbvralv 2764	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$ $\$ $\$
121	114, 120	sylib 188	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
122	121	adantllr 699	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
123		inss2 3390	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$
124		difss 3303	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
125		xpss2 4796	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
126	124, 125	ax-mp 8	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$
127	123, 126	sstri 3188	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$
128	45	inex1 4155	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
129	128	elpw 3631	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$ $\$ $\$
130	127, 129	mpbir 200	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$
131		simpllr 735	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	72	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$
133	132	ad2antll 709	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
134		vex 2791	. . . . . . . . . . . . . . . . . . . . . . . . 25
135		difexg 4162	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
136	134, 135	ax-mp 8	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
137		psseq1 3263	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
138		xpeq1 4703	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
139	138	pweqd 3630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
140		pweq 3628	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
141	140	raleqdv 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
142		f1eq2 5433	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
143	142	rexbidv 2564	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
144	141, 143	imbi12d 311	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $\$
145	139, 144	raleqbidv 2748	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
146	137, 145	imbi12d 311	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$ $\$
147	136, 146	spcv 2874	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$
148	131, 133, 147	sylc 56	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
149		imaeq1 5007	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $\$ $\$
150	149	breq2d 4035	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
151	150	ralbidv 2563	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$ $\$ $\$
152		pweq 3628	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
153	152	rexeqdv 2743	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$ $\$ $\$
154	151, 153	imbi12d 311	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
155	154	rspcva 2882	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
156	130, 148, 155	sylancr 644	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
157	122, 156	mpd 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
158		f1eq1 5432	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
159	158	cbvrexv 2765	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $\$ $\$ $\$
160	157, 159	sylib 188	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
161		vex 2791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
162	38, 161	elimasn 5038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
163	162	biimpi 186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
164	163	snssd 3760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
165	164	ad2antlr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $\$
166		elpwi 3633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$ $\$ $\$
167		inss1 3389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
168	166, 167	syl6ss 3191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
169	168	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $\$
170	165, 169	unssd 3351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $\$
171	45	elpw2 4175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
172	170, 171	sylibr 203	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $\$
173	172	ad2ant2lr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
174	38, 161	f1osn 5513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
175	174	a1i 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $/\$ $\$
176		f1f1orn 5483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
177	176	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $/\$ $\$ $\$
178		disjdif 3526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
179	178	a1i 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $/\$ $\$ $\$
180		incom 3361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
181	166, 123	syl6ss 3191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$ $\$ $\$ $\$
182		rnss 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $\$ $\$ $\$ $\$
183		rnxpss 5108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $\$ $\$ $\$
184	182, 183	syl6ss 3191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$ $\$ $\$
185	181, 184	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$ $\$
186		incom 3361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$ $\$
187		disjdif 3526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$
188	186, 187	eqtri 2303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$
189		ssdisj 3504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $/\$ $\$
190	185, 188, 189	sylancl 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$
191	180, 190	syl5eq 2327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
192	191	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $/\$ $\$
193		f1oun 5492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $\$ $/\$ $\$ $/\$ $\$
194	175, 177, 179, 192, 193	syl22anc 1183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$ $/\$ $\$ $\$
195	194	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
196		snssi 3759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
197	196	ad2antrl 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
198		undif 3534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
199	197, 198	sylib 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
200		f1oeq2 5464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
201	199, 200	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$
202	201	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
203	195, 202	mpbid 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
204		f1of1 5471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
205		ssv 3198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
206		f1ss 5442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
207	204, 205, 206	sylancl 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
208	203, 207	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
209		f1eq1 5432	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
210	209	rspcev 2884	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
211	173, 208, 210	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
212	211	exp32 588	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $\$ $\$
213	212	rexlimdv 2666	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $\$ $\$
214	213	ex 423	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $\$ $\$
215	214	adantr 451	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
216	215	ad2antlr 707	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
217	216	impr 602	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
218	217	adantllr 699	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
219	160, 218	mpd 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
220	219	expr 598	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
221	220	exp3a 425	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
222	221	impr 602	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
223	222	exlimdv 1664	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
224	57, 223	mpd 14	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
225	224	expr 598	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
226	225	exlimdv 1664	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
227	32, 226	syl5bi 208	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
228	31, 227	pm2.61dne 2523	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
229		exanali 1572	. . . . . . . . . 10 $/\$ $/\$ $/\$
230		simprll 738	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
231		pssss 3271	. . . . . . . . . . . . . . . . . . . 20
232	230, 231	syl 15	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
233		sspwb 4223	. . . . . . . . . . . . . . . . . . 19
234	232, 233	sylib 188	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
235		simplrr 737	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
236		ssralv 3237	. . . . . . . . . . . . . . . . . 18
237	234, 235, 236	sylc 56	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
238		elpwi 3633	. . . . . . . . . . . . . . . . . . . . 21
239		resima2 4988	. . . . . . . . . . . . . . . . . . . . 21
240	238, 239	syl 15	. . . . . . . . . . . . . . . . . . . 20
241	240	eqcomd 2288	. . . . . . . . . . . . . . . . . . 19
242	241	breq2d 4035	. . . . . . . . . . . . . . . . . 18
243	242	ralbiia 2575	. . . . . . . . . . . . . . . . 17
244	237, 243	sylib 188	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245		simplrl 736	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
246		ssres 4981	. . . . . . . . . . . . . . . . . . . . 21
247		df-res 4701	. . . . . . . . . . . . . . . . . . . . . 22
248		inxp 4818	. . . . . . . . . . . . . . . . . . . . . . 23
249		inss2 3390	. . . . . . . . . . . . . . . . . . . . . . . 24
250		inss1 3389	. . . . . . . . . . . . . . . . . . . . . . . 24
251		xpss12 4792	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
252	249, 250, 251	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . 23
253	248, 252	eqsstri 3208	. . . . . . . . . . . . . . . . . . . . . 22
254	247, 253	eqsstri 3208	. . . . . . . . . . . . . . . . . . . . 21
255	246, 254	syl6ss 3191	. . . . . . . . . . . . . . . . . . . 20
256	100, 255	syl 15	. . . . . . . . . . . . . . . . . . 19
257	45	resex 4995	. . . . . . . . . . . . . . . . . . . 20
258	257	elpw 3631	. . . . . . . . . . . . . . . . . . 19
259	256, 258	sylibr 203	. . . . . . . . . . . . . . . . . 18
260	245, 259	syl 15	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
261		simpllr 735	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
262		psseq1 3263	. . . . . . . . . . . . . . . . . . . 20
263		xpeq1 4703	. . . . . . . . . . . . . . . . . . . . . 22
264	263	pweqd 3630	. . . . . . . . . . . . . . . . . . . . 21
265		pweq 3628	. . . . . . . . . . . . . . . . . . . . . . 23
266	265	raleqdv 2742	. . . . . . . . . . . . . . . . . . . . . 22
267		f1eq2 5433	. . . . . . . . . . . . . . . . . . . . . . 23
268	267	rexbidv 2564	. . . . . . . . . . . . . . . . . . . . . 22
269	266, 268	imbi12d 311	. . . . . . . . . . . . . . . . . . . . 21
270	264, 269	raleqbidv 2748	. . . . . . . . . . . . . . . . . . . 20
271	262, 270	imbi12d 311	. . . . . . . . . . . . . . . . . . 19
272	271	spv 1938	. . . . . . . . . . . . . . . . . 18
273	261, 230, 272	sylc 56	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
274		imaeq1 5007	. . . . . . . . . . . . . . . . . . . . 21
275	274	breq2d 4035	. . . . . . . . . . . . . . . . . . . 20
276	275	ralbidv 2563	. . . . . . . . . . . . . . . . . . 19
277		pweq 3628	. . . . . . . . . . . . . . . . . . . 20
278	277	rexeqdv 2743	. . . . . . . . . . . . . . . . . . 19
279	276, 278	imbi12d 311	. . . . . . . . . . . . . . . . . 18
280	279	rspcva 2882	. . . . . . . . . . . . . . . . 17 $/\$
281	260, 273, 280	syl2anc 642	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
282	244, 281	mpd 14	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
283		f1eq1 5432	. . . . . . . . . . . . . . . 16
284	283	cbvrexv 2765	. . . . . . . . . . . . . . 15
285	282, 284	sylib 188	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
286	231	ad2antrr 706	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
287	286	ad2antlr 707	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
288		elpwi 3633	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
289		difss 3303	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
290	288, 289	syl6ss 3191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
291	290	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
292	287, 291	unssd 3351	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
293	134	elpw2 4175	. . . . . . . . . . . . . . . . . . . . . . . . 25
294	292, 293	sylibr 203	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
295		simprr 733	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
296	295	ad2antrr 706	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$