Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . . . . . . . . 12
|
2 | 1 | kqid 21531 |
. . . . . . . . . . 11
TopOn
KQ |
3 | 2 | ad2antrr 762 |
. . . . . . . . . 10
TopOn KQ
KQ |
4 | | cnima 21069 |
. . . . . . . . . 10
KQ KQ
|
5 | 3, 4 | sylan 488 |
. . . . . . . . 9
TopOn KQ
KQ
|
6 | | eleq2 2690 |
. . . . . . . . . . 11
|
7 | | eleq2 2690 |
. . . . . . . . . . 11
|
8 | 6, 7 | imbi12d 334 |
. . . . . . . . . 10
|
9 | 8 | rspcv 3305 |
. . . . . . . . 9
|
10 | 5, 9 | syl 17 |
. . . . . . . 8
TopOn KQ
KQ
|
11 | 1 | kqffn 21528 |
. . . . . . . . . . . . 13
TopOn
|
12 | 11 | ad2antrr 762 |
. . . . . . . . . . . 12
TopOn KQ
|
13 | 12 | adantr 481 |
. . . . . . . . . . 11
TopOn KQ
KQ
|
14 | | fnfun 5988 |
. . . . . . . . . . 11
|
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
TopOn KQ
KQ
|
16 | | simprl 794 |
. . . . . . . . . . . 12
TopOn KQ |
17 | 16 | adantr 481 |
. . . . . . . . . . 11
TopOn KQ
KQ
|
18 | | fndm 5990 |
. . . . . . . . . . . 12
|
19 | 13, 18 | syl 17 |
. . . . . . . . . . 11
TopOn KQ
KQ
|
20 | 17, 19 | eleqtrrd 2704 |
. . . . . . . . . 10
TopOn KQ
KQ
|
21 | | fvimacnv 6332 |
. . . . . . . . . 10
|
22 | 15, 20, 21 | syl2anc 693 |
. . . . . . . . 9
TopOn KQ
KQ
|
23 | | simprr 796 |
. . . . . . . . . . . 12
TopOn KQ
|
24 | 23 | adantr 481 |
. . . . . . . . . . 11
TopOn KQ
KQ
|
25 | 24, 19 | eleqtrrd 2704 |
. . . . . . . . . 10
TopOn KQ
KQ
|
26 | | fvimacnv 6332 |
. . . . . . . . . 10
|
27 | 15, 25, 26 | syl2anc 693 |
. . . . . . . . 9
TopOn KQ
KQ
|
28 | 22, 27 | imbi12d 334 |
. . . . . . . 8
TopOn KQ
KQ
|
29 | 10, 28 | sylibrd 249 |
. . . . . . 7
TopOn KQ
KQ
|
30 | 29 | ralrimdva 2969 |
. . . . . 6
TopOn KQ
KQ |
31 | | simplr 792 |
. . . . . . 7
TopOn KQ KQ |
32 | | fnfvelrn 6356 |
. . . . . . . . 9
|
33 | 12, 16, 32 | syl2anc 693 |
. . . . . . . 8
TopOn KQ |
34 | 1 | kqtopon 21530 |
. . . . . . . . . 10
TopOn
KQ TopOn |
35 | 34 | ad2antrr 762 |
. . . . . . . . 9
TopOn KQ KQ TopOn |
36 | | toponuni 20719 |
. . . . . . . . 9
KQ TopOn
KQ |
37 | 35, 36 | syl 17 |
. . . . . . . 8
TopOn KQ KQ |
38 | 33, 37 | eleqtrd 2703 |
. . . . . . 7
TopOn KQ KQ |
39 | | fnfvelrn 6356 |
. . . . . . . . 9
|
40 | 12, 23, 39 | syl2anc 693 |
. . . . . . . 8
TopOn KQ |
41 | 40, 37 | eleqtrd 2703 |
. . . . . . 7
TopOn KQ KQ |
42 | | eqid 2622 |
. . . . . . . 8
KQ KQ |
43 | 42 | t1sep2 21173 |
. . . . . . 7
KQ KQ
KQ KQ
|
44 | 31, 38, 41, 43 | syl3anc 1326 |
. . . . . 6
TopOn KQ KQ
|
45 | 30, 44 | syld 47 |
. . . . 5
TopOn KQ
|
46 | 1 | kqfeq 21527 |
. . . . . . . 8
TopOn
|
47 | | eleq2 2690 |
. . . . . . . . . 10
|
48 | | eleq2 2690 |
. . . . . . . . . 10
|
49 | 47, 48 | bibi12d 335 |
. . . . . . . . 9
|
50 | 49 | cbvralv 3171 |
. . . . . . . 8
|
51 | 46, 50 | syl6bbr 278 |
. . . . . . 7
TopOn
|
52 | 51 | 3expb 1266 |
. . . . . 6
TopOn
|
53 | 52 | adantlr 751 |
. . . . 5
TopOn KQ
|
54 | 45, 53 | sylibd 229 |
. . . 4
TopOn KQ
|
55 | 54 | ralrimivva 2971 |
. . 3
TopOn KQ
|
56 | 55 | ex 450 |
. 2
TopOn
KQ
|
57 | | simpll 790 |
. . . . . . . . . . 11
TopOn TopOn |
58 | 1 | kqopn 21537 |
. . . . . . . . . . 11
TopOn KQ |
59 | 57, 58 | sylan 488 |
. . . . . . . . . 10
TopOn
KQ |
60 | | eleq2 2690 |
. . . . . . . . . . . 12
|
61 | | eleq2 2690 |
. . . . . . . . . . . 12
|
62 | 60, 61 | imbi12d 334 |
. . . . . . . . . . 11
|
63 | 62 | rspcv 3305 |
. . . . . . . . . 10
KQ
KQ
|
64 | 59, 63 | syl 17 |
. . . . . . . . 9
TopOn
KQ |
65 | 1 | kqfvima 21533 |
. . . . . . . . . . . . 13
TopOn
|
66 | 65 | 3expa 1265 |
. . . . . . . . . . . 12
TopOn
|
67 | 66 | an32s 846 |
. . . . . . . . . . 11
TopOn
|
68 | 67 | adantlr 751 |
. . . . . . . . . 10
TopOn
|
69 | 1 | kqfvima 21533 |
. . . . . . . . . . . . 13
TopOn
|
70 | 69 | 3expa 1265 |
. . . . . . . . . . . 12
TopOn
|
71 | 70 | an32s 846 |
. . . . . . . . . . 11
TopOn
|
72 | 71 | adantllr 755 |
. . . . . . . . . 10
TopOn
|
73 | 68, 72 | imbi12d 334 |
. . . . . . . . 9
TopOn
|
74 | 64, 73 | sylibrd 249 |
. . . . . . . 8
TopOn
KQ
|
75 | 74 | ralrimdva 2969 |
. . . . . . 7
TopOn
KQ
|
76 | 1 | kqfval 21526 |
. . . . . . . . . . 11
TopOn
|
77 | 76 | adantr 481 |
. . . . . . . . . 10
TopOn
|
78 | 1 | kqfval 21526 |
. . . . . . . . . . 11
TopOn
|
79 | 78 | adantlr 751 |
. . . . . . . . . 10
TopOn
|
80 | 77, 79 | eqeq12d 2637 |
. . . . . . . . 9
TopOn
|
81 | | rabbi 3120 |
. . . . . . . . . 10
|
82 | 50, 81 | bitri 264 |
. . . . . . . . 9
|
83 | 80, 82 | syl6bbr 278 |
. . . . . . . 8
TopOn
|
84 | 83 | biimprd 238 |
. . . . . . 7
TopOn
|
85 | 75, 84 | imim12d 81 |
. . . . . 6
TopOn
KQ |
86 | 85 | ralimdva 2962 |
. . . . 5
TopOn
KQ
|
87 | 86 | ralimdva 2962 |
. . . 4
TopOn
KQ
|
88 | | eleq1 2689 |
. . . . . . . . . . 11
|
89 | 88 | imbi1d 331 |
. . . . . . . . . 10
|
90 | 89 | ralbidv 2986 |
. . . . . . . . 9
KQ
KQ |
91 | | eqeq1 2626 |
. . . . . . . . 9
|
92 | 90, 91 | imbi12d 334 |
. . . . . . . 8
KQ
KQ
|
93 | 92 | ralbidv 2986 |
. . . . . . 7
KQ
KQ
|
94 | 93 | ralrn 6362 |
. . . . . 6
KQ
KQ
|
95 | | eleq1 2689 |
. . . . . . . . . . 11
|
96 | 95 | imbi2d 330 |
. . . . . . . . . 10
|
97 | 96 | ralbidv 2986 |
. . . . . . . . 9
KQ
KQ |
98 | | eqeq2 2633 |
. . . . . . . . 9
|
99 | 97, 98 | imbi12d 334 |
. . . . . . . 8
KQ
KQ
|
100 | 99 | ralrn 6362 |
. . . . . . 7
KQ
KQ |
101 | 100 | ralbidv 2986 |
. . . . . 6
KQ
KQ |
102 | 94, 101 | bitrd 268 |
. . . . 5
KQ
KQ
|
103 | 11, 102 | syl 17 |
. . . 4
TopOn
KQ
KQ |
104 | 87, 103 | sylibrd 249 |
. . 3
TopOn
KQ
|
105 | | ist1-2 21151 |
. . . 4
KQ TopOn KQ
KQ |
106 | 34, 105 | syl 17 |
. . 3
TopOn
KQ
KQ |
107 | 104, 106 | sylibrd 249 |
. 2
TopOn
KQ |
108 | 56, 107 | impbid 202 |
1
TopOn
KQ
|