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 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 )