Step | Hyp | Ref
| Expression |
1 | | qtophmeo.2 |
. . . . 5
TopOn |
2 | | qtophmeo.3 |
. . . . 5
|
3 | | qtophmeo.4 |
. . . . . . 7
|
4 | | fofn 6117 |
. . . . . . 7
|
5 | 3, 4 | syl 17 |
. . . . . 6
|
6 | | qtopid 21508 |
. . . . . 6
TopOn qTop |
7 | 1, 5, 6 | syl2anc 693 |
. . . . 5
qTop |
8 | | df-3an 1039 |
. . . . . 6
|
9 | | qtophmeo.5 |
. . . . . . . 8
|
10 | 9 | biimpd 219 |
. . . . . . 7
|
11 | 10 | impr 649 |
. . . . . 6
|
12 | 8, 11 | sylan2b 492 |
. . . . 5
|
13 | 1, 2, 7, 12 | qtopeu 21519 |
. . . 4
qTop qTop |
14 | | reurex 3160 |
. . . 4
qTop qTop qTop qTop |
15 | 13, 14 | syl 17 |
. . 3
qTop qTop |
16 | | simprl 794 |
. . . . . . 7
qTop qTop
qTop qTop |
17 | | fofn 6117 |
. . . . . . . . . . . . 13
|
18 | 2, 17 | syl 17 |
. . . . . . . . . . . 12
|
19 | | qtopid 21508 |
. . . . . . . . . . . 12
TopOn qTop |
20 | 1, 18, 19 | syl2anc 693 |
. . . . . . . . . . 11
qTop |
21 | | df-3an 1039 |
. . . . . . . . . . . 12
|
22 | 9 | biimprd 238 |
. . . . . . . . . . . . 13
|
23 | 22 | impr 649 |
. . . . . . . . . . . 12
|
24 | 21, 23 | sylan2b 492 |
. . . . . . . . . . 11
|
25 | 1, 3, 20, 24 | qtopeu 21519 |
. . . . . . . . . 10
qTop qTop |
26 | 25 | adantr 481 |
. . . . . . . . 9
qTop qTop
qTop qTop |
27 | | reurex 3160 |
. . . . . . . . 9
qTop qTop qTop qTop |
28 | 26, 27 | syl 17 |
. . . . . . . 8
qTop qTop
qTop qTop |
29 | | qtoptopon 21507 |
. . . . . . . . . . . . 13
TopOn qTop TopOn |
30 | 1, 2, 29 | syl2anc 693 |
. . . . . . . . . . . 12
qTop TopOn |
31 | 30 | ad2antrr 762 |
. . . . . . . . . . 11
qTop qTop qTop qTop qTop TopOn |
32 | | qtoptopon 21507 |
. . . . . . . . . . . . 13
TopOn qTop TopOn |
33 | 1, 3, 32 | syl2anc 693 |
. . . . . . . . . . . 12
qTop TopOn |
34 | 33 | ad2antrr 762 |
. . . . . . . . . . 11
qTop qTop qTop qTop qTop TopOn |
35 | | simplrl 800 |
. . . . . . . . . . 11
qTop qTop qTop qTop qTop qTop |
36 | | cnf2 21053 |
. . . . . . . . . . 11
qTop TopOn
qTop TopOn qTop qTop |
37 | 31, 34, 35, 36 | syl3anc 1326 |
. . . . . . . . . 10
qTop qTop qTop qTop |
38 | | simprl 794 |
. . . . . . . . . . 11
qTop qTop qTop qTop qTop qTop |
39 | | cnf2 21053 |
. . . . . . . . . . 11
qTop TopOn
qTop TopOn qTop qTop |
40 | 34, 31, 38, 39 | syl3anc 1326 |
. . . . . . . . . 10
qTop qTop qTop qTop |
41 | | coeq1 5279 |
. . . . . . . . . . . 12
|
42 | 41 | eqeq2d 2632 |
. . . . . . . . . . 11
|
43 | | coeq1 5279 |
. . . . . . . . . . . 12
|
44 | 43 | eqeq2d 2632 |
. . . . . . . . . . 11
|
45 | | simpr3 1069 |
. . . . . . . . . . . . 13
|
46 | 1, 2, 20, 45 | qtopeu 21519 |
. . . . . . . . . . . 12
qTop qTop |
47 | 46 | ad2antrr 762 |
. . . . . . . . . . 11
qTop qTop qTop qTop qTop qTop |
48 | | cnco 21070 |
. . . . . . . . . . . 12
qTop qTop qTop qTop qTop qTop |
49 | 35, 38, 48 | syl2anc 693 |
. . . . . . . . . . 11
qTop qTop qTop qTop qTop qTop |
50 | | idcn 21061 |
. . . . . . . . . . . . 13
qTop TopOn qTop qTop |
51 | 30, 50 | syl 17 |
. . . . . . . . . . . 12
qTop qTop |
52 | 51 | ad2antrr 762 |
. . . . . . . . . . 11
qTop qTop qTop qTop qTop qTop |
53 | | simprr 796 |
. . . . . . . . . . . . 13
qTop qTop qTop qTop |
54 | | simplrr 801 |
. . . . . . . . . . . . . 14
qTop qTop qTop qTop |
55 | 54 | coeq2d 5284 |
. . . . . . . . . . . . 13
qTop qTop qTop qTop |
56 | 53, 55 | eqtrd 2656 |
. . . . . . . . . . . 12
qTop qTop qTop qTop |
57 | | coass 5654 |
. . . . . . . . . . . 12
|
58 | 56, 57 | syl6eqr 2674 |
. . . . . . . . . . 11
qTop qTop qTop qTop |
59 | | fof 6115 |
. . . . . . . . . . . . . . 15
|
60 | 2, 59 | syl 17 |
. . . . . . . . . . . . . 14
|
61 | 60 | ad2antrr 762 |
. . . . . . . . . . . . 13
qTop qTop qTop qTop |
62 | | fcoi2 6079 |
. . . . . . . . . . . . 13
|
63 | 61, 62 | syl 17 |
. . . . . . . . . . . 12
qTop qTop qTop qTop |
64 | 63 | eqcomd 2628 |
. . . . . . . . . . 11
qTop qTop qTop qTop |
65 | 42, 44, 47, 49, 52, 58, 64 | reu2eqd 3403 |
. . . . . . . . . 10
qTop qTop qTop qTop
|
66 | | coeq1 5279 |
. . . . . . . . . . . 12
|
67 | 66 | eqeq2d 2632 |
. . . . . . . . . . 11
|
68 | | coeq1 5279 |
. . . . . . . . . . . 12
|
69 | 68 | eqeq2d 2632 |
. . . . . . . . . . 11
|
70 | | simpr3 1069 |
. . . . . . . . . . . . 13
|
71 | 1, 3, 7, 70 | qtopeu 21519 |
. . . . . . . . . . . 12
qTop qTop |
72 | 71 | ad2antrr 762 |
. . . . . . . . . . 11
qTop qTop qTop qTop qTop qTop |
73 | | cnco 21070 |
. . . . . . . . . . . 12
qTop qTop qTop qTop qTop qTop |
74 | 38, 35, 73 | syl2anc 693 |
. . . . . . . . . . 11
qTop qTop qTop qTop qTop qTop |
75 | | idcn 21061 |
. . . . . . . . . . . . 13
qTop TopOn qTop qTop |
76 | 33, 75 | syl 17 |
. . . . . . . . . . . 12
qTop qTop |
77 | 76 | ad2antrr 762 |
. . . . . . . . . . 11
qTop qTop qTop qTop qTop qTop |
78 | 53 | coeq2d 5284 |
. . . . . . . . . . . . 13
qTop qTop qTop qTop |
79 | 54, 78 | eqtrd 2656 |
. . . . . . . . . . . 12
qTop qTop qTop qTop |
80 | | coass 5654 |
. . . . . . . . . . . 12
|
81 | 79, 80 | syl6eqr 2674 |
. . . . . . . . . . 11
qTop qTop qTop qTop |
82 | | fof 6115 |
. . . . . . . . . . . . . . 15
|
83 | 3, 82 | syl 17 |
. . . . . . . . . . . . . 14
|
84 | 83 | ad2antrr 762 |
. . . . . . . . . . . . 13
qTop qTop qTop qTop |
85 | | fcoi2 6079 |
. . . . . . . . . . . . 13
|
86 | 84, 85 | syl 17 |
. . . . . . . . . . . 12
qTop qTop qTop qTop |
87 | 86 | eqcomd 2628 |
. . . . . . . . . . 11
qTop qTop qTop qTop |
88 | 67, 69, 72, 74, 77, 81, 87 | reu2eqd 3403 |
. . . . . . . . . 10
qTop qTop qTop qTop
|
89 | 37, 40, 65, 88 | 2fcoidinvd 6550 |
. . . . . . . . 9
qTop qTop qTop qTop |
90 | 89, 38 | eqeltrd 2701 |
. . . . . . . 8
qTop qTop qTop qTop qTop qTop |
91 | 28, 90 | rexlimddv 3035 |
. . . . . . 7
qTop qTop
qTop qTop |
92 | | ishmeo 21562 |
. . . . . . 7
qTop qTop
qTop qTop
qTop
qTop |
93 | 16, 91, 92 | sylanbrc 698 |
. . . . . 6
qTop qTop
qTop qTop |
94 | | simprr 796 |
. . . . . 6
qTop qTop
|
95 | 93, 94 | jca 554 |
. . . . 5
qTop qTop
qTop qTop |
96 | 95 | ex 450 |
. . . 4
qTop qTop
qTop qTop |
97 | 96 | reximdv2 3014 |
. . 3
qTop qTop qTop qTop |
98 | 15, 97 | mpd 15 |
. 2
qTop qTop |
99 | | eqtr2 2642 |
. . . 4
|
100 | 2 | adantr 481 |
. . . . 5
qTop qTop qTop qTop |
101 | 30 | adantr 481 |
. . . . . . 7
qTop qTop qTop qTop qTop TopOn |
102 | 33 | adantr 481 |
. . . . . . 7
qTop qTop qTop qTop qTop TopOn |
103 | | simprl 794 |
. . . . . . 7
qTop qTop qTop qTop qTop qTop |
104 | | hmeof1o2 21566 |
. . . . . . 7
qTop TopOn
qTop TopOn qTop qTop |
105 | 101, 102,
103, 104 | syl3anc 1326 |
. . . . . 6
qTop qTop qTop qTop |
106 | | f1ofn 6138 |
. . . . . 6
|
107 | 105, 106 | syl 17 |
. . . . 5
qTop qTop qTop qTop |
108 | | simprr 796 |
. . . . . . 7
qTop qTop qTop qTop qTop qTop |
109 | | hmeof1o2 21566 |
. . . . . . 7
qTop TopOn
qTop TopOn qTop qTop |
110 | 101, 102,
108, 109 | syl3anc 1326 |
. . . . . 6
qTop qTop qTop qTop |
111 | | f1ofn 6138 |
. . . . . 6
|
112 | 110, 111 | syl 17 |
. . . . 5
qTop qTop qTop qTop |
113 | | cocan2 6547 |
. . . . 5
|
114 | 100, 107,
112, 113 | syl3anc 1326 |
. . . 4
qTop qTop qTop qTop |
115 | 99, 114 | syl5ib 234 |
. . 3
qTop qTop qTop qTop |
116 | 115 | ralrimivva 2971 |
. 2
qTop qTop qTop qTop
|
117 | | coeq1 5279 |
. . . 4
|
118 | 117 | eqeq2d 2632 |
. . 3
|
119 | 118 | reu4 3400 |
. 2
qTop qTop
qTop qTop
qTop qTop
qTop qTop
|
120 | 98, 116, 119 | sylanbrc 698 |
1
qTop qTop |