Description: Lemma for ttukey . The G function forms a (transfinitely long) chain of inclusions. (Contributed by Mario Carneiro, 15-May-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ttukeylem.1 | |
|
ttukeylem.2 | |
||
ttukeylem.3 | |
||
ttukeylem.4 | |
||
Assertion | ttukeylem5 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ttukeylem.1 | |
|
2 | ttukeylem.2 | |
|
3 | ttukeylem.3 | |
|
4 | ttukeylem.4 | |
|
5 | sseq2 | |
|
6 | fveq2 | |
|
7 | 6 | sseq2d | |
8 | 5 7 | imbi12d | |
9 | 8 | imbi2d | |
10 | sseq2 | |
|
11 | fveq2 | |
|
12 | 11 | sseq2d | |
13 | 10 12 | imbi12d | |
14 | 13 | imbi2d | |
15 | r19.21v | |
|
16 | onsseleq | |
|
17 | 16 | ad4ant23 | |
18 | sseq2 | |
|
19 | sseq2 | |
|
20 | 4 | tfr1 | |
21 | simplr | |
|
22 | onss | |
|
23 | 21 22 | syl | |
24 | simprr | |
|
25 | fnfvima | |
|
26 | 20 23 24 25 | mp3an2i | |
27 | elssuni | |
|
28 | 26 27 | syl | |
29 | n0i | |
|
30 | iffalse | |
|
31 | 24 29 30 | 3syl | |
32 | 28 31 | sseqtrrd | |
33 | 32 | adantr | |
34 | 24 | adantr | |
35 | elssuni | |
|
36 | 34 35 | syl | |
37 | sseq2 | |
|
38 | fveq2 | |
|
39 | 38 | sseq2d | |
40 | 37 39 | imbi12d | |
41 | simplrl | |
|
42 | vuniex | |
|
43 | 42 | sucid | |
44 | eloni | |
|
45 | orduniorsuc | |
|
46 | 21 44 45 | 3syl | |
47 | 46 | orcanai | |
48 | 43 47 | eleqtrrid | |
49 | 40 41 48 | rspcdva | |
50 | 36 49 | mpd | |
51 | ssun1 | |
|
52 | 50 51 | sstrdi | |
53 | 18 19 33 52 | ifbothda | |
54 | 1 2 3 4 | ttukeylem3 | |
55 | 54 | ad4ant13 | |
56 | 53 55 | sseqtrrd | |
57 | 56 | expr | |
58 | fveq2 | |
|
59 | eqimss | |
|
60 | 58 59 | syl | |
61 | 60 | a1i | |
62 | 57 61 | jaod | |
63 | 17 62 | sylbid | |
64 | 63 | ex | |
65 | 64 | expcom | |
66 | 65 | a2d | |
67 | 15 66 | syl5bi | |
68 | 9 14 67 | tfis3 | |
69 | 68 | expdcom | |
70 | 69 | 3imp2 | |