Step | Hyp | Ref
| Expression |
1 | | imasval.u |
. 2
s |
2 | | df-imas 16168 |
. . . 4
s
Scalar Scalar Scalar
TopSet
qTop
inf
g |
3 | 2 | a1i 11 |
. . 3
s
Scalar Scalar Scalar
TopSet
qTop
inf
g |
4 | | fvexd 6203 |
. . . 4
|
5 | | simplrl 800 |
. . . . . . . . . 10
|
6 | 5 | rneqd 5353 |
. . . . . . . . 9
|
7 | | imasval.f |
. . . . . . . . . . 11
|
8 | | forn 6118 |
. . . . . . . . . . 11
|
9 | 7, 8 | syl 17 |
. . . . . . . . . 10
|
10 | 9 | ad2antrr 762 |
. . . . . . . . 9
|
11 | 6, 10 | eqtrd 2656 |
. . . . . . . 8
|
12 | 11 | opeq2d 4409 |
. . . . . . 7
|
13 | | simplrr 801 |
. . . . . . . . . . . 12
|
14 | 13 | fveq2d 6195 |
. . . . . . . . . . 11
|
15 | | simpr 477 |
. . . . . . . . . . 11
|
16 | | imasval.v |
. . . . . . . . . . . 12
|
17 | 16 | ad2antrr 762 |
. . . . . . . . . . 11
|
18 | 14, 15, 17 | 3eqtr4d 2666 |
. . . . . . . . . 10
|
19 | 5 | fveq1d 6193 |
. . . . . . . . . . . . . 14
|
20 | 5 | fveq1d 6193 |
. . . . . . . . . . . . . 14
|
21 | 19, 20 | opeq12d 4410 |
. . . . . . . . . . . . 13
|
22 | 13 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
23 | | imasval.p |
. . . . . . . . . . . . . . . 16
|
24 | 22, 23 | syl6eqr 2674 |
. . . . . . . . . . . . . . 15
|
25 | 24 | oveqd 6667 |
. . . . . . . . . . . . . 14
|
26 | 5, 25 | fveq12d 6197 |
. . . . . . . . . . . . 13
|
27 | 21, 26 | opeq12d 4410 |
. . . . . . . . . . . 12
|
28 | 27 | sneqd 4189 |
. . . . . . . . . . 11
|
29 | 18, 28 | iuneq12d 4546 |
. . . . . . . . . 10
|
30 | 18, 29 | iuneq12d 4546 |
. . . . . . . . 9
|
31 | | imasval.a |
. . . . . . . . . 10
|
32 | 31 | ad2antrr 762 |
. . . . . . . . 9
|
33 | 30, 32 | eqtr4d 2659 |
. . . . . . . 8
|
34 | 33 | opeq2d 4409 |
. . . . . . 7
|
35 | 13 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
36 | | imasval.m |
. . . . . . . . . . . . . . . 16
|
37 | 35, 36 | syl6eqr 2674 |
. . . . . . . . . . . . . . 15
|
38 | 37 | oveqd 6667 |
. . . . . . . . . . . . . 14
|
39 | 5, 38 | fveq12d 6197 |
. . . . . . . . . . . . 13
|
40 | 21, 39 | opeq12d 4410 |
. . . . . . . . . . . 12
|
41 | 40 | sneqd 4189 |
. . . . . . . . . . 11
|
42 | 18, 41 | iuneq12d 4546 |
. . . . . . . . . 10
|
43 | 18, 42 | iuneq12d 4546 |
. . . . . . . . 9
|
44 | | imasval.t |
. . . . . . . . . 10
|
45 | 44 | ad2antrr 762 |
. . . . . . . . 9
|
46 | 43, 45 | eqtr4d 2659 |
. . . . . . . 8
|
47 | 46 | opeq2d 4409 |
. . . . . . 7
|
48 | 12, 34, 47 | tpeq123d 4283 |
. . . . . 6
|
49 | 13 | fveq2d 6195 |
. . . . . . . . 9
Scalar Scalar |
50 | | imasval.g |
. . . . . . . . 9
Scalar |
51 | 49, 50 | syl6eqr 2674 |
. . . . . . . 8
Scalar |
52 | 51 | opeq2d 4409 |
. . . . . . 7
Scalar Scalar Scalar |
53 | 51 | fveq2d 6195 |
. . . . . . . . . . . 12
Scalar |
54 | | imasval.k |
. . . . . . . . . . . 12
|
55 | 53, 54 | syl6eqr 2674 |
. . . . . . . . . . 11
Scalar |
56 | 20 | sneqd 4189 |
. . . . . . . . . . 11
|
57 | 13 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
58 | | imasval.q |
. . . . . . . . . . . . . 14
|
59 | 57, 58 | syl6eqr 2674 |
. . . . . . . . . . . . 13
|
60 | 59 | oveqd 6667 |
. . . . . . . . . . . 12
|
61 | 5, 60 | fveq12d 6197 |
. . . . . . . . . . 11
|
62 | 55, 56, 61 | mpt2eq123dv 6717 |
. . . . . . . . . 10
Scalar
|
63 | 62 | iuneq2d 4547 |
. . . . . . . . 9
Scalar
|
64 | 18 | iuneq1d 4545 |
. . . . . . . . 9
Scalar
Scalar |
65 | | imasval.s |
. . . . . . . . . 10
|
66 | 65 | ad2antrr 762 |
. . . . . . . . 9
|
67 | 63, 64, 66 | 3eqtr4d 2666 |
. . . . . . . 8
Scalar |
68 | 67 | opeq2d 4409 |
. . . . . . 7
Scalar
|
69 | 13 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
70 | | imasval.i |
. . . . . . . . . . . . . . 15
|
71 | 69, 70 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
|
72 | 71 | oveqd 6667 |
. . . . . . . . . . . . 13
|
73 | 21, 72 | opeq12d 4410 |
. . . . . . . . . . . 12
|
74 | 73 | sneqd 4189 |
. . . . . . . . . . 11
|
75 | 18, 74 | iuneq12d 4546 |
. . . . . . . . . 10
|
76 | 18, 75 | iuneq12d 4546 |
. . . . . . . . 9
|
77 | | imasval.w |
. . . . . . . . . 10
|
78 | 77 | ad2antrr 762 |
. . . . . . . . 9
|
79 | 76, 78 | eqtr4d 2659 |
. . . . . . . 8
|
80 | 79 | opeq2d 4409 |
. . . . . . 7
|
81 | 52, 68, 80 | tpeq123d 4283 |
. . . . . 6
Scalar Scalar Scalar
Scalar |
82 | 48, 81 | uneq12d 3768 |
. . . . 5
Scalar Scalar Scalar
Scalar |
83 | 13 | fveq2d 6195 |
. . . . . . . . . 10
|
84 | | imasval.j |
. . . . . . . . . 10
|
85 | 83, 84 | syl6eqr 2674 |
. . . . . . . . 9
|
86 | 85, 5 | oveq12d 6668 |
. . . . . . . 8
qTop qTop |
87 | | imasval.o |
. . . . . . . . 9
qTop |
88 | 87 | ad2antrr 762 |
. . . . . . . 8
qTop |
89 | 86, 88 | eqtr4d 2659 |
. . . . . . 7
qTop |
90 | 89 | opeq2d 4409 |
. . . . . 6
TopSet qTop TopSet |
91 | 13 | fveq2d 6195 |
. . . . . . . . . . 11
|
92 | | imasval.n |
. . . . . . . . . . 11
|
93 | 91, 92 | syl6eqr 2674 |
. . . . . . . . . 10
|
94 | 5, 93 | coeq12d 5286 |
. . . . . . . . 9
|
95 | 5 | cnveqd 5298 |
. . . . . . . . 9
|
96 | 94, 95 | coeq12d 5286 |
. . . . . . . 8
|
97 | | imasval.l |
. . . . . . . . 9
|
98 | 97 | ad2antrr 762 |
. . . . . . . 8
|
99 | 96, 98 | eqtr4d 2659 |
. . . . . . 7
|
100 | 99 | opeq2d 4409 |
. . . . . 6
|
101 | 18 | sqxpeqd 5141 |
. . . . . . . . . . . . . . 15
|
102 | 101 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
103 | 5 | fveq1d 6193 |
. . . . . . . . . . . . . . . 16
|
104 | 103 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
|
105 | 5 | fveq1d 6193 |
. . . . . . . . . . . . . . . 16
|
106 | 105 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
|
107 | 5 | fveq1d 6193 |
. . . . . . . . . . . . . . . . 17
|
108 | 5 | fveq1d 6193 |
. . . . . . . . . . . . . . . . 17
|
109 | 107, 108 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
|
110 | 109 | ralbidv 2986 |
. . . . . . . . . . . . . . 15
|
111 | 104, 106,
110 | 3anbi123d 1399 |
. . . . . . . . . . . . . 14
|
112 | 102, 111 | rabeqbidv 3195 |
. . . . . . . . . . . . 13
|
113 | 13 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
114 | | imasval.e |
. . . . . . . . . . . . . . . 16
|
115 | 113, 114 | syl6eqr 2674 |
. . . . . . . . . . . . . . 15
|
116 | 115 | coeq1d 5283 |
. . . . . . . . . . . . . 14
|
117 | 116 | oveq2d 6666 |
. . . . . . . . . . . . 13
g g |
118 | 112, 117 | mpteq12dv 4733 |
. . . . . . . . . . . 12
g g |
119 | 118 | rneqd 5353 |
. . . . . . . . . . 11
g g |
120 | 119 | iuneq2d 4547 |
. . . . . . . . . 10
g
g |
121 | 120 | infeq1d 8383 |
. . . . . . . . 9
inf g inf
g |
122 | 11, 11, 121 | mpt2eq123dv 6717 |
. . . . . . . 8
inf
g
inf g
|
123 | | imasval.d |
. . . . . . . . 9
inf
g |
124 | 123 | ad2antrr 762 |
. . . . . . . 8
inf g
|
125 | 122, 124 | eqtr4d 2659 |
. . . . . . 7
inf
g |
126 | 125 | opeq2d 4409 |
. . . . . 6
inf g
|
127 | 90, 100, 126 | tpeq123d 4283 |
. . . . 5
TopSet qTop
inf
g
TopSet |
128 | 82, 127 | uneq12d 3768 |
. . . 4
Scalar Scalar Scalar
TopSet
qTop
inf
g Scalar TopSet
|
129 | 4, 128 | csbied 3560 |
. . 3
Scalar Scalar Scalar
TopSet
qTop
inf
g Scalar TopSet
|
130 | | fof 6115 |
. . . . 5
|
131 | 7, 130 | syl 17 |
. . . 4
|
132 | | fvex 6201 |
. . . . 5
|
133 | 16, 132 | syl6eqel 2709 |
. . . 4
|
134 | | fex 6490 |
. . . 4
|
135 | 131, 133,
134 | syl2anc 693 |
. . 3
|
136 | | imasval.r |
. . . 4
|
137 | | elex 3212 |
. . . 4
|
138 | 136, 137 | syl 17 |
. . 3
|
139 | | tpex 6957 |
. . . . . 6
|
140 | | tpex 6957 |
. . . . . 6
Scalar |
141 | 139, 140 | unex 6956 |
. . . . 5
Scalar |
142 | | tpex 6957 |
. . . . 5
TopSet |
143 | 141, 142 | unex 6956 |
. . . 4
Scalar TopSet
|
144 | 143 | a1i 11 |
. . 3
Scalar TopSet
|
145 | 3, 129, 135, 138, 144 | ovmpt2d 6788 |
. 2
s
Scalar TopSet
|
146 | 1, 145 | eqtrd 2656 |
1
Scalar TopSet
|