Detailed syntax breakdown of Definition df-ltrn
Step | Hyp | Ref
| Expression |
1 | | cltrn 37852 |
. 2
class
LTrn |
2 | | vk |
. . 3
setvar 𝑘 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | vw |
. . . 4
setvar 𝑤 |
5 | 2 | cv 1542 |
. . . . 5
class 𝑘 |
6 | | clh 37735 |
. . . . 5
class
LHyp |
7 | 5, 6 | cfv 6380 |
. . . 4
class
(LHyp‘𝑘) |
8 | | vp |
. . . . . . . . . . . 12
setvar 𝑝 |
9 | 8 | cv 1542 |
. . . . . . . . . . 11
class 𝑝 |
10 | 4 | cv 1542 |
. . . . . . . . . . 11
class 𝑤 |
11 | | cple 16809 |
. . . . . . . . . . . 12
class
le |
12 | 5, 11 | cfv 6380 |
. . . . . . . . . . 11
class
(le‘𝑘) |
13 | 9, 10, 12 | wbr 5053 |
. . . . . . . . . 10
wff 𝑝(le‘𝑘)𝑤 |
14 | 13 | wn 3 |
. . . . . . . . 9
wff ¬
𝑝(le‘𝑘)𝑤 |
15 | | vq |
. . . . . . . . . . . 12
setvar 𝑞 |
16 | 15 | cv 1542 |
. . . . . . . . . . 11
class 𝑞 |
17 | 16, 10, 12 | wbr 5053 |
. . . . . . . . . 10
wff 𝑞(le‘𝑘)𝑤 |
18 | 17 | wn 3 |
. . . . . . . . 9
wff ¬
𝑞(le‘𝑘)𝑤 |
19 | 14, 18 | wa 399 |
. . . . . . . 8
wff (¬
𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) |
20 | | vf |
. . . . . . . . . . . . 13
setvar 𝑓 |
21 | 20 | cv 1542 |
. . . . . . . . . . . 12
class 𝑓 |
22 | 9, 21 | cfv 6380 |
. . . . . . . . . . 11
class (𝑓‘𝑝) |
23 | | cjn 17818 |
. . . . . . . . . . . 12
class
join |
24 | 5, 23 | cfv 6380 |
. . . . . . . . . . 11
class
(join‘𝑘) |
25 | 9, 22, 24 | co 7213 |
. . . . . . . . . 10
class (𝑝(join‘𝑘)(𝑓‘𝑝)) |
26 | | cmee 17819 |
. . . . . . . . . . 11
class
meet |
27 | 5, 26 | cfv 6380 |
. . . . . . . . . 10
class
(meet‘𝑘) |
28 | 25, 10, 27 | co 7213 |
. . . . . . . . 9
class ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) |
29 | 16, 21 | cfv 6380 |
. . . . . . . . . . 11
class (𝑓‘𝑞) |
30 | 16, 29, 24 | co 7213 |
. . . . . . . . . 10
class (𝑞(join‘𝑘)(𝑓‘𝑞)) |
31 | 30, 10, 27 | co 7213 |
. . . . . . . . 9
class ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤) |
32 | 28, 31 | wceq 1543 |
. . . . . . . 8
wff ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤) |
33 | 19, 32 | wi 4 |
. . . . . . 7
wff ((¬
𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤)) |
34 | | catm 37014 |
. . . . . . . 8
class
Atoms |
35 | 5, 34 | cfv 6380 |
. . . . . . 7
class
(Atoms‘𝑘) |
36 | 33, 15, 35 | wral 3061 |
. . . . . 6
wff
∀𝑞 ∈
(Atoms‘𝑘)((¬
𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤)) |
37 | 36, 8, 35 | wral 3061 |
. . . . 5
wff
∀𝑝 ∈
(Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤)) |
38 | | cldil 37851 |
. . . . . . 7
class
LDil |
39 | 5, 38 | cfv 6380 |
. . . . . 6
class
(LDil‘𝑘) |
40 | 10, 39 | cfv 6380 |
. . . . 5
class
((LDil‘𝑘)‘𝑤) |
41 | 37, 20, 40 | crab 3065 |
. . . 4
class {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))} |
42 | 4, 7, 41 | cmpt 5135 |
. . 3
class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))}) |
43 | 2, 3, 42 | cmpt 5135 |
. 2
class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))})) |
44 | 1, 43 | wceq 1543 |
1
wff LTrn =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))})) |