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