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

Metamath Proof Explorer

Theorem chdmm1i

Description: De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 ⊢ 𝐴 ∈ Cℋ
chjcl.2 ⊢ 𝐵 ∈ Cℋ
Assertion chdmm1i ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ch0le.1 ⊢ 𝐴 ∈ Cℋ
2 chjcl.2 ⊢ 𝐵 ∈ Cℋ
3 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
4 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
5 3 4 chub1i ⊢ ( ⊥ ‘ 𝐴 ) ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) )
6 3 4 chjcli ⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
7 1 6 chsscon1i ⊢ ( ( ⊥ ‘ 𝐴 ) ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ↔ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ 𝐴 )
8 5 7 mpbi ⊢ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ 𝐴
9 4 3 chub2i ⊢ ( ⊥ ‘ 𝐵 ) ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) )
10 2 6 chsscon1i ⊢ ( ( ⊥ ‘ 𝐵 ) ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ↔ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ 𝐵 )
11 9 10 mpbi ⊢ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ 𝐵
12 8 11 ssini ⊢ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ ( 𝐴 ∩ 𝐵 )
13 1 2 chincli ⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
14 6 13 chsscon1i ⊢ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ ( 𝐴 ∩ 𝐵 ) ↔ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) )
15 12 14 mpbi ⊢ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) )
16 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
17 13 1 chsscon3i ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ↔ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) )
18 16 17 mpbi ⊢ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) )
19 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
20 13 2 chsscon3i ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) )
21 19 20 mpbi ⊢ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) )
22 13 choccli ⊢ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ
23 3 4 22 chlubii ⊢ ( ( ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ⊆ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) )
24 18 21 23 mp2an ⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ⊆ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) )
25 15 24 eqssi ⊢ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) )