Detailed syntax breakdown of Definition df-om1
Step | Hyp | Ref
| Expression |
1 | | comi 24174 |
. 2
class
Ω1 |
2 | | vj |
. . 3
setvar 𝑗 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | ctop 22052 |
. . 3
class
Top |
5 | 2 | cv 1538 |
. . . 4
class 𝑗 |
6 | 5 | cuni 4839 |
. . 3
class ∪ 𝑗 |
7 | | cnx 16904 |
. . . . . 6
class
ndx |
8 | | cbs 16922 |
. . . . . 6
class
Base |
9 | 7, 8 | cfv 6426 |
. . . . 5
class
(Base‘ndx) |
10 | | cc0 10881 |
. . . . . . . . 9
class
0 |
11 | | vf |
. . . . . . . . . 10
setvar 𝑓 |
12 | 11 | cv 1538 |
. . . . . . . . 9
class 𝑓 |
13 | 10, 12 | cfv 6426 |
. . . . . . . 8
class (𝑓‘0) |
14 | 3 | cv 1538 |
. . . . . . . 8
class 𝑦 |
15 | 13, 14 | wceq 1539 |
. . . . . . 7
wff (𝑓‘0) = 𝑦 |
16 | | c1 10882 |
. . . . . . . . 9
class
1 |
17 | 16, 12 | cfv 6426 |
. . . . . . . 8
class (𝑓‘1) |
18 | 17, 14 | wceq 1539 |
. . . . . . 7
wff (𝑓‘1) = 𝑦 |
19 | 15, 18 | wa 396 |
. . . . . 6
wff ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦) |
20 | | cii 24048 |
. . . . . . 7
class
II |
21 | | ccn 22385 |
. . . . . . 7
class
Cn |
22 | 20, 5, 21 | co 7267 |
. . . . . 6
class (II Cn
𝑗) |
23 | 19, 11, 22 | crab 3068 |
. . . . 5
class {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)} |
24 | 9, 23 | cop 4567 |
. . . 4
class
〈(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}〉 |
25 | | cplusg 16972 |
. . . . . 6
class
+g |
26 | 7, 25 | cfv 6426 |
. . . . 5
class
(+g‘ndx) |
27 | | cpco 24173 |
. . . . . 6
class
*𝑝 |
28 | 5, 27 | cfv 6426 |
. . . . 5
class
(*𝑝‘𝑗) |
29 | 26, 28 | cop 4567 |
. . . 4
class
〈(+g‘ndx), (*𝑝‘𝑗)〉 |
30 | | cts 16978 |
. . . . . 6
class
TopSet |
31 | 7, 30 | cfv 6426 |
. . . . 5
class
(TopSet‘ndx) |
32 | | cxko 22722 |
. . . . . 6
class
↑ko |
33 | 5, 20, 32 | co 7267 |
. . . . 5
class (𝑗 ↑ko
II) |
34 | 31, 33 | cop 4567 |
. . . 4
class
〈(TopSet‘ndx), (𝑗 ↑ko
II)〉 |
35 | 24, 29, 34 | ctp 4565 |
. . 3
class
{〈(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}〉, 〈(+g‘ndx),
(*𝑝‘𝑗)〉, 〈(TopSet‘ndx), (𝑗 ↑ko
II)〉} |
36 | 2, 3, 4, 6, 35 | cmpo 7269 |
. 2
class (𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗 ↦
{〈(Base‘ndx), {𝑓
∈ (II Cn 𝑗) ∣
((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}〉, 〈(+g‘ndx),
(*𝑝‘𝑗)〉, 〈(TopSet‘ndx), (𝑗 ↑ko
II)〉}) |
37 | 1, 36 | wceq 1539 |
1
wff
Ω1 = (𝑗
∈ Top, 𝑦 ∈ ∪ 𝑗
↦ {〈(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}〉, 〈(+g‘ndx),
(*𝑝‘𝑗)〉, 〈(TopSet‘ndx), (𝑗 ↑ko
II)〉}) |