This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
hlatle.l ⊢ ≤ = ( le ‘ 𝐾 )
hlatle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion hlateq ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 ↔ 𝑝 ≤ 𝑌 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 hlatle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 hlatle.l ⊢ ≤ = ( le ‘ 𝐾 )
3 hlatle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 ralbiim ⊢ ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 ↔ 𝑝 ≤ 𝑌 ) ↔ ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑌 → 𝑝 ≤ 𝑋 ) ) )
5 1 2 3 hlatle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ) )
6 1 2 3 hlatle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 ≤ 𝑋 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑌 → 𝑝 ≤ 𝑋 ) ) )
7 6 3com23 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ≤ 𝑋 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑌 → 𝑝 ≤ 𝑋 ) ) )
8 5 7 anbi12d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ↔ ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑌 → 𝑝 ≤ 𝑋 ) ) ) )
9 4 8 bitr4id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 ↔ 𝑝 ≤ 𝑌 ) ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ) )
10 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
11 1 2 latasymb ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ↔ 𝑋 = 𝑌 ) )
12 10 11 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ↔ 𝑋 = 𝑌 ) )
13 9 12 bitrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 ↔ 𝑝 ≤ 𝑌 ) ↔ 𝑋 = 𝑌 ) )