| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6906 | . . . 4
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾)) | 
| 2 |  | isoml.b | . . . 4
⊢ 𝐵 = (Base‘𝐾) | 
| 3 | 1, 2 | eqtr4di 2795 | . . 3
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵) | 
| 4 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾)) | 
| 5 |  | isoml.l | . . . . . . 7
⊢  ≤ =
(le‘𝐾) | 
| 6 | 4, 5 | eqtr4di 2795 | . . . . . 6
⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ ) | 
| 7 | 6 | breqd 5154 | . . . . 5
⊢ (𝑘 = 𝐾 → (𝑥(le‘𝑘)𝑦 ↔ 𝑥 ≤ 𝑦)) | 
| 8 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾)) | 
| 9 |  | isoml.j | . . . . . . . 8
⊢  ∨ =
(join‘𝐾) | 
| 10 | 8, 9 | eqtr4di 2795 | . . . . . . 7
⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ ) | 
| 11 |  | eqidd 2738 | . . . . . . 7
⊢ (𝑘 = 𝐾 → 𝑥 = 𝑥) | 
| 12 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = (meet‘𝐾)) | 
| 13 |  | isoml.m | . . . . . . . . 9
⊢  ∧ =
(meet‘𝐾) | 
| 14 | 12, 13 | eqtr4di 2795 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = ∧ ) | 
| 15 |  | eqidd 2738 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → 𝑦 = 𝑦) | 
| 16 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (oc‘𝑘) = (oc‘𝐾)) | 
| 17 |  | isoml.o | . . . . . . . . . 10
⊢  ⊥ =
(oc‘𝐾) | 
| 18 | 16, 17 | eqtr4di 2795 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → (oc‘𝑘) = ⊥ ) | 
| 19 | 18 | fveq1d 6908 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → ((oc‘𝑘)‘𝑥) = ( ⊥ ‘𝑥)) | 
| 20 | 14, 15, 19 | oveq123d 7452 | . . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)) = (𝑦 ∧ ( ⊥ ‘𝑥))) | 
| 21 | 10, 11, 20 | oveq123d 7452 | . . . . . 6
⊢ (𝑘 = 𝐾 → (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥))) = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))) | 
| 22 | 21 | eqeq2d 2748 | . . . . 5
⊢ (𝑘 = 𝐾 → (𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥))) ↔ 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))) | 
| 23 | 7, 22 | imbi12d 344 | . . . 4
⊢ (𝑘 = 𝐾 → ((𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)))) ↔ (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))) | 
| 24 | 3, 23 | raleqbidv 3346 | . . 3
⊢ (𝑘 = 𝐾 → (∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)))) ↔ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))) | 
| 25 | 3, 24 | raleqbidv 3346 | . 2
⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))) | 
| 26 |  | df-oml 39180 | . 2
⊢ OML =
{𝑘 ∈ OL ∣
∀𝑥 ∈
(Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥))))} | 
| 27 | 25, 26 | elrab2 3695 | 1
⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))) |