Detailed syntax breakdown of Definition df-omni
Step | Hyp | Ref
| Expression |
1 | | comni 7106 |
. 2
class
Omni |
2 | | vy |
. . . . . . 7
setvar 𝑦 |
3 | 2 | cv 1347 |
. . . . . 6
class 𝑦 |
4 | | c2o 6386 |
. . . . . 6
class
2o |
5 | | vf |
. . . . . . 7
setvar 𝑓 |
6 | 5 | cv 1347 |
. . . . . 6
class 𝑓 |
7 | 3, 4, 6 | wf 5192 |
. . . . 5
wff 𝑓:𝑦⟶2o |
8 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
9 | 8 | cv 1347 |
. . . . . . . . 9
class 𝑥 |
10 | 9, 6 | cfv 5196 |
. . . . . . . 8
class (𝑓‘𝑥) |
11 | | c0 3414 |
. . . . . . . 8
class
∅ |
12 | 10, 11 | wceq 1348 |
. . . . . . 7
wff (𝑓‘𝑥) = ∅ |
13 | 12, 8, 3 | wrex 2449 |
. . . . . 6
wff
∃𝑥 ∈
𝑦 (𝑓‘𝑥) = ∅ |
14 | | c1o 6385 |
. . . . . . . 8
class
1o |
15 | 10, 14 | wceq 1348 |
. . . . . . 7
wff (𝑓‘𝑥) = 1o |
16 | 15, 8, 3 | wral 2448 |
. . . . . 6
wff
∀𝑥 ∈
𝑦 (𝑓‘𝑥) = 1o |
17 | 13, 16 | wo 703 |
. . . . 5
wff
(∃𝑥 ∈
𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o) |
18 | 7, 17 | wi 4 |
. . . 4
wff (𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)) |
19 | 18, 5 | wal 1346 |
. . 3
wff
∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)) |
20 | 19, 2 | cab 2156 |
. 2
class {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))} |
21 | 1, 20 | wceq 1348 |
1
wff Omni =
{𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))} |