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 ∧ 𝑋𝐵𝑌𝐵 ) → ( ∀ 𝑝𝐴 ( 𝑝 𝑋𝑝 𝑌 ) ↔ 𝑋 = 𝑌 ) )