Detailed syntax breakdown of Definition df-om1
Step | Hyp | Ref
| Expression |
1 | | comi 23208 |
. 2
class
Ω1 |
2 | | vj |
. . 3
setvar 𝑗 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | ctop 21105 |
. . 3
class
Top |
5 | 2 | cv 1600 |
. . . 4
class 𝑗 |
6 | 5 | cuni 4671 |
. . 3
class ∪ 𝑗 |
7 | | cnx 16252 |
. . . . . 6
class
ndx |
8 | | cbs 16255 |
. . . . . 6
class
Base |
9 | 7, 8 | cfv 6135 |
. . . . 5
class
(Base‘ndx) |
10 | | cc0 10272 |
. . . . . . . . 9
class
0 |
11 | | vf |
. . . . . . . . . 10
setvar 𝑓 |
12 | 11 | cv 1600 |
. . . . . . . . 9
class 𝑓 |
13 | 10, 12 | cfv 6135 |
. . . . . . . 8
class (𝑓‘0) |
14 | 3 | cv 1600 |
. . . . . . . 8
class 𝑦 |
15 | 13, 14 | wceq 1601 |
. . . . . . 7
wff (𝑓‘0) = 𝑦 |
16 | | c1 10273 |
. . . . . . . . 9
class
1 |
17 | 16, 12 | cfv 6135 |
. . . . . . . 8
class (𝑓‘1) |
18 | 17, 14 | wceq 1601 |
. . . . . . 7
wff (𝑓‘1) = 𝑦 |
19 | 15, 18 | wa 386 |
. . . . . 6
wff ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦) |
20 | | cii 23086 |
. . . . . . 7
class
II |
21 | | ccn 21436 |
. . . . . . 7
class
Cn |
22 | 20, 5, 21 | co 6922 |
. . . . . 6
class (II Cn
𝑗) |
23 | 19, 11, 22 | crab 3094 |
. . . . 5
class {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)} |
24 | 9, 23 | cop 4404 |
. . . 4
class
〈(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}〉 |
25 | | cplusg 16338 |
. . . . . 6
class
+g |
26 | 7, 25 | cfv 6135 |
. . . . 5
class
(+g‘ndx) |
27 | | cpco 23207 |
. . . . . 6
class
*𝑝 |
28 | 5, 27 | cfv 6135 |
. . . . 5
class
(*𝑝‘𝑗) |
29 | 26, 28 | cop 4404 |
. . . 4
class
〈(+g‘ndx), (*𝑝‘𝑗)〉 |
30 | | cts 16344 |
. . . . . 6
class
TopSet |
31 | 7, 30 | cfv 6135 |
. . . . 5
class
(TopSet‘ndx) |
32 | | cxko 21773 |
. . . . . 6
class
^ko |
33 | 5, 20, 32 | co 6922 |
. . . . 5
class (𝑗 ^ko
II) |
34 | 31, 33 | cop 4404 |
. . . 4
class
〈(TopSet‘ndx), (𝑗 ^ko
II)〉 |
35 | 24, 29, 34 | ctp 4402 |
. . 3
class
{〈(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}〉, 〈(+g‘ndx),
(*𝑝‘𝑗)〉, 〈(TopSet‘ndx), (𝑗 ^ko
II)〉} |
36 | 2, 3, 4, 6, 35 | cmpt2 6924 |
. 2
class (𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗 ↦
{〈(Base‘ndx), {𝑓
∈ (II Cn 𝑗) ∣
((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}〉, 〈(+g‘ndx),
(*𝑝‘𝑗)〉, 〈(TopSet‘ndx), (𝑗 ^ko
II)〉}) |
37 | 1, 36 | wceq 1601 |
1
wff
Ω1 = (𝑗
∈ Top, 𝑦 ∈ ∪ 𝑗
↦ {〈(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}〉, 〈(+g‘ndx),
(*𝑝‘𝑗)〉, 〈(TopSet‘ndx), (𝑗 ^ko
II)〉}) |