Step | Hyp | Ref
| Expression |
1 | | neq0 3930 |
. . . . . . 7
|
2 | | indistop 20806 |
. . . . . . . . . . 11
|
3 | | indistop 20806 |
. . . . . . . . . . 11
|
4 | | eltx 21371 |
. . . . . . . . . . 11
|
5 | 2, 3, 4 | mp2an 708 |
. . . . . . . . . 10
|
6 | | rsp 2929 |
. . . . . . . . . 10
|
7 | 5, 6 | sylbi 207 |
. . . . . . . . 9
|
8 | | elssuni 4467 |
. . . . . . . . . . . . . 14
|
9 | | indisuni 20807 |
. . . . . . . . . . . . . . 15
|
10 | | indisuni 20807 |
. . . . . . . . . . . . . . 15
|
11 | 2, 3, 9, 10 | txunii 21396 |
. . . . . . . . . . . . . 14
|
12 | 8, 11 | syl6sseqr 3652 |
. . . . . . . . . . . . 13
|
13 | 12 | ad2antrr 762 |
. . . . . . . . . . . 12
|
14 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . . . 20
|
15 | 14 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . 19
|
16 | | xpnz 5553 |
. . . . . . . . . . . . . . . . . . 19
|
17 | 15, 16 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
|
18 | 17 | simpld 475 |
. . . . . . . . . . . . . . . . 17
|
19 | 18 | neneqd 2799 |
. . . . . . . . . . . . . . . 16
|
20 | | simpll 790 |
. . . . . . . . . . . . . . . . . . 19
|
21 | | indislem 20804 |
. . . . . . . . . . . . . . . . . . 19
|
22 | 20, 21 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . 18
|
23 | | elpri 4197 |
. . . . . . . . . . . . . . . . . 18
|
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
25 | 24 | ord 392 |
. . . . . . . . . . . . . . . 16
|
26 | 19, 25 | mpd 15 |
. . . . . . . . . . . . . . 15
|
27 | 17 | simprd 479 |
. . . . . . . . . . . . . . . . 17
|
28 | 27 | neneqd 2799 |
. . . . . . . . . . . . . . . 16
|
29 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
|
30 | | indislem 20804 |
. . . . . . . . . . . . . . . . . . 19
|
31 | 29, 30 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . 18
|
32 | | elpri 4197 |
. . . . . . . . . . . . . . . . . 18
|
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
34 | 33 | ord 392 |
. . . . . . . . . . . . . . . 16
|
35 | 28, 34 | mpd 15 |
. . . . . . . . . . . . . . 15
|
36 | 26, 35 | xpeq12d 5140 |
. . . . . . . . . . . . . 14
|
37 | | simprr 796 |
. . . . . . . . . . . . . 14
|
38 | 36, 37 | eqsstr3d 3640 |
. . . . . . . . . . . . 13
|
39 | 38 | adantll 750 |
. . . . . . . . . . . 12
|
40 | 13, 39 | eqssd 3620 |
. . . . . . . . . . 11
|
41 | 40 | ex 450 |
. . . . . . . . . 10
|
42 | 41 | rexlimdvva 3038 |
. . . . . . . . 9
|
43 | 7, 42 | syld 47 |
. . . . . . . 8
|
44 | 43 | exlimdv 1861 |
. . . . . . 7
|
45 | 1, 44 | syl5bi 232 |
. . . . . 6
|
46 | 45 | orrd 393 |
. . . . 5
|
47 | | vex 3203 |
. . . . . 6
|
48 | 47 | elpr 4198 |
. . . . 5
|
49 | 46, 48 | sylibr 224 |
. . . 4
|
50 | 49 | ssriv 3607 |
. . 3
|
51 | 9 | toptopon 20722 |
. . . . . . 7
TopOn |
52 | 2, 51 | mpbi 220 |
. . . . . 6
TopOn
|
53 | 10 | toptopon 20722 |
. . . . . . 7
TopOn |
54 | 3, 53 | mpbi 220 |
. . . . . 6
TopOn
|
55 | | txtopon 21394 |
. . . . . 6
TopOn
TopOn TopOn |
56 | 52, 54, 55 | mp2an 708 |
. . . . 5
TopOn |
57 | | topgele 20734 |
. . . . 5
TopOn
|
58 | 56, 57 | ax-mp 5 |
. . . 4
|
59 | 58 | simpli 474 |
. . 3
|
60 | 50, 59 | eqssi 3619 |
. 2
|
61 | | txindislem 21436 |
. . 3
|
62 | 61 | preq2i 4272 |
. 2
|
63 | | indislem 20804 |
. 2
|
64 | 60, 62, 63 | 3eqtri 2648 |
1
|