Metamath Proof Explorer


Theorem lejdii

Description: An ortholattice is distributive in one ordering direction (join version). (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses ledi.1 𝐴C
ledi.2 𝐵C
ledi.3 𝐶C
Assertion lejdii ( 𝐴 ( 𝐵𝐶 ) ) ⊆ ( ( 𝐴 𝐵 ) ∩ ( 𝐴 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ledi.1 𝐴C
2 ledi.2 𝐵C
3 ledi.3 𝐶C
4 1 2 chub1i 𝐴 ⊆ ( 𝐴 𝐵 )
5 1 3 chub1i 𝐴 ⊆ ( 𝐴 𝐶 )
6 4 5 ssini 𝐴 ⊆ ( ( 𝐴 𝐵 ) ∩ ( 𝐴 𝐶 ) )
7 inss1 ( 𝐵𝐶 ) ⊆ 𝐵
8 2 1 chub2i 𝐵 ⊆ ( 𝐴 𝐵 )
9 7 8 sstri ( 𝐵𝐶 ) ⊆ ( 𝐴 𝐵 )
10 inss2 ( 𝐵𝐶 ) ⊆ 𝐶
11 3 1 chub2i 𝐶 ⊆ ( 𝐴 𝐶 )
12 10 11 sstri ( 𝐵𝐶 ) ⊆ ( 𝐴 𝐶 )
13 9 12 ssini ( 𝐵𝐶 ) ⊆ ( ( 𝐴 𝐵 ) ∩ ( 𝐴 𝐶 ) )
14 2 3 chincli ( 𝐵𝐶 ) ∈ C
15 1 2 chjcli ( 𝐴 𝐵 ) ∈ C
16 1 3 chjcli ( 𝐴 𝐶 ) ∈ C
17 15 16 chincli ( ( 𝐴 𝐵 ) ∩ ( 𝐴 𝐶 ) ) ∈ C
18 1 14 17 chlubi ( ( 𝐴 ⊆ ( ( 𝐴 𝐵 ) ∩ ( 𝐴 𝐶 ) ) ∧ ( 𝐵𝐶 ) ⊆ ( ( 𝐴 𝐵 ) ∩ ( 𝐴 𝐶 ) ) ) ↔ ( 𝐴 ( 𝐵𝐶 ) ) ⊆ ( ( 𝐴 𝐵 ) ∩ ( 𝐴 𝐶 ) ) )
19 18 bicomi ( ( 𝐴 ( 𝐵𝐶 ) ) ⊆ ( ( 𝐴 𝐵 ) ∩ ( 𝐴 𝐶 ) ) ↔ ( 𝐴 ⊆ ( ( 𝐴 𝐵 ) ∩ ( 𝐴 𝐶 ) ) ∧ ( 𝐵𝐶 ) ⊆ ( ( 𝐴 𝐵 ) ∩ ( 𝐴 𝐶 ) ) ) )
20 6 13 19 mpbir2an ( 𝐴 ( 𝐵𝐶 ) ) ⊆ ( ( 𝐴 𝐵 ) ∩ ( 𝐴 𝐶 ) )