Theorem ttukeylem6 8915

Description: Lemma for ttukey 8919. (Contributed by Mario Carneiro, 15-May-2015.)

Hypotheses

Ref	Expression
ttukeylem.1
ttukeylem.2
ttukeylem.3
ttukeylem.4

Assertion

Ref	Expression
ttukeylem6

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

Proof of Theorem ttukeylem6

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

Step	Hyp	Ref	Expression
1		cardon 8346	. . . . 5
2	1	onsuci 6673	. . . 4
3	2	a1i 11	. . 3
4		onelon 4908	. . 3
5	3, 4	sylan 471	. 2
6		eleq1 2529	. . . . . 6
7		fveq2 5871	. . . . . . 7
8	7	eleq1d 2526	. . . . . 6
9	6, 8	imbi12d 320	. . . . 5
10	9	imbi2d 316	. . . 4
11		eleq1 2529	. . . . . 6
12		fveq2 5871	. . . . . . 7
13	12	eleq1d 2526	. . . . . 6
14	11, 13	imbi12d 320	. . . . 5
15	14	imbi2d 316	. . . 4
16		r19.21v 2862	. . . . . 6
17	2	onordi 4987	. . . . . . . . . . . . . . 15
18	17	a1i 11	. . . . . . . . . . . . . 14
19		ordelss 4899	. . . . . . . . . . . . . 14
20	18, 19	sylan 471	. . . . . . . . . . . . 13
21	20	sselda 3503	. . . . . . . . . . . 12
22		biimt 335	. . . . . . . . . . . 12
23	21, 22	syl 16	. . . . . . . . . . 11
24	23	ralbidva 2893	. . . . . . . . . 10
25	2	onssi 6672	. . . . . . . . . . . . . 14
26		simprl 756	. . . . . . . . . . . . . 14
27	25, 26	sseldi 3501	. . . . . . . . . . . . 13
28		ttukeylem.1	. . . . . . . . . . . . . 14
29		ttukeylem.2	. . . . . . . . . . . . . 14
30		ttukeylem.3	. . . . . . . . . . . . . 14
31		ttukeylem.4	. . . . . . . . . . . . . 14
32	28, 29, 30, 31	ttukeylem3 8912	. . . . . . . . . . . . 13
33	27, 32	syldan 470	. . . . . . . . . . . 12
34	29	ad3antrrr 729	. . . . . . . . . . . . . 14
35		inss2 3718	. . . . . . . . . . . . . . . . . . . . 21
36		simpr 461	. . . . . . . . . . . . . . . . . . . . 21
37	35, 36	sseldi 3501	. . . . . . . . . . . . . . . . . . . 20
38		inss1 3717	. . . . . . . . . . . . . . . . . . . . . . . 24
39	38, 36	sseldi 3501	. . . . . . . . . . . . . . . . . . . . . . 23
40	39	elpwid 4022	. . . . . . . . . . . . . . . . . . . . . 22
41	31	tfr1 7085	. . . . . . . . . . . . . . . . . . . . . . 23
42		fnfun 5683	. . . . . . . . . . . . . . . . . . . . . . 23
43		funiunfv 6160	. . . . . . . . . . . . . . . . . . . . . . 23
44	41, 42, 43	mp2b 10	. . . . . . . . . . . . . . . . . . . . . 22
45	40, 44	syl6sseqr 3550	. . . . . . . . . . . . . . . . . . . . 21
46		dfss3 3493	. . . . . . . . . . . . . . . . . . . . . 22
47		eliun 4335	. . . . . . . . . . . . . . . . . . . . . . 23
48	47	ralbii 2888	. . . . . . . . . . . . . . . . . . . . . 22
49	46, 48	bitri 249	. . . . . . . . . . . . . . . . . . . . 21
50	45, 49	sylib 196	. . . . . . . . . . . . . . . . . . . 20
51		fveq2 5871	. . . . . . . . . . . . . . . . . . . . . 22
52	51	eleq2d 2527	. . . . . . . . . . . . . . . . . . . . 21
53	52	ac6sfi 7784	. . . . . . . . . . . . . . . . . . . 20
54	37, 50, 53	syl2anc 661	. . . . . . . . . . . . . . . . . . 19
55		eleq1 2529	. . . . . . . . . . . . . . . . . . . . . 22
56		simp-4l 767	. . . . . . . . . . . . . . . . . . . . . . 23
57		simprrl 765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
58	57	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26
59		frn 5742	. . . . . . . . . . . . . . . . . . . . . . . . . 26
60	58, 59	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25
61	27	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62		onss 6626	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
63	61, 62	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
64	60, 63	sstrd 3513	. . . . . . . . . . . . . . . . . . . . . . . . . 26
65	37	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
66	65	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
67		ffn 5736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
68	58, 67	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
69		dffn4 5806	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
70	68, 69	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
71		fofi 7826	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
72	66, 70, 71	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . 26
73		dm0rn0 5224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
74		fdm 5740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
75	57, 74	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
76	75	eqeq1d 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77	73, 76	syl5bbr 259	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
78	77	necon3bid 2715	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
79	78	biimpar 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26
80		ordunifi 7790	. . . . . . . . . . . . . . . . . . . . . . . . . 26
81	64, 72, 79, 80	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . 25
82	60, 81	sseldd 3504	. . . . . . . . . . . . . . . . . . . . . . . 24
83		simplrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25
84	83	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24
85		fveq2 5871	. . . . . . . . . . . . . . . . . . . . . . . . . 26
86	85	eleq1d 2526	. . . . . . . . . . . . . . . . . . . . . . . . 25
87	86	rspcv 3206	. . . . . . . . . . . . . . . . . . . . . . . 24
88	82, 84, 87	sylc 60	. . . . . . . . . . . . . . . . . . . . . . 23
89		simp-4l 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
90	27	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
91	90, 62	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
92		ffvelrn 6029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
93	92	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
94	91, 93	sseldd 3504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
95	59	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
96	95, 91	sstrd 3513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
97		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
98	97	rnex 6734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
99	98	ssonunii 6623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
100	96, 99	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
101	67	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
102		simprr 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
103		fnfvelrn 6028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
104	101, 102, 103	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105		elssuni 4279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
106	104, 105	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
107	28, 29, 30, 31	ttukeylem5 8914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
108	89, 94, 100, 106, 107	syl13anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
109	108	sseld 3502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
110	109	anassrs 648	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
111	110	ralimdva 2865	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
112	111	expimpd 603	. . . . . . . . . . . . . . . . . . . . . . . . . 26
113	112	impr 619	. . . . . . . . . . . . . . . . . . . . . . . . 25
114	113	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24
115		dfss3 3493	. . . . . . . . . . . . . . . . . . . . . . . 24
116	114, 115	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . 23
117	28, 29, 30	ttukeylem2 8911	. . . . . . . . . . . . . . . . . . . . . . 23
118	56, 88, 116, 117	syl12anc 1226	. . . . . . . . . . . . . . . . . . . . . 22
119		0ss 3814	. . . . . . . . . . . . . . . . . . . . . . . . 25
120	28, 29, 30	ttukeylem2 8911	. . . . . . . . . . . . . . . . . . . . . . . . 25
121	119, 120	mpanr2 684	. . . . . . . . . . . . . . . . . . . . . . . 24
122	29, 121	mpdan 668	. . . . . . . . . . . . . . . . . . . . . . 23
123	122	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . 22
124	55, 118, 123	pm2.61ne 2772	. . . . . . . . . . . . . . . . . . . . 21
125	124	expr 615	. . . . . . . . . . . . . . . . . . . 20
126	125	exlimdv 1724	. . . . . . . . . . . . . . . . . . 19
127	54, 126	mpd 15	. . . . . . . . . . . . . . . . . 18
128	127	ex 434	. . . . . . . . . . . . . . . . 17
129	128	ssrdv 3509	. . . . . . . . . . . . . . . 16
130	28, 29, 30	ttukeylem1 8910	. . . . . . . . . . . . . . . . 17
131	130	ad2antrr 725	. . . . . . . . . . . . . . . 16