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

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.
StepHypRef Expression
1 cardon 8346 . . . . 5
21onsuci 6673 . . . 4
32a1i 11 . . 3
4 onelon 4908 . . 3
53, 4sylan 471 . 2
6 eleq1 2529 . . . . . 6
7 fveq2 5871 . . . . . . 7
87eleq1d 2526 . . . . . 6
96, 8imbi12d 320 . . . . 5
109imbi2d 316 . . . 4
11 eleq1 2529 . . . . . 6
12 fveq2 5871 . . . . . . 7
1312eleq1d 2526 . . . . . 6
1411, 13imbi12d 320 . . . . 5
1514imbi2d 316 . . . 4
16 r19.21v 2862 . . . . . 6
172onordi 4987 . . . . . . . . . . . . . . 15
1817a1i 11 . . . . . . . . . . . . . 14
19 ordelss 4899 . . . . . . . . . . . . . 14
2018, 19sylan 471 . . . . . . . . . . . . 13
2120sselda 3503 . . . . . . . . . . . 12
22 biimt 335 . . . . . . . . . . . 12
2321, 22syl 16 . . . . . . . . . . 11
2423ralbidva 2893 . . . . . . . . . 10
252onssi 6672 . . . . . . . . . . . . . 14
26 simprl 756 . . . . . . . . . . . . . 14
2725, 26sseldi 3501 . . . . . . . . . . . . 13
28 ttukeylem.1 . . . . . . . . . . . . . 14
29 ttukeylem.2 . . . . . . . . . . . . . 14
30 ttukeylem.3 . . . . . . . . . . . . . 14
31 ttukeylem.4 . . . . . . . . . . . . . 14
3228, 29, 30, 31ttukeylem3 8912 . . . . . . . . . . . . 13
3327, 32syldan 470 . . . . . . . . . . . 12
3429ad3antrrr 729 . . . . . . . . . . . . . 14
35 inss2 3718 . . . . . . . . . . . . . . . . . . . . 21
36 simpr 461 . . . . . . . . . . . . . . . . . . . . 21
3735, 36sseldi 3501 . . . . . . . . . . . . . . . . . . . 20
38 inss1 3717 . . . . . . . . . . . . . . . . . . . . . . . 24
3938, 36sseldi 3501 . . . . . . . . . . . . . . . . . . . . . . 23
4039elpwid 4022 . . . . . . . . . . . . . . . . . . . . . 22
4131tfr1 7085 . . . . . . . . . . . . . . . . . . . . . . 23
42 fnfun 5683 . . . . . . . . . . . . . . . . . . . . . . 23
43 funiunfv 6160 . . . . . . . . . . . . . . . . . . . . . . 23
4441, 42, 43mp2b 10 . . . . . . . . . . . . . . . . . . . . . 22
4540, 44syl6sseqr 3550 . . . . . . . . . . . . . . . . . . . . 21
46 dfss3 3493 . . . . . . . . . . . . . . . . . . . . . 22
47 eliun 4335 . . . . . . . . . . . . . . . . . . . . . . 23
4847ralbii 2888 . . . . . . . . . . . . . . . . . . . . . 22
4946, 48bitri 249 . . . . . . . . . . . . . . . . . . . . 21
5045, 49sylib 196 . . . . . . . . . . . . . . . . . . . 20
51 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . 22
5251eleq2d 2527 . . . . . . . . . . . . . . . . . . . . 21
5352ac6sfi 7784 . . . . . . . . . . . . . . . . . . . 20
5437, 50, 53syl2anc 661 . . . . . . . . . . . . . . . . . . 19
55 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . 22
56 simp-4l 767 . . . . . . . . . . . . . . . . . . . . . . 23
57 simprrl 765 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5857adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
59 frn 5742 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6058, 59syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
6127ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62 onss 6626 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6361, 62syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6460, 63sstrd 3513 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6537adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6665adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
67 ffn 5736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6858, 67syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
69 dffn4 5806 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7068, 69sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
71 fofi 7826 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7266, 70, 71syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26
73 dm0rn0 5224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
74 fdm 5740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7557, 74syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7675eqeq1d 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7773, 76syl5bbr 259 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7877necon3bid 2715 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7978biimpar 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26
80 ordunifi 7790 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8164, 72, 79, 80syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25
8260, 81sseldd 3504 . . . . . . . . . . . . . . . . . . . . . . . 24
83 simplrr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25
8483ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24
85 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8685eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . 25
8786rspcv 3206 . . . . . . . . . . . . . . . . . . . . . . . 24
8882, 84, 87sylc 60 . . . . . . . . . . . . . . . . . . . . . . 23
89 simp-4l 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9027ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9190, 62syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
92 ffvelrn 6029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9392adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9491, 93sseldd 3504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9559ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9695, 91sstrd 3513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
97 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9897rnex 6734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9998ssonunii 6623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
10096, 99syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
10167ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
102 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
103 fnfvelrn 6028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
104101, 102, 103syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105 elssuni 4279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
106104, 105syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
10728, 29, 30, 31ttukeylem5 8914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
10889, 94, 100, 106, 107syl13anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
109108sseld 3502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
110109anassrs 648 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
111110ralimdva 2865 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
112111expimpd 603 . . . . . . . . . . . . . . . . . . . . . . . . . 26
113112impr 619 . . . . . . . . . . . . . . . . . . . . . . . . 25
114113adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
115 dfss3 3493 . . . . . . . . . . . . . . . . . . . . . . . 24
116114, 115sylibr 212 . . . . . . . . . . . . . . . . . . . . . . 23
11728, 29, 30ttukeylem2 8911 . . . . . . . . . . . . . . . . . . . . . . 23
11856, 88, 116, 117syl12anc 1226 . . . . . . . . . . . . . . . . . . . . . 22
119 0ss 3814 . . . . . . . . . . . . . . . . . . . . . . . . 25
12028, 29, 30ttukeylem2 8911 . . . . . . . . . . . . . . . . . . . . . . . . 25
121119, 120mpanr2 684 . . . . . . . . . . . . . . . . . . . . . . . 24
12229, 121mpdan 668 . . . . . . . . . . . . . . . . . . . . . . 23
123122ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22
12455, 118, 123pm2.61ne 2772 . . . . . . . . . . . . . . . . . . . . 21
125124expr 615 . . . . . . . . . . . . . . . . . . . 20
126125exlimdv 1724 . . . . . . . . . . . . . . . . . . 19
12754, 126mpd 15 . . . . . . . . . . . . . . . . . 18
128127ex 434 . . . . . . . . . . . . . . . . 17
129128ssrdv 3509 . . . . . . . . . . . . . . . 16
13028, 29, 30ttukeylem1 8910 . . . . . . . . . . . . . . . . 17
131130ad2antrr 725 . . . . . . . . . . . . . . . 16