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

Metamath Proof Explorer

Theorem chabs2

Description: Hilbert lattice absorption law. From definition of lattice in Kalmbach p. 14. (Contributed by NM, 16-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	chabs2	⊢ ( ( 𝐴 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → ( 𝐴 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		chub1	⊢ ( ( 𝐴 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → 𝐴 ⊆ ( 𝐴 ∨_ℋ 𝐵 ) )
2		ssid	⊢ 𝐴 ⊆ 𝐴
3	1 2	jctil	⊢ ( ( 𝐴 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → ( 𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐴 ∨_ℋ 𝐵 ) ) )
4		ssin	⊢ ( ( 𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐴 ∨_ℋ 𝐵 ) ) ↔ 𝐴 ⊆ ( 𝐴 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) )
5	3 4	sylib	⊢ ( ( 𝐴 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → 𝐴 ⊆ ( 𝐴 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) )
6		inss1	⊢ ( 𝐴 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ 𝐴
7	5 6	jctil	⊢ ( ( 𝐴 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → ( ( 𝐴 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐴 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ) )
8		eqss	⊢ ( ( 𝐴 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) = 𝐴 ↔ ( ( 𝐴 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐴 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ) )
9	7 8	sylibr	⊢ ( ( 𝐴 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → ( 𝐴 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) = 𝐴 )