Step | Hyp | Ref
| Expression |
1 | | ltrnset.t |
. . 3
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
2 | | ltrnset.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
3 | | ltrnset.j |
. . . . 5
⊢ ∨ =
(join‘𝐾) |
4 | | ltrnset.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
5 | | ltrnset.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
6 | | ltrnset.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
7 | 2, 3, 4, 5, 6 | ltrnfset 38127 |
. . . 4
⊢ (𝐾 ∈ 𝐵 → (LTrn‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))})) |
8 | 7 | fveq1d 6773 |
. . 3
⊢ (𝐾 ∈ 𝐵 → ((LTrn‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))})‘𝑊)) |
9 | 1, 8 | eqtrid 2792 |
. 2
⊢ (𝐾 ∈ 𝐵 → 𝑇 = ((𝑤 ∈ 𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))})‘𝑊)) |
10 | | fveq2 6771 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((LDil‘𝐾)‘𝑤) = ((LDil‘𝐾)‘𝑊)) |
11 | | ltrnset.d |
. . . . 5
⊢ 𝐷 = ((LDil‘𝐾)‘𝑊) |
12 | 10, 11 | eqtr4di 2798 |
. . . 4
⊢ (𝑤 = 𝑊 → ((LDil‘𝐾)‘𝑤) = 𝐷) |
13 | | breq2 5083 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑝 ≤ 𝑤 ↔ 𝑝 ≤ 𝑊)) |
14 | 13 | notbid 318 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (¬ 𝑝 ≤ 𝑤 ↔ ¬ 𝑝 ≤ 𝑊)) |
15 | | breq2 5083 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑞 ≤ 𝑤 ↔ 𝑞 ≤ 𝑊)) |
16 | 15 | notbid 318 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (¬ 𝑞 ≤ 𝑤 ↔ ¬ 𝑞 ≤ 𝑊)) |
17 | 14, 16 | anbi12d 631 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) ↔ (¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊))) |
18 | | oveq2 7279 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊)) |
19 | | oveq2 7279 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑊)) |
20 | 18, 19 | eqeq12d 2756 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤) ↔ ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑊))) |
21 | 17, 20 | imbi12d 345 |
. . . . 5
⊢ (𝑤 = 𝑊 → (((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤)) ↔ ((¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑊)))) |
22 | 21 | 2ralbidv 3125 |
. . . 4
⊢ (𝑤 = 𝑊 → (∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤)) ↔ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑊)))) |
23 | 12, 22 | rabeqbidv 3419 |
. . 3
⊢ (𝑤 = 𝑊 → {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))} = {𝑓 ∈ 𝐷 ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑊))}) |
24 | | eqid 2740 |
. . 3
⊢ (𝑤 ∈ 𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))}) = (𝑤 ∈ 𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))}) |
25 | 11 | fvexi 6785 |
. . . 4
⊢ 𝐷 ∈ V |
26 | 25 | rabex 5260 |
. . 3
⊢ {𝑓 ∈ 𝐷 ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑊))} ∈ V |
27 | 23, 24, 26 | fvmpt 6872 |
. 2
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))})‘𝑊) = {𝑓 ∈ 𝐷 ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑊))}) |
28 | 9, 27 | sylan9eq 2800 |
1
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻) → 𝑇 = {𝑓 ∈ 𝐷 ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑊) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑊))}) |