Step | Hyp | Ref
| Expression |
1 | | metcn.2 |
. . . . 5
|
2 | 1 | mopntopon 22244 |
. . . 4
TopOn |
3 | 2 | 3ad2ant1 1082 |
. . 3
TopOn |
4 | | metcn.4 |
. . . . 5
|
5 | 4 | mopnval 22243 |
. . . 4
|
6 | 5 | 3ad2ant2 1083 |
. . 3
|
7 | 4 | mopntopon 22244 |
. . . 4
TopOn |
8 | 7 | 3ad2ant2 1083 |
. . 3
TopOn |
9 | | simp3 1063 |
. . 3
|
10 | 3, 6, 8, 9 | tgcnp 21057 |
. 2
|
11 | | simpll2 1101 |
. . . . . . . 8
|
12 | | simplr 792 |
. . . . . . . . 9
|
13 | | simpll3 1102 |
. . . . . . . . 9
|
14 | 12, 13 | ffvelrnd 6360 |
. . . . . . . 8
|
15 | | simpr 477 |
. . . . . . . 8
|
16 | | blcntr 22218 |
. . . . . . . 8
|
17 | 11, 14, 15, 16 | syl3anc 1326 |
. . . . . . 7
|
18 | | rpxr 11840 |
. . . . . . . . . 10
|
19 | 18 | adantl 482 |
. . . . . . . . 9
|
20 | | blelrn 22222 |
. . . . . . . . 9
|
21 | 11, 14, 19, 20 | syl3anc 1326 |
. . . . . . . 8
|
22 | | eleq2 2690 |
. . . . . . . . . 10
|
23 | | sseq2 3627 |
. . . . . . . . . . . 12
|
24 | 23 | anbi2d 740 |
. . . . . . . . . . 11
|
25 | 24 | rexbidv 3052 |
. . . . . . . . . 10
|
26 | 22, 25 | imbi12d 334 |
. . . . . . . . 9
|
27 | 26 | rspcv 3305 |
. . . . . . . 8
|
28 | 21, 27 | syl 17 |
. . . . . . 7
|
29 | 17, 28 | mpid 44 |
. . . . . 6
|
30 | | simpl1 1064 |
. . . . . . . . . . . 12
|
31 | 30 | ad2antrr 762 |
. . . . . . . . . . 11
|
32 | | simplrr 801 |
. . . . . . . . . . 11
|
33 | | simpr 477 |
. . . . . . . . . . 11
|
34 | 1 | mopni2 22298 |
. . . . . . . . . . 11
|
35 | 31, 32, 33, 34 | syl3anc 1326 |
. . . . . . . . . 10
|
36 | | sstr2 3610 |
. . . . . . . . . . . 12
|
37 | | imass2 5501 |
. . . . . . . . . . . 12
|
38 | 36, 37 | syl11 33 |
. . . . . . . . . . 11
|
39 | 38 | reximdv 3016 |
. . . . . . . . . 10
|
40 | 35, 39 | syl5com 31 |
. . . . . . . . 9
|
41 | 40 | expimpd 629 |
. . . . . . . 8
|
42 | 41 | expr 643 |
. . . . . . 7
|
43 | 42 | rexlimdv 3030 |
. . . . . 6
|
44 | 29, 43 | syld 47 |
. . . . 5
|
45 | 44 | ralrimdva 2969 |
. . . 4
|
46 | | simpl2 1065 |
. . . . . . . . 9
|
47 | | blss 22230 |
. . . . . . . . . 10
|
48 | 47 | 3expib 1268 |
. . . . . . . . 9
|
49 | 46, 48 | syl 17 |
. . . . . . . 8
|
50 | | r19.29r 3073 |
. . . . . . . . . 10
|
51 | 30 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
|
52 | 13 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
53 | | rpxr 11840 |
. . . . . . . . . . . . . . . . 17
|
54 | 53 | ad2antrl 764 |
. . . . . . . . . . . . . . . 16
|
55 | 1 | blopn 22305 |
. . . . . . . . . . . . . . . 16
|
56 | 51, 52, 54, 55 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
57 | | simprl 794 |
. . . . . . . . . . . . . . . 16
|
58 | | blcntr 22218 |
. . . . . . . . . . . . . . . 16
|
59 | 51, 52, 57, 58 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
60 | | sstr 3611 |
. . . . . . . . . . . . . . . . 17
|
61 | 60 | ad2ant2l 782 |
. . . . . . . . . . . . . . . 16
|
62 | 61 | ancoms 469 |
. . . . . . . . . . . . . . 15
|
63 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
|
64 | | imaeq2 5462 |
. . . . . . . . . . . . . . . . . 18
|
65 | 64 | sseq1d 3632 |
. . . . . . . . . . . . . . . . 17
|
66 | 63, 65 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
|
67 | 66 | rspcev 3309 |
. . . . . . . . . . . . . . 15
|
68 | 56, 59, 62, 67 | syl12anc 1324 |
. . . . . . . . . . . . . 14
|
69 | 68 | expr 643 |
. . . . . . . . . . . . 13
|
70 | 69 | rexlimdva 3031 |
. . . . . . . . . . . 12
|
71 | 70 | expimpd 629 |
. . . . . . . . . . 11
|
72 | 71 | rexlimdva 3031 |
. . . . . . . . . 10
|
73 | 50, 72 | syl5 34 |
. . . . . . . . 9
|
74 | 73 | expd 452 |
. . . . . . . 8
|
75 | 49, 74 | syld 47 |
. . . . . . 7
|
76 | 75 | com23 86 |
. . . . . 6
|
77 | 76 | exp4a 633 |
. . . . 5
|
78 | 77 | ralrimdv 2968 |
. . . 4
|
79 | 45, 78 | impbid 202 |
. . 3
|
80 | 79 | pm5.32da 673 |
. 2
|
81 | 10, 80 | bitrd 268 |
1
|