Step | Hyp | Ref
| Expression |
1 | | fveq2 6767 |
. . . 4
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾)) |
2 | | isoml.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
3 | 1, 2 | eqtr4di 2796 |
. . 3
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵) |
4 | | fveq2 6767 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾)) |
5 | | isoml.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
6 | 4, 5 | eqtr4di 2796 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ ) |
7 | 6 | breqd 5085 |
. . . . 5
⊢ (𝑘 = 𝐾 → (𝑥(le‘𝑘)𝑦 ↔ 𝑥 ≤ 𝑦)) |
8 | | fveq2 6767 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾)) |
9 | | isoml.j |
. . . . . . . 8
⊢ ∨ =
(join‘𝐾) |
10 | 8, 9 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ ) |
11 | | eqidd 2739 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → 𝑥 = 𝑥) |
12 | | fveq2 6767 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = (meet‘𝐾)) |
13 | | isoml.m |
. . . . . . . . 9
⊢ ∧ =
(meet‘𝐾) |
14 | 12, 13 | eqtr4di 2796 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = ∧ ) |
15 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → 𝑦 = 𝑦) |
16 | | fveq2 6767 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (oc‘𝑘) = (oc‘𝐾)) |
17 | | isoml.o |
. . . . . . . . . 10
⊢ ⊥ =
(oc‘𝐾) |
18 | 16, 17 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (oc‘𝑘) = ⊥ ) |
19 | 18 | fveq1d 6769 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((oc‘𝑘)‘𝑥) = ( ⊥ ‘𝑥)) |
20 | 14, 15, 19 | oveq123d 7289 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)) = (𝑦 ∧ ( ⊥ ‘𝑥))) |
21 | 10, 11, 20 | oveq123d 7289 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥))) = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))) |
22 | 21 | eqeq2d 2749 |
. . . . 5
⊢ (𝑘 = 𝐾 → (𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥))) ↔ 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))) |
23 | 7, 22 | imbi12d 345 |
. . . 4
⊢ (𝑘 = 𝐾 → ((𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)))) ↔ (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))) |
24 | 3, 23 | raleqbidv 3334 |
. . 3
⊢ (𝑘 = 𝐾 → (∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)))) ↔ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))) |
25 | 3, 24 | raleqbidv 3334 |
. 2
⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))) |
26 | | df-oml 37179 |
. 2
⊢ OML =
{𝑘 ∈ OL ∣
∀𝑥 ∈
(Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥))))} |
27 | 25, 26 | elrab2 3627 |
1
⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))) |