Detailed syntax breakdown of Definition df-locfin
Step | Hyp | Ref
| Expression |
1 | | clocfin 22258 |
. 2
class
LocFin |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | ctop 21647 |
. . 3
class
Top |
4 | 2 | cv 1541 |
. . . . . . 7
class 𝑥 |
5 | 4 | cuni 4797 |
. . . . . 6
class ∪ 𝑥 |
6 | | vy |
. . . . . . . 8
setvar 𝑦 |
7 | 6 | cv 1541 |
. . . . . . 7
class 𝑦 |
8 | 7 | cuni 4797 |
. . . . . 6
class ∪ 𝑦 |
9 | 5, 8 | wceq 1542 |
. . . . 5
wff ∪ 𝑥 =
∪ 𝑦 |
10 | | vp |
. . . . . . . . 9
setvar 𝑝 |
11 | | vn |
. . . . . . . . 9
setvar 𝑛 |
12 | 10, 11 | wel 2115 |
. . . . . . . 8
wff 𝑝 ∈ 𝑛 |
13 | | vs |
. . . . . . . . . . . . 13
setvar 𝑠 |
14 | 13 | cv 1541 |
. . . . . . . . . . . 12
class 𝑠 |
15 | 11 | cv 1541 |
. . . . . . . . . . . 12
class 𝑛 |
16 | 14, 15 | cin 3843 |
. . . . . . . . . . 11
class (𝑠 ∩ 𝑛) |
17 | | c0 4212 |
. . . . . . . . . . 11
class
∅ |
18 | 16, 17 | wne 2935 |
. . . . . . . . . 10
wff (𝑠 ∩ 𝑛) ≠ ∅ |
19 | 18, 13, 7 | crab 3058 |
. . . . . . . . 9
class {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} |
20 | | cfn 8558 |
. . . . . . . . 9
class
Fin |
21 | 19, 20 | wcel 2114 |
. . . . . . . 8
wff {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin |
22 | 12, 21 | wa 399 |
. . . . . . 7
wff (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
23 | 22, 11, 4 | wrex 3055 |
. . . . . 6
wff
∃𝑛 ∈
𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
24 | 23, 10, 5 | wral 3054 |
. . . . 5
wff
∀𝑝 ∈
∪ 𝑥∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
25 | 9, 24 | wa 399 |
. . . 4
wff (∪ 𝑥 =
∪ 𝑦 ∧ ∀𝑝 ∈ ∪ 𝑥∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
26 | 25, 6 | cab 2717 |
. . 3
class {𝑦 ∣ (∪ 𝑥 =
∪ 𝑦 ∧ ∀𝑝 ∈ ∪ 𝑥∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))} |
27 | 2, 3, 26 | cmpt 5111 |
. 2
class (𝑥 ∈ Top ↦ {𝑦 ∣ (∪ 𝑥 =
∪ 𝑦 ∧ ∀𝑝 ∈ ∪ 𝑥∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))}) |
28 | 1, 27 | wceq 1542 |
1
wff LocFin =
(𝑥 ∈ Top ↦
{𝑦 ∣ (∪ 𝑥 =
∪ 𝑦 ∧ ∀𝑝 ∈ ∪ 𝑥∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))}) |