Detailed syntax breakdown of Definition df-trnN
Step | Hyp | Ref
| Expression |
1 | | ctrnN 38113 |
. 2
class
Trn |
2 | | vk |
. . 3
setvar 𝑘 |
3 | | cvv 3431 |
. . 3
class
V |
4 | | vd |
. . . 4
setvar 𝑑 |
5 | 2 | cv 1541 |
. . . . 5
class 𝑘 |
6 | | catm 37273 |
. . . . 5
class
Atoms |
7 | 5, 6 | cfv 6432 |
. . . 4
class
(Atoms‘𝑘) |
8 | | vq |
. . . . . . . . . . 11
setvar 𝑞 |
9 | 8 | cv 1541 |
. . . . . . . . . 10
class 𝑞 |
10 | | vf |
. . . . . . . . . . . 12
setvar 𝑓 |
11 | 10 | cv 1541 |
. . . . . . . . . . 11
class 𝑓 |
12 | 9, 11 | cfv 6432 |
. . . . . . . . . 10
class (𝑓‘𝑞) |
13 | | cpadd 37805 |
. . . . . . . . . . 11
class
+𝑃 |
14 | 5, 13 | cfv 6432 |
. . . . . . . . . 10
class
(+𝑃‘𝑘) |
15 | 9, 12, 14 | co 7271 |
. . . . . . . . 9
class (𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) |
16 | 4 | cv 1541 |
. . . . . . . . . . 11
class 𝑑 |
17 | 16 | csn 4567 |
. . . . . . . . . 10
class {𝑑} |
18 | | cpolN 37912 |
. . . . . . . . . . 11
class
⊥𝑃 |
19 | 5, 18 | cfv 6432 |
. . . . . . . . . 10
class
(⊥𝑃‘𝑘) |
20 | 17, 19 | cfv 6432 |
. . . . . . . . 9
class
((⊥𝑃‘𝑘)‘{𝑑}) |
21 | 15, 20 | cin 3891 |
. . . . . . . 8
class ((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) |
22 | | vr |
. . . . . . . . . . 11
setvar 𝑟 |
23 | 22 | cv 1541 |
. . . . . . . . . 10
class 𝑟 |
24 | 23, 11 | cfv 6432 |
. . . . . . . . . 10
class (𝑓‘𝑟) |
25 | 23, 24, 14 | co 7271 |
. . . . . . . . 9
class (𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) |
26 | 25, 20 | cin 3891 |
. . . . . . . 8
class ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) |
27 | 21, 26 | wceq 1542 |
. . . . . . 7
wff ((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) |
28 | | cwpointsN 37996 |
. . . . . . . . 9
class
WAtoms |
29 | 5, 28 | cfv 6432 |
. . . . . . . 8
class
(WAtoms‘𝑘) |
30 | 16, 29 | cfv 6432 |
. . . . . . 7
class
((WAtoms‘𝑘)‘𝑑) |
31 | 27, 22, 30 | wral 3066 |
. . . . . 6
wff
∀𝑟 ∈
((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) |
32 | 31, 8, 30 | wral 3066 |
. . . . 5
wff
∀𝑞 ∈
((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) |
33 | | cdilN 38112 |
. . . . . . 7
class
Dil |
34 | 5, 33 | cfv 6432 |
. . . . . 6
class
(Dil‘𝑘) |
35 | 16, 34 | cfv 6432 |
. . . . 5
class
((Dil‘𝑘)‘𝑑) |
36 | 32, 10, 35 | crab 3070 |
. . . 4
class {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑}))} |
37 | 4, 7, 36 | cmpt 5162 |
. . 3
class (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑}))}) |
38 | 2, 3, 37 | cmpt 5162 |
. 2
class (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑}))})) |
39 | 1, 38 | wceq 1542 |
1
wff Trn =
(𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑}))})) |