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 e. CH
	pjoml2.2	|- B e. CH
Assertion	cmbr4i	|- ( A C_H B <-> ( A i^i ( ( _|_ ` A ) vH B ) ) C_ B )

Proof

Step	Hyp	Ref	Expression
1		pjoml2.1	|- A e. CH
2		pjoml2.2	|- B e. CH
3	1 2	cmbr3i	|- ( A C_H B <-> ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) )
4		inss2	|- ( A i^i B ) C_ B
5		sseq1	|- ( ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) -> ( ( A i^i ( ( _|_ ` A ) vH B ) ) C_ B <-> ( A i^i B ) C_ B ) )
6	4 5	mpbiri	|- ( ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) -> ( A i^i ( ( _|_ ` A ) vH B ) ) C_ B )
7		inss1	|- ( A i^i ( ( _|_ ` A ) vH B ) ) C_ A
8	7	jctl	|- ( ( A i^i ( ( _|_ ` A ) vH B ) ) C_ B -> ( ( A i^i ( ( _|_ ` A ) vH B ) ) C_ A /\ ( A i^i ( ( _|_ ` A ) vH B ) ) C_ B ) )
9		ssin	|- ( ( ( A i^i ( ( _|_ ` A ) vH B ) ) C_ A /\ ( A i^i ( ( _|_ ` A ) vH B ) ) C_ B ) <-> ( A i^i ( ( _|_ ` A ) vH B ) ) C_ ( A i^i B ) )
10	8 9	sylib	|- ( ( A i^i ( ( _|_ ` A ) vH B ) ) C_ B -> ( A i^i ( ( _|_ ` A ) vH B ) ) C_ ( A i^i B ) )
11	1	choccli	|- ( _|_ ` A ) e. CH
12	2 11	chub2i	|- B C_ ( ( _|_ ` A ) vH B )
13		sslin	|- ( B C_ ( ( _|_ ` A ) vH B ) -> ( A i^i B ) C_ ( A i^i ( ( _|_ ` A ) vH B ) ) )
14	12 13	ax-mp	|- ( A i^i B ) C_ ( A i^i ( ( _|_ ` A ) vH B ) )
15	10 14	jctir	|- ( ( A i^i ( ( _|_ ` A ) vH B ) ) C_ B -> ( ( A i^i ( ( _|_ ` A ) vH B ) ) C_ ( A i^i B ) /\ ( A i^i B ) C_ ( A i^i ( ( _|_ ` A ) vH B ) ) ) )
16		eqss	|- ( ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) <-> ( ( A i^i ( ( _|_ ` A ) vH B ) ) C_ ( A i^i B ) /\ ( A i^i B ) C_ ( A i^i ( ( _|_ ` A ) vH B ) ) ) )
17	15 16	sylibr	|- ( ( A i^i ( ( _|_ ` A ) vH B ) ) C_ B -> ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) )
18	6 17	impbii	|- ( ( A i^i ( ( _|_ ` A ) vH B ) ) = ( A i^i B ) <-> ( A i^i ( ( _|_ ` A ) vH B ) ) C_ B )
19	3 18	bitri	|- ( A C_H B <-> ( A i^i ( ( _|_ ` A ) vH B ) ) C_ B )