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

Metamath Proof Explorer

Theorem cmbr4i

Description: Alternate definition for the commutes relation. (Contributed by NM, 6-Dec-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 ⊢ 𝐴 ∈ Cℋ
pjoml2.2 ⊢ 𝐵 ∈ Cℋ
Assertion cmbr4i ( 𝐴 𝐶ℋ 𝐵 ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 pjoml2.1 ⊢ 𝐴 ∈ Cℋ
2 pjoml2.2 ⊢ 𝐵 ∈ Cℋ
3 1 2 cmbr3i ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) )
4 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
5 sseq1 ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) → ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ) )
6 4 5 mpbiri ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐵 )
7 inss1 ⊢ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐴
8 7 jctl ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐵 → ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐴 ∧ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐵 ) )
9 ssin ⊢ ( ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐴 ∧ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐵 ) ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∩ 𝐵 ) )
10 8 9 sylib ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐵 → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∩ 𝐵 ) )
11 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
12 2 11 chub2i ⊢ 𝐵 ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 )
13 sslin ⊢ ( 𝐵 ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) )
14 12 13 ax-mp ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) )
15 10 14 jctir ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐵 → ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
16 eqss ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) ↔ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
17 15 16 sylibr ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐵 → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) )
18 6 17 impbii ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐵 )
19 3 18 bitri ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐵 )