Detailed syntax breakdown of Definition df-trcl
Step | Hyp | Ref
| Expression |
1 | | ctcl 14694 |
. 2
class
t+ |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cvv 3431 |
. . 3
class
V |
4 | 2 | cv 1541 |
. . . . . . 7
class 𝑥 |
5 | | vz |
. . . . . . . 8
setvar 𝑧 |
6 | 5 | cv 1541 |
. . . . . . 7
class 𝑧 |
7 | 4, 6 | wss 3892 |
. . . . . 6
wff 𝑥 ⊆ 𝑧 |
8 | 6, 6 | ccom 5594 |
. . . . . . 7
class (𝑧 ∘ 𝑧) |
9 | 8, 6 | wss 3892 |
. . . . . 6
wff (𝑧 ∘ 𝑧) ⊆ 𝑧 |
10 | 7, 9 | wa 396 |
. . . . 5
wff (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) |
11 | 10, 5 | cab 2717 |
. . . 4
class {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} |
12 | 11 | cint 4885 |
. . 3
class ∩ {𝑧
∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} |
13 | 2, 3, 12 | cmpt 5162 |
. 2
class (𝑥 ∈ V ↦ ∩ {𝑧
∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |
14 | 1, 13 | wceq 1542 |
1
wff t+ = (𝑥 ∈ V ↦ ∩ {𝑧
∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |