Theorem marypha1lem 7913

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 5018	. . . . 5
2	1	pweqd 4017	. . . 4
3		pweq 4015	. . . . . 6
4	3	raleqdv 3060	. . . . 5
5		f1eq2 5782	. . . . . 6
6	5	rexbidv 2968	. . . . 5
7	4, 6	imbi12d 320	. . . 4
8	2, 7	raleqbidv 3068	. . 3
9	8	imbi2d 316	. 2
10		xpeq1 5018	. . . . 5
11	10	pweqd 4017	. . . 4
12		pweq 4015	. . . . . 6
13	12	raleqdv 3060	. . . . 5
14		f1eq2 5782	. . . . . 6
15	14	rexbidv 2968	. . . . 5
16	13, 15	imbi12d 320	. . . 4
17	11, 16	raleqbidv 3068	. . 3
18	17	imbi2d 316	. 2
19		bi2.04 361	. . . . 5
20	19	albii 1640	. . . 4
21		19.21v 1729	. . . 4
22	20, 21	bitri 249	. . 3
23		0elpw 4621	. . . . . . . . . . . . 13
24		f10 5852	. . . . . . . . . . . . 13
25		f1eq1 5781	. . . . . . . . . . . . . 14
26	25	rspcev 3210	. . . . . . . . . . . . 13
27	23, 24, 26	mp2an 672	. . . . . . . . . . . 12
28		f1eq2 5782	. . . . . . . . . . . . 13
29	28	rexbidv 2968	. . . . . . . . . . . 12
30	27, 29	mpbiri 233	. . . . . . . . . . 11
31	30	a1i 11	. . . . . . . . . 10
32		n0 3794	. . . . . . . . . . 11
33		snelpwi 4697	. . . . . . . . . . . . . . . . . . 19
34		id 22	. . . . . . . . . . . . . . . . . . . . . . 23
35		imaeq2 5338	. . . . . . . . . . . . . . . . . . . . . . 23
36	34, 35	breq12d 4465	. . . . . . . . . . . . . . . . . . . . . 22
37	36	rspcva 3208	. . . . . . . . . . . . . . . . . . . . 21
38		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . . 25
39	38	snnz 4148	. . . . . . . . . . . . . . . . . . . . . . . 24
40		snex 4693	. . . . . . . . . . . . . . . . . . . . . . . . 25
41	40	0sdom 7668	. . . . . . . . . . . . . . . . . . . . . . . 24
42	39, 41	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . 23
43		sdomdomtr 7670	. . . . . . . . . . . . . . . . . . . . . . 23
44	42, 43	mpan 670	. . . . . . . . . . . . . . . . . . . . . 22
45		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . 24
46		imaexg 6737	. . . . . . . . . . . . . . . . . . . . . . . 24
47	45, 46	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23
48	47	0sdom 7668	. . . . . . . . . . . . . . . . . . . . . 22
49	44, 48	sylib 196	. . . . . . . . . . . . . . . . . . . . 21
50	37, 49	syl 16	. . . . . . . . . . . . . . . . . . . 20
51	50	expcom 435	. . . . . . . . . . . . . . . . . . 19
52	33, 51	syl5 32	. . . . . . . . . . . . . . . . . 18
53	52	adantl 466	. . . . . . . . . . . . . . . . 17
54	53	ad2antlr 726	. . . . . . . . . . . . . . . 16
55	54	impr 619	. . . . . . . . . . . . . . 15
56		n0 3794	. . . . . . . . . . . . . . 15
57	55, 56	sylib 196	. . . . . . . . . . . . . 14
58		imaexg 6737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
59		difexg 4600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
60	45, 58, 59	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
61	60	0dom 7667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
62		breq1 4455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
63	61, 62	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
65		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
66		elpwi 4021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
67	66	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
68		difsnpss 4173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
69	68	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
70	69	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
71	67, 70	sspsstrd 3611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
72		simprr 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	71, 72	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
74		psseq1 3590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
75		neeq1 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
76	74, 75	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
77		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
78		imaeq2 5338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
79	77, 78	breq12d 4465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
80	76, 79	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
81	80	spv 2011	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
82	65, 73, 81	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
83		domdifsn 7620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
84	82, 83	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
85	84	expr 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86	64, 85	pm2.61dne 2774	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
87	86	adantlrr 720	. . . . . . . . . . . . . . . . . . . . . . . . . 26
88	87	adantll 713	. . . . . . . . . . . . . . . . . . . . . . . . 25
89		df-ss 3489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
90	66, 89	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
91	90	imaeq2d 5342	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
92	91	ineq1d 3698	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
93	92	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26
94		indif2 3740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
95		imassrn 5353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
96		elpwi 4021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
97		rnss 5236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
98		rnxpss 5444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99	97, 98	syl6ss 3515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
100	96, 99	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
101	95, 100	syl5ss 3514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
102		df-ss 3489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103	101, 102	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
104	103	difeq1d 3620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
105	104	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	94, 105	syl5eq 2510	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	106	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	93, 107	eqtrd 2498	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	88, 108	breqtrrd 4478	. . . . . . . . . . . . . . . . . . . . . . . 24
110	109	ralrimiva 2871	. . . . . . . . . . . . . . . . . . . . . . 23
111		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25
112		imainrect 5453	. . . . . . . . . . . . . . . . . . . . . . . . . 26
113		imaeq2 5338	. . . . . . . . . . . . . . . . . . . . . . . . . 26
114	112, 113	syl5eqr 2512	. . . . . . . . . . . . . . . . . . . . . . . . 25
115	111, 114	breq12d 4465	. . . . . . . . . . . . . . . . . . . . . . . 24
116	115	cbvralv 3084	. . . . . . . . . . . . . . . . . . . . . . 23
117	110, 116	sylib 196	. . . . . . . . . . . . . . . . . . . . . 22
118	117	adantllr 718	. . . . . . . . . . . . . . . . . . . . 21
119		inss2 3718	. . . . . . . . . . . . . . . . . . . . . . . 24
120		difss 3630	. . . . . . . . . . . . . . . . . . . . . . . . 25
121		xpss2 5117	. . . . . . . . . . . . . . . . . . . . . . . . 25
122	120, 121	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24
123	119, 122	sstri 3512	. . . . . . . . . . . . . . . . . . . . . . 23
124	45	inex1 4593	. . . . . . . . . . . . . . . . . . . . . . . 24
125	124	elpw 4018	. . . . . . . . . . . . . . . . . . . . . . 23
126	123, 125	mpbir 209	. . . . . . . . . . . . . . . . . . . . . 22
127		simpllr 760	. . . . . . . . . . . . . . . . . . . . . . 23
128	69	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24
129	128	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . 23
130		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . . 25
131		difexg 4600	. . . . . . . . . . . . . . . . . . . . . . . . 25
132	130, 131	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24
133		psseq1 3590	. . . . . . . . . . . . . . . . . . . . . . . . 25
134		xpeq1 5018	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
135	134	pweqd 4017	. . . . . . . . . . . . . . . . . . . . . . . . . 26
136		pweq 4015	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
137	136	raleqdv 3060	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
138		f1eq2 5782	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
139	138	rexbidv 2968	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
140	137, 139	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . 26
141	135, 140	raleqbidv 3068	. . . . . . . . . . . . . . . . . . . . . . . . 25
142	133, 141	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . 24
143	132, 142	spcv 3200	. . . . . . . . . . . . . . . . . . . . . . 23
144	127, 129, 143	sylc 60	. . . . . . . . . . . . . . . . . . . . . 22
145		imaeq1 5337	. . . . . . . . . . . . . . . . . . . . . . . . . 26
146	145	breq2d 4464	. . . . . . . . . . . . . . . . . . . . . . . . 25
147	146	ralbidv 2896	. . . . . . . . . . . . . . . . . . . . . . . 24
148		pweq 4015	. . . . . . . . . . . . . . . . . . . . . . . . 25
149	148	rexeqdv 3061	. . . . . . . . . . . . . . . . . . . . . . . 24
150	147, 149	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . 23