Metamath Proof Explorer

Theorem mdbr2

Description: Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr . (Contributed by NM, 15-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion mdbr2 
|- ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdbr 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )
2 chub1 
 |-  ( ( x e. CH /\ A e. CH ) -> x C_ ( x vH A ) )
3 2 ancoms 
 |-  ( ( A e. CH /\ x e. CH ) -> x C_ ( x vH A ) )
4 iba 
 |-  ( x C_ B -> ( x C_ ( x vH A ) <-> ( x C_ ( x vH A ) /\ x C_ B ) ) )
5 ssin 
 |-  ( ( x C_ ( x vH A ) /\ x C_ B ) <-> x C_ ( ( x vH A ) i^i B ) )
6 4 5 bitrdi 
 |-  ( x C_ B -> ( x C_ ( x vH A ) <-> x C_ ( ( x vH A ) i^i B ) ) )
7 3 6 syl5ibcom 
 |-  ( ( A e. CH /\ x e. CH ) -> ( x C_ B -> x C_ ( ( x vH A ) i^i B ) ) )
8 chub2 
 |-  ( ( A e. CH /\ x e. CH ) -> A C_ ( x vH A ) )
9 8 ssrind 
 |-  ( ( A e. CH /\ x e. CH ) -> ( A i^i B ) C_ ( ( x vH A ) i^i B ) )
10 7 9 jctird 
 |-  ( ( A e. CH /\ x e. CH ) -> ( x C_ B -> ( x C_ ( ( x vH A ) i^i B ) /\ ( A i^i B ) C_ ( ( x vH A ) i^i B ) ) ) )
11 10 adantlr 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( x C_ B -> ( x C_ ( ( x vH A ) i^i B ) /\ ( A i^i B ) C_ ( ( x vH A ) i^i B ) ) ) )
12 simpr 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> x e. CH )
13 chincl 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A i^i B ) e. CH )
14 13 adantr 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( A i^i B ) e. CH )
15 chjcl 
 |-  ( ( x e. CH /\ A e. CH ) -> ( x vH A ) e. CH )
16 15 ancoms 
 |-  ( ( A e. CH /\ x e. CH ) -> ( x vH A ) e. CH )
17 chincl 
 |-  ( ( ( x vH A ) e. CH /\ B e. CH ) -> ( ( x vH A ) i^i B ) e. CH )
18 16 17 sylan 
 |-  ( ( ( A e. CH /\ x e. CH ) /\ B e. CH ) -> ( ( x vH A ) i^i B ) e. CH )
19 18 an32s 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( x vH A ) i^i B ) e. CH )
20 chlub 
 |-  ( ( x e. CH /\ ( A i^i B ) e. CH /\ ( ( x vH A ) i^i B ) e. CH ) -> ( ( x C_ ( ( x vH A ) i^i B ) /\ ( A i^i B ) C_ ( ( x vH A ) i^i B ) ) <-> ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) ) )
21 12 14 19 20 syl3anc 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( x C_ ( ( x vH A ) i^i B ) /\ ( A i^i B ) C_ ( ( x vH A ) i^i B ) ) <-> ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) ) )
22 11 21 sylibd 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( x C_ B -> ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) ) )
23 eqss 
 |-  ( ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) <-> ( ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) /\ ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) ) )
24 23 rbaib 
 |-  ( ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) -> ( ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) <-> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) )
25 22 24 syl6 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( x C_ B -> ( ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) <-> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) )
26 25 pm5.74d 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) <-> ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) )
27 26 ralbidva 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) )
28 1 27 bitrd 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) )