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 ⊢ A ∈ C ℋ
pjoml2.2 ⊢ B ∈ C ℋ
Assertion cmbr4i ⊢ A 𝐶 ℋ B ↔ A ∩ ⊥ ⁡ A ∨ ℋ B ⊆ B

Proof

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