Detailed syntax breakdown of Definition df-cvm
Step | Hyp | Ref
| Expression |
1 | | ccvm 32788 |
. 2
class
CovMap |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | vj |
. . 3
setvar 𝑗 |
4 | | ctop 21644 |
. . 3
class
Top |
5 | | vx |
. . . . . . . 8
setvar 𝑥 |
6 | | vk |
. . . . . . . 8
setvar 𝑘 |
7 | 5, 6 | wel 2115 |
. . . . . . 7
wff 𝑥 ∈ 𝑘 |
8 | | vs |
. . . . . . . . . . . 12
setvar 𝑠 |
9 | 8 | cv 1541 |
. . . . . . . . . . 11
class 𝑠 |
10 | 9 | cuni 4796 |
. . . . . . . . . 10
class ∪ 𝑠 |
11 | | vf |
. . . . . . . . . . . . 13
setvar 𝑓 |
12 | 11 | cv 1541 |
. . . . . . . . . . . 12
class 𝑓 |
13 | 12 | ccnv 5524 |
. . . . . . . . . . 11
class ◡𝑓 |
14 | 6 | cv 1541 |
. . . . . . . . . . 11
class 𝑘 |
15 | 13, 14 | cima 5528 |
. . . . . . . . . 10
class (◡𝑓 “ 𝑘) |
16 | 10, 15 | wceq 1542 |
. . . . . . . . 9
wff ∪ 𝑠 =
(◡𝑓 “ 𝑘) |
17 | | vu |
. . . . . . . . . . . . . . 15
setvar 𝑢 |
18 | 17 | cv 1541 |
. . . . . . . . . . . . . 14
class 𝑢 |
19 | | vv |
. . . . . . . . . . . . . . 15
setvar 𝑣 |
20 | 19 | cv 1541 |
. . . . . . . . . . . . . 14
class 𝑣 |
21 | 18, 20 | cin 3842 |
. . . . . . . . . . . . 13
class (𝑢 ∩ 𝑣) |
22 | | c0 4211 |
. . . . . . . . . . . . 13
class
∅ |
23 | 21, 22 | wceq 1542 |
. . . . . . . . . . . 12
wff (𝑢 ∩ 𝑣) = ∅ |
24 | 18 | csn 4516 |
. . . . . . . . . . . . 13
class {𝑢} |
25 | 9, 24 | cdif 3840 |
. . . . . . . . . . . 12
class (𝑠 ∖ {𝑢}) |
26 | 23, 19, 25 | wral 3053 |
. . . . . . . . . . 11
wff
∀𝑣 ∈
(𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ |
27 | 12, 18 | cres 5527 |
. . . . . . . . . . . 12
class (𝑓 ↾ 𝑢) |
28 | 2 | cv 1541 |
. . . . . . . . . . . . . 14
class 𝑐 |
29 | | crest 16797 |
. . . . . . . . . . . . . 14
class
↾t |
30 | 28, 18, 29 | co 7170 |
. . . . . . . . . . . . 13
class (𝑐 ↾t 𝑢) |
31 | 3 | cv 1541 |
. . . . . . . . . . . . . 14
class 𝑗 |
32 | 31, 14, 29 | co 7170 |
. . . . . . . . . . . . 13
class (𝑗 ↾t 𝑘) |
33 | | chmeo 22504 |
. . . . . . . . . . . . 13
class
Homeo |
34 | 30, 32, 33 | co 7170 |
. . . . . . . . . . . 12
class ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)) |
35 | 27, 34 | wcel 2114 |
. . . . . . . . . . 11
wff (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)) |
36 | 26, 35 | wa 399 |
. . . . . . . . . 10
wff
(∀𝑣 ∈
(𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘))) |
37 | 36, 17, 9 | wral 3053 |
. . . . . . . . 9
wff
∀𝑢 ∈
𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘))) |
38 | 16, 37 | wa 399 |
. . . . . . . 8
wff (∪ 𝑠 =
(◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))) |
39 | 28 | cpw 4488 |
. . . . . . . . 9
class 𝒫
𝑐 |
40 | 22 | csn 4516 |
. . . . . . . . 9
class
{∅} |
41 | 39, 40 | cdif 3840 |
. . . . . . . 8
class
(𝒫 𝑐 ∖
{∅}) |
42 | 38, 8, 41 | wrex 3054 |
. . . . . . 7
wff
∃𝑠 ∈
(𝒫 𝑐 ∖
{∅})(∪ 𝑠 = (◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))) |
43 | 7, 42 | wa 399 |
. . . . . 6
wff (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 =
(◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘))))) |
44 | 43, 6, 31 | wrex 3054 |
. . . . 5
wff
∃𝑘 ∈
𝑗 (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 =
(◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘))))) |
45 | 31 | cuni 4796 |
. . . . 5
class ∪ 𝑗 |
46 | 44, 5, 45 | wral 3053 |
. . . 4
wff
∀𝑥 ∈
∪ 𝑗∃𝑘 ∈ 𝑗 (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 =
(◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘))))) |
47 | | ccn 21975 |
. . . . 5
class
Cn |
48 | 28, 31, 47 | co 7170 |
. . . 4
class (𝑐 Cn 𝑗) |
49 | 46, 11, 48 | crab 3057 |
. . 3
class {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑘 ∈ 𝑗 (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 =
(◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))))} |
50 | 2, 3, 4, 4, 49 | cmpo 7172 |
. 2
class (𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑘 ∈ 𝑗 (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 =
(◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))))}) |
51 | 1, 50 | wceq 1542 |
1
wff CovMap =
(𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑘 ∈ 𝑗 (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 =
(◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))))}) |