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	⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) ⊆ 𝐵 )