Detailed syntax breakdown of Definition df-cfilu
Step | Hyp | Ref
| Expression |
1 | | ccfilu 23382 |
. 2
class
CauFilu |
2 | | vu |
. . 3
setvar 𝑢 |
3 | | cust 23295 |
. . . . 5
class
UnifOn |
4 | 3 | crn 5586 |
. . . 4
class ran
UnifOn |
5 | 4 | cuni 4841 |
. . 3
class ∪ ran UnifOn |
6 | | va |
. . . . . . . . 9
setvar 𝑎 |
7 | 6 | cv 1538 |
. . . . . . . 8
class 𝑎 |
8 | 7, 7 | cxp 5583 |
. . . . . . 7
class (𝑎 × 𝑎) |
9 | | vv |
. . . . . . . 8
setvar 𝑣 |
10 | 9 | cv 1538 |
. . . . . . 7
class 𝑣 |
11 | 8, 10 | wss 3888 |
. . . . . 6
wff (𝑎 × 𝑎) ⊆ 𝑣 |
12 | | vf |
. . . . . . 7
setvar 𝑓 |
13 | 12 | cv 1538 |
. . . . . 6
class 𝑓 |
14 | 11, 6, 13 | wrex 3063 |
. . . . 5
wff
∃𝑎 ∈
𝑓 (𝑎 × 𝑎) ⊆ 𝑣 |
15 | 2 | cv 1538 |
. . . . 5
class 𝑢 |
16 | 14, 9, 15 | wral 3062 |
. . . 4
wff
∀𝑣 ∈
𝑢 ∃𝑎 ∈ 𝑓 (𝑎 × 𝑎) ⊆ 𝑣 |
17 | 15 | cuni 4841 |
. . . . . 6
class ∪ 𝑢 |
18 | 17 | cdm 5585 |
. . . . 5
class dom ∪ 𝑢 |
19 | | cfbas 20529 |
. . . . 5
class
fBas |
20 | 18, 19 | cfv 6423 |
. . . 4
class
(fBas‘dom ∪ 𝑢) |
21 | 16, 12, 20 | crab 3066 |
. . 3
class {𝑓 ∈ (fBas‘dom ∪ 𝑢)
∣ ∀𝑣 ∈
𝑢 ∃𝑎 ∈ 𝑓 (𝑎 × 𝑎) ⊆ 𝑣} |
22 | 2, 5, 21 | cmpt 5158 |
. 2
class (𝑢 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (fBas‘dom ∪ 𝑢)
∣ ∀𝑣 ∈
𝑢 ∃𝑎 ∈ 𝑓 (𝑎 × 𝑎) ⊆ 𝑣}) |
23 | 1, 22 | wceq 1539 |
1
wff
CauFilu = (𝑢 ∈ ∪ ran
UnifOn ↦ {𝑓 ∈
(fBas‘dom ∪ 𝑢) ∣ ∀𝑣 ∈ 𝑢 ∃𝑎 ∈ 𝑓 (𝑎 × 𝑎) ⊆ 𝑣}) |