Theorem fpwwe2lem12 9040

Description: Lemma for fpwwe2 9042. (Contributed by Mario Carneiro, 18-May-2015.)

Hypotheses

Ref	Expression
fpwwe2.1
fpwwe2.2
fpwwe2.3
fpwwe2.4

Assertion

Ref	Expression
fpwwe2lem12

Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,   ,,,,

Proof of Theorem fpwwe2lem12

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fpwwe2.4	. . . . 5
2		vex 3112	. . . . . . . . 9
3	2	eldm 5205	. . . . . . . 8
4		fpwwe2.1	. . . . . . . . . . . . . 14
5		fpwwe2.2	. . . . . . . . . . . . . 14
6	4, 5	fpwwe2lem2 9031	. . . . . . . . . . . . 13
7	6	simprbda 623	. . . . . . . . . . . 12
8	7	simpld 459	. . . . . . . . . . 11
9		selpw 4019	. . . . . . . . . . 11
10	8, 9	sylibr 212	. . . . . . . . . 10
11	10	ex 434	. . . . . . . . 9
12	11	exlimdv 1724	. . . . . . . 8
13	3, 12	syl5bi 217	. . . . . . 7
14	13	ssrdv 3509	. . . . . 6
15		sspwuni 4416	. . . . . 6
16	14, 15	sylib 196	. . . . 5
17	1, 16	syl5eqss 3547	. . . 4
18		vex 3112	. . . . . . . 8
19	18	elrn 5248	. . . . . . 7
20	7	simprd 463	. . . . . . . . . . 11
21	4	relopabi 5133	. . . . . . . . . . . . . . . 16
22	21	releldmi 5244	. . . . . . . . . . . . . . 15
23	22	adantl 466	. . . . . . . . . . . . . 14
24		elssuni 4279	. . . . . . . . . . . . . 14
25	23, 24	syl 16	. . . . . . . . . . . . 13
26	25, 1	syl6sseqr 3550	. . . . . . . . . . . 12
27		xpss12 5113	. . . . . . . . . . . 12
28	26, 26, 27	syl2anc 661	. . . . . . . . . . 11
29	20, 28	sstrd 3513	. . . . . . . . . 10
30		selpw 4019	. . . . . . . . . 10
31	29, 30	sylibr 212	. . . . . . . . 9
32	31	ex 434	. . . . . . . 8
33	32	exlimdv 1724	. . . . . . 7
34	19, 33	syl5bi 217	. . . . . 6
35	34	ssrdv 3509	. . . . 5
36		sspwuni 4416	. . . . 5
37	35, 36	sylib 196	. . . 4
38	17, 37	jca 532	. . 3
39		n0 3794	. . . . . . . . 9
40		ssel2 3498	. . . . . . . . . . . . . 14
41	40	adantl 466	. . . . . . . . . . . . 13
42	1	eleq2i 2535	. . . . . . . . . . . . . 14
43		eluni2 4253	. . . . . . . . . . . . . 14
44	42, 43	bitri 249	. . . . . . . . . . . . 13
45	41, 44	sylib 196	. . . . . . . . . . . 12
46	2	inex2 4594	. . . . . . . . . . . . . . . . . . 19
47	46	a1i 11	. . . . . . . . . . . . . . . . . 18
48	6	simplbda 624	. . . . . . . . . . . . . . . . . . . . 21
49	48	simpld 459	. . . . . . . . . . . . . . . . . . . 20
50	49	ad2ant2r 746	. . . . . . . . . . . . . . . . . . 19
51		wefr 4874	. . . . . . . . . . . . . . . . . . 19
52	50, 51	syl 16	. . . . . . . . . . . . . . . . . 18
53		inss2 3718	. . . . . . . . . . . . . . . . . . 19
54	53	a1i 11	. . . . . . . . . . . . . . . . . 18
55		simplrr 762	. . . . . . . . . . . . . . . . . . 19
56		simprr 757	. . . . . . . . . . . . . . . . . . 19
57		inelcm 3881	. . . . . . . . . . . . . . . . . . 19
58	55, 56, 57	syl2anc 661	. . . . . . . . . . . . . . . . . 18
59		fri 4846	. . . . . . . . . . . . . . . . . 18
60	47, 52, 54, 58, 59	syl22anc 1229	. . . . . . . . . . . . . . . . 17
61		inss1 3717	. . . . . . . . . . . . . . . . . . . . 21
62		simprl 756	. . . . . . . . . . . . . . . . . . . . 21
63	61, 62	sseldi 3501	. . . . . . . . . . . . . . . . . . . 20
64		simplrr 762	. . . . . . . . . . . . . . . . . . . . . . 23
65		ralnex 2903	. . . . . . . . . . . . . . . . . . . . . . 23
66	64, 65	sylib 196	. . . . . . . . . . . . . . . . . . . . . 22
67		df-br 4453	. . . . . . . . . . . . . . . . . . . . . . . 24
68		eluni2 4253	. . . . . . . . . . . . . . . . . . . . . . . 24
69	67, 68	bitri 249	. . . . . . . . . . . . . . . . . . . . . . 23
70		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . . . 26
71	70	elrn 5248	. . . . . . . . . . . . . . . . . . . . . . . . 25
72		df-br 4453	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
73		simprll 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
74	73	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
75		simprr 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
76		simp-4l 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
77		simprl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
78	77	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
79		simprlr 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
80		simprr 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
81	4, 5	fpwwe2lem2 9031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
82	81	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
83	80, 82	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
84	83	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
85	84	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
86	76, 78, 79, 85	syl12anc 1226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
87	86	ssbrd 4493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
88	75, 87	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
89		brxp 5035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
90	89	simplbi 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
91	88, 90	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
92	91	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
93	53, 62	sseldi 3501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
94	93	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
95		simplrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96		brinxp2 5066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97	92, 94, 95, 96	syl3anbrc 1180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98		simprr 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
99	98	breqd 4463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
100	97, 99	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
101	76, 78, 20	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
102	101	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
103	102	ssbrd 4493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
104	100, 103	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
105		brxp 5035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
106	105	simplbi 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
107	104, 106	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
108	74, 107	elind 3687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109		breq1 4455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110	109	rspcev 3210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111	108, 100, 110	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112	73	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
113		simprl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
114	91	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
115	113, 114	sseldd 3504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
116	112, 115	elind 3687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
117		simplrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
118		simprr 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
119		inss1 3717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
120	118, 119	syl6eqss 3553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
121	120	ssbrd 4493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
122	117, 121	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
123	116, 122, 110	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
124	5	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125		fpwwe2.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
126	125	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
127		simprl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
128	4, 124, 126, 127, 80	fpwwe2lem10 9038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
129	76, 78, 79, 128	syl12anc 1226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
130	111, 123, 129	mpjaodan 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
131	130	expr 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
132	72, 131	syl5bir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
133	132	expr 615	. . . . . . . . . . . . . . . . . . . . . . . . . 26
134	133	exlimdv 1724	. . . . . . . . . . . . . . . . . . . . . . . . 25
135	71, 134	syl5bi 217	. . . . . . . . . . . . . . . . . . . . . . . 24
136	135	rexlimdv 2947	. . . . . . . . . . . . . . . . . . . . . . 23
137	69, 136	syl5bi 217	. . . . . . . . . . . . . . . . . . . . . 22
138	66, 137	mtod 177	. . . . . . . . . . . . . . . . . . . . 21
139	138	ralrimiva 2871	. . . . . . . . . . . . . . . . . . . 20
140	63, 139	jca 532	. . . . . . . . . . . . . . . . . . 19
141	140	ex 434	. . . . . . . . . . . . . . . . . 18
142	141	reximdv2 2928	. . . . . . . . . . . . . . . . 17
143	60, 142	mpd 15	. . . . . . . . . . . . . . . 16
144	143	exp32 605	. . . . . . . . . . . . . . 15
145	144	exlimdv 1724	. . . . . . . . . . . . . 14
146	3, 145	syl5bi 217	. . . . . . . . . . . . 13
147	146	rexlimdv 2947	. . . . . . . . . . . 12
148	45, 147	mpd 15	. . . . . . . . . . 11
149	148	expr 615	. . . . . . . . . 10
150	149	exlimdv 1724	. . . . . . . . 9
151	39, 150	syl5bi 217	. . . . . . . 8
152	151	expimpd 603	. . . . . . 7
153	152	alrimiv 1719	. . . . . 6
154		df-fr 4843	. . . . . 6