Metamath Proof Explorer

Theorem hlateq

Description: The equality of two Hilbert lattice elements is determined by the atoms under them. ( chrelat4i analog.) (Contributed by NM, 24-May-2012)

Ref Expression
Hypotheses hlatle.b ⊢ B = Base K
hlatle.l ⊢ ≤ ˙ = ≤ K
hlatle.a ⊢ A = Atoms ⁡ K
Assertion hlateq ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → ∀ p ∈ A p ≤ ˙ X ↔ p ≤ ˙ Y ↔ X = Y

Proof

Step Hyp Ref Expression
1 hlatle.b ⊢ B = Base K
2 hlatle.l ⊢ ≤ ˙ = ≤ K
3 hlatle.a ⊢ A = Atoms ⁡ K
4 1 2 3 hlatle ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ ∀ p ∈ A p ≤ ˙ X → p ≤ ˙ Y
5 1 2 3 hlatle ⊢ K ∈ HL ∧ Y ∈ B ∧ X ∈ B → Y ≤ ˙ X ↔ ∀ p ∈ A p ≤ ˙ Y → p ≤ ˙ X
6 5 3com23 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → Y ≤ ˙ X ↔ ∀ p ∈ A p ≤ ˙ Y → p ≤ ˙ X
7 4 6 anbi12d ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ∧ Y ≤ ˙ X ↔ ∀ p ∈ A p ≤ ˙ X → p ≤ ˙ Y ∧ ∀ p ∈ A p ≤ ˙ Y → p ≤ ˙ X
8 ralbiim ⊢ ∀ p ∈ A p ≤ ˙ X ↔ p ≤ ˙ Y ↔ ∀ p ∈ A p ≤ ˙ X → p ≤ ˙ Y ∧ ∀ p ∈ A p ≤ ˙ Y → p ≤ ˙ X
9 7 8 syl6rbbr ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → ∀ p ∈ A p ≤ ˙ X ↔ p ≤ ˙ Y ↔ X ≤ ˙ Y ∧ Y ≤ ˙ X
10 hllat ⊢ K ∈ HL → K ∈ Lat
11 1 2 latasymb ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ∧ Y ≤ ˙ X ↔ X = Y
12 10 11 syl3an1 ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ∧ Y ≤ ˙ X ↔ X = Y
13 9 12 bitrd ⊢ K ∈ HL ∧ X ∈ B ∧ Y ∈ B → ∀ p ∈ A p ≤ ˙ X ↔ p ≤ ˙ Y ↔ X = Y