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 7944

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 4847	. . . . 5
2	1	pweqd 3955	. . . 4
3		pweq 3953	. . . . . 6
4	3	raleqdv 2992	. . . . 5
5		f1eq2 5773	. . . . . 6
6	5	rexbidv 2900	. . . . 5
7	4, 6	imbi12d 322	. . . 4
8	2, 7	raleqbidv 3000	. . 3
9	8	imbi2d 318	. 2
10		xpeq1 4847	. . . . 5
11	10	pweqd 3955	. . . 4
12		pweq 3953	. . . . . 6
13	12	raleqdv 2992	. . . . 5
14		f1eq2 5773	. . . . . 6
15	14	rexbidv 2900	. . . . 5
16	13, 15	imbi12d 322	. . . 4
17	11, 16	raleqbidv 3000	. . 3
18	17	imbi2d 318	. 2
19		bi2.04 363	. . . . 5
20	19	albii 1690	. . . 4
21		19.21v 1785	. . . 4
22	20, 21	bitri 253	. . 3
23		0elpw 4571	. . . . . . . . . . . . 13
24		f10 5843	. . . . . . . . . . . . 13
25		f1eq1 5772	. . . . . . . . . . . . . 14
26	25	rspcev 3149	. . . . . . . . . . . . 13 $/\$
27	23, 24, 26	mp2an 677	. . . . . . . . . . . 12
28		f1eq2 5773	. . . . . . . . . . . . 13
29	28	rexbidv 2900	. . . . . . . . . . . 12
30	27, 29	mpbiri 237	. . . . . . . . . . 11
31	30	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		n0 3740	. . . . . . . . . . 11
33		snelpwi 4644	. . . . . . . . . . . . . . . . . . 19
34		id 22	. . . . . . . . . . . . . . . . . . . . . . 23
35		imaeq2 5163	. . . . . . . . . . . . . . . . . . . . . . 23
36	34, 35	breq12d 4414	. . . . . . . . . . . . . . . . . . . . . 22
37	36	rspcva 3147	. . . . . . . . . . . . . . . . . . . . 21 $/\$
38		vex 3047	. . . . . . . . . . . . . . . . . . . . . . . . 25
39	38	snnz 4089	. . . . . . . . . . . . . . . . . . . . . . . 24
40		snex 4640	. . . . . . . . . . . . . . . . . . . . . . . . 25
41	40	0sdom 7700	. . . . . . . . . . . . . . . . . . . . . . . 24
42	39, 41	mpbir 213	. . . . . . . . . . . . . . . . . . . . . . 23
43		sdomdomtr 7702	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
44	42, 43	mpan 675	. . . . . . . . . . . . . . . . . . . . . 22
45		vex 3047	. . . . . . . . . . . . . . . . . . . . . . . 24
46		imaexg 6727	. . . . . . . . . . . . . . . . . . . . . . . 24
47	45, 46	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23
48	47	0sdom 7700	. . . . . . . . . . . . . . . . . . . . . 22
49	44, 48	sylib 200	. . . . . . . . . . . . . . . . . . . . 21
50	37, 49	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
51	50	expcom 437	. . . . . . . . . . . . . . . . . . 19
52	33, 51	syl5 33	. . . . . . . . . . . . . . . . . 18
53	52	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
54	53	ad2antlr 732	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	54	impr 624	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		n0 3740	. . . . . . . . . . . . . . 15
57	55, 56	sylib 200	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		imaexg 6727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59		difexg 4550	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
60	45, 58, 59	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
61	60	0dom 7699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
62		breq1 4404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
63	61, 62	mpbiri 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$
65		simpll 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
66		elpwi 3959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$
67	66	ad2antrl 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $\$ $/\$ $\$
68		difsnpss 4114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$
69	68	biimpi 198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$
70	69	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $\$ $/\$ $\$
71	67, 70	sspsstrd 3540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $\$ $/\$
72		simprr 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $\$ $/\$
73	71, 72	jca 535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
74		psseq1 3519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
75		neeq1 2685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
76	74, 75	anbi12d 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
77		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
78		imaeq2 5163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
79	77, 78	breq12d 4414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
80	76, 79	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
81	80	spv 2103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
82	65, 73, 81	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $\$ $/\$
83		domdifsn 7652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
84	82, 83	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $/\$ $\$
85	84	expr 619	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$
86	64, 85	pm2.61dne 2709	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$
87	86	adantlrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $\$ $\$
88	87	adantll 719	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
89		df-ss 3417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
90	66, 89	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
91	90	imaeq2d 5167	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
92	91	ineq1d 3632	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$ $\$ $\$
93	92	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
94		indif2 3685	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
95		imassrn 5178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
96		elpwi 3959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
97		rnss 5062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
98		rnxpss 5268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99	97, 98	syl6ss 3443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
100	96, 99	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
101	95, 100	syl5ss 3442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
102		df-ss 3417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103	101, 102	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
104	103	difeq1d 3549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
105	104	ad2antrl 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$
106	94, 105	syl5eq 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$
107	106	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
108	93, 107	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
109	88, 108	breqtrrd 4428	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
110	109	ralrimiva 2801	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
111		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25
112		imainrect 5277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $\$ $\$
113		imaeq2 5163	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $\$ $\$
114	112, 113	syl5eqr 2498	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
115	111, 114	breq12d 4414	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$
116	115	cbvralv 3018	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$ $\$ $\$
117	110, 116	sylib 200	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
118	117	adantllr 724	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
119		inss2 3652	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$
120		difss 3559	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
121		xpss2 4943	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
122	120, 121	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$
123	119, 122	sstri 3440	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$
124	45	inex1 4543	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
125	124	elpw 3956	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$ $\$ $\$
126	123, 125	mpbir 213	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$
127		simpllr 768	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128	69	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$
129	128	ad2antll 734	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
130		vex 3047	. . . . . . . . . . . . . . . . . . . . . . . . 25
131		difexg 4550	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
132	130, 131	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
133		psseq1 3519	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
134		xpeq1 4847	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
135	134	pweqd 3955	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
136		pweq 3953	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
137	136	raleqdv 2992	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
138		f1eq2 5773	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
139	138	rexbidv 2900	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
140	137, 139	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $\$
141	135, 140	raleqbidv 3000	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
142	133, 141	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$ $\$
143	132, 142	spcv 3139	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$
144	127, 129, 143	sylc 62	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
145		imaeq1 5162	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $\$ $\$
146	145	breq2d 4413	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
147	146	ralbidv 2826	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$ $\$ $\$
148		pweq 3953	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $\$ $\$
149	148	rexeqdv 2993	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$ $\$ $\$
150	147, 149	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
151	150	rspcva 3147	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
152	126, 144, 151	sylancr 668	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
153	118, 152	mpd 15	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
154		f1eq1 5772	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
155	154	cbvrexv 3019	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $\$ $\$ $\$
156	153, 155	sylib 200	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
157		vex 3047	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
158	38, 157	elimasn 5192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
159	158	biimpi 198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
160	159	snssd 4116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
161	160	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $\$
162		elpwi 3959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $\$ $\$
163		inss1 3651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
164	162, 163	syl6ss 3443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
165	164	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $\$
166	161, 165	unssd 3609	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $\$
167	45	elpw2 4566	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
168	166, 167	sylibr 216	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$
169	168	ad2ant2lr 753	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
170	38, 157	f1osn 5850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
171	170	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$ $/\$ $\$
172		f1f1orn 5823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
173	172	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$ $/\$ $\$ $\$
174		disjdif 3838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
175	174	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$ $/\$ $\$ $\$
176		incom 3624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
177	162, 119	syl6ss 3443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$ $\$ $\$
178		rnss 5062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$ $\$ $\$ $\$
179		rnxpss 5268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$ $\$ $\$
180	178, 179	syl6ss 3443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$ $\$
181	177, 180	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$ $\$
182		incom 3624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$ $\$
183		disjdif 3838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $\$
184	182, 183	eqtri 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$
185		ssdisj 3813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $/\$ $\$
186	181, 184, 185	sylancl 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
187	176, 186	syl5eq 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
188	187	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$ $/\$ $\$
189		f1oun 5831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\$ $/\$ $\$ $/\$ $\$
190	171, 173, 175, 188, 189	syl22anc 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$ $/\$ $\$ $\$
191	190	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
192		snssi 4115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
193	192	ad2antrl 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
194		undif 3847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
195	193, 194	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$
196		f1oeq2 5804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
197	195, 196	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$
198	197	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
199	191, 198	mpbid 214	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
200		f1of1 5811	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
201		ssv 3451	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
202		f1ss 5782	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
203	200, 201, 202	sylancl 667	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
204	199, 203	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
205		f1eq1 5772	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
206	205	rspcev 3149	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
207	169, 204, 206	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$
208	207	rexlimdvaa 2879	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $\$ $\$
209	208	ex 436	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $\$ $\$
210	209	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
211	210	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
212	211	impr 624	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
213	212	adantllr 724	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
214	156, 213	mpd 15	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
215	214	expr 619	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
216	215	expd 438	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
217	216	impr 624	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
218	217	exlimdv 1778	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
219	57, 218	mpd 15	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
220	219	expr 619	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
221	220	exlimdv 1778	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
222	32, 221	syl5bi 221	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
223	31, 222	pm2.61dne 2709	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
224		exanali 1720	. . . . . . . . . 10 $/\$ $/\$ $/\$
225		simprll 771	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
226		pssss 3527	. . . . . . . . . . . . . . . . . . . 20
227	225, 226	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
228		sspwb 4648	. . . . . . . . . . . . . . . . . . 19
229	227, 228	sylib 200	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
230		simplrr 770	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
231		ssralv 3492	. . . . . . . . . . . . . . . . . 18
232	229, 230, 231	sylc 62	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
233		elpwi 3959	. . . . . . . . . . . . . . . . . . . . 21
234		resima2 5137	. . . . . . . . . . . . . . . . . . . . 21
235	233, 234	syl 17	. . . . . . . . . . . . . . . . . . . 20
236	235	eqcomd 2456	. . . . . . . . . . . . . . . . . . 19
237	236	breq2d 4413	. . . . . . . . . . . . . . . . . 18
238	237	ralbiia 2817	. . . . . . . . . . . . . . . . 17
239	232, 238	sylib 200	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
240		simplrl 769	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
241		ssres 5129	. . . . . . . . . . . . . . . . . . . . 21
242		df-res 4845	. . . . . . . . . . . . . . . . . . . . . 22
243		inxp 4966	. . . . . . . . . . . . . . . . . . . . . . 23
244		inss2 3652	. . . . . . . . . . . . . . . . . . . . . . . 24
245		inss1 3651	. . . . . . . . . . . . . . . . . . . . . . . 24
246		xpss12 4939	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
247	244, 245, 246	mp2an 677	. . . . . . . . . . . . . . . . . . . . . . 23
248	243, 247	eqsstri 3461	. . . . . . . . . . . . . . . . . . . . . 22
249	242, 248	eqsstri 3461	. . . . . . . . . . . . . . . . . . . . 21
250	241, 249	syl6ss 3443	. . . . . . . . . . . . . . . . . . . 20
251	96, 250	syl 17	. . . . . . . . . . . . . . . . . . 19
252	45	resex 5147	. . . . . . . . . . . . . . . . . . . 20
253	252	elpw 3956	. . . . . . . . . . . . . . . . . . 19
254	251, 253	sylibr 216	. . . . . . . . . . . . . . . . . 18
255	240, 254	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
256		simpllr 768	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
257		psseq1 3519	. . . . . . . . . . . . . . . . . . . 20
258		xpeq1 4847	. . . . . . . . . . . . . . . . . . . . . 22
259	258	pweqd 3955	. . . . . . . . . . . . . . . . . . . . 21
260		pweq 3953	. . . . . . . . . . . . . . . . . . . . . . 23
261	260	raleqdv 2992	. . . . . . . . . . . . . . . . . . . . . 22
262		f1eq2 5773	. . . . . . . . . . . . . . . . . . . . . . 23
263	262	rexbidv 2900	. . . . . . . . . . . . . . . . . . . . . 22
264	261, 263	imbi12d 322	. . . . . . . . . . . . . . . . . . . . 21
265	259, 264	raleqbidv 3000	. . . . . . . . . . . . . . . . . . . 20
266	257, 265	imbi12d 322	. . . . . . . . . . . . . . . . . . 19
267	266	spv 2103	. . . . . . . . . . . . . . . . . 18
268	256, 225, 267	sylc 62	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
269		imaeq1 5162	. . . . . . . . . . . . . . . . . . . . 21
270	269	breq2d 4413	. . . . . . . . . . . . . . . . . . . 20
271	270	ralbidv 2826	. . . . . . . . . . . . . . . . . . 19
272		pweq 3953	. . . . . . . . . . . . . . . . . . . 20
273	272	rexeqdv 2993	. . . . . . . . . . . . . . . . . . 19
274	271, 273	imbi12d 322	. . . . . . . . . . . . . . . . . 18
275	274	rspcva 3147	. . . . . . . . . . . . . . . . 17 $/\$
276	255, 268, 275	syl2anc 666	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
277	239, 276	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
278		f1eq1 5772	. . . . . . . . . . . . . . . 16
279	278	cbvrexv 3019	. . . . . . . . . . . . . . 15
280	277, 279	sylib 200	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
281	226	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
282	281	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
283		elpwi 3959	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
284		difss 3559	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
285	283, 284	syl6ss 3443	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
286	285	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
287	282, 286	unssd 3609	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
288	130	elpw2 4566	. . . . . . . . . . . . . . . . . . . . . . . . 25
289	287, 288	sylibr 216	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
290		simprr 765	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
291	290	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
292		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26
293		imaeq2 5163	. . . . . . . . . . . . . . . . . . . . . . . . . 26
294	292, 293	breq12d 4414	. . . . . . . . . . . . . . . . . . . . . . . . 25
295	294	rspcva 3147	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
296	289, 291, 295	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
297		imaundi 5247	. . . . . . . . . . . . . . . . . . . . . . . 24
298		undif2 3842	. . . . . . . . . . . . . . . . . . . . . . . 24