Metamath Proof Explorer


Theorem cvmdi

Description: The covering property implies the modular pair property. Lemma 7.5.1 of MaedaMaeda p. 31. (Contributed by NM, 16-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdsl.1
|- A e. CH
mdsl.2
|- B e. CH
Assertion cvmdi
|- ( ( A i^i B )  A MH B )

Proof

Step Hyp Ref Expression
1 mdsl.1
 |-  A e. CH
2 mdsl.2
 |-  B e. CH
3 anass
 |-  ( ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) /\ x C_ B ) <-> ( ( A i^i B ) C_ x /\ ( x C_ ( A vH B ) /\ x C_ B ) ) )
4 2 1 chub2i
 |-  B C_ ( A vH B )
5 sstr
 |-  ( ( x C_ B /\ B C_ ( A vH B ) ) -> x C_ ( A vH B ) )
6 4 5 mpan2
 |-  ( x C_ B -> x C_ ( A vH B ) )
7 6 pm4.71ri
 |-  ( x C_ B <-> ( x C_ ( A vH B ) /\ x C_ B ) )
8 7 anbi2i
 |-  ( ( ( A i^i B ) C_ x /\ x C_ B ) <-> ( ( A i^i B ) C_ x /\ ( x C_ ( A vH B ) /\ x C_ B ) ) )
9 3 8 bitr4i
 |-  ( ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) /\ x C_ B ) <-> ( ( A i^i B ) C_ x /\ x C_ B ) )
10 1 2 chincli
 |-  ( A i^i B ) e. CH
11 cvnbtwn4
 |-  ( ( ( A i^i B ) e. CH /\ B e. CH /\ x e. CH ) -> ( ( A i^i B )  ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( x = ( A i^i B ) \/ x = B ) ) ) )
12 10 2 11 mp3an12
 |-  ( x e. CH -> ( ( A i^i B )  ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( x = ( A i^i B ) \/ x = B ) ) ) )
13 12 impcom
 |-  ( ( ( A i^i B )  ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( x = ( A i^i B ) \/ x = B ) ) )
14 10 1 chjcomi
 |-  ( ( A i^i B ) vH A ) = ( A vH ( A i^i B ) )
15 1 2 chabs1i
 |-  ( A vH ( A i^i B ) ) = A
16 14 15 eqtri
 |-  ( ( A i^i B ) vH A ) = A
17 16 ineq1i
 |-  ( ( ( A i^i B ) vH A ) i^i B ) = ( A i^i B )
18 10 chjidmi
 |-  ( ( A i^i B ) vH ( A i^i B ) ) = ( A i^i B )
19 17 18 eqtr4i
 |-  ( ( ( A i^i B ) vH A ) i^i B ) = ( ( A i^i B ) vH ( A i^i B ) )
20 oveq1
 |-  ( x = ( A i^i B ) -> ( x vH A ) = ( ( A i^i B ) vH A ) )
21 20 ineq1d
 |-  ( x = ( A i^i B ) -> ( ( x vH A ) i^i B ) = ( ( ( A i^i B ) vH A ) i^i B ) )
22 oveq1
 |-  ( x = ( A i^i B ) -> ( x vH ( A i^i B ) ) = ( ( A i^i B ) vH ( A i^i B ) ) )
23 19 21 22 3eqtr4a
 |-  ( x = ( A i^i B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) )
24 incom
 |-  ( ( B vH A ) i^i B ) = ( B i^i ( B vH A ) )
25 2 1 chabs2i
 |-  ( B i^i ( B vH A ) ) = B
26 2 1 chabs1i
 |-  ( B vH ( B i^i A ) ) = B
27 incom
 |-  ( B i^i A ) = ( A i^i B )
28 27 oveq2i
 |-  ( B vH ( B i^i A ) ) = ( B vH ( A i^i B ) )
29 25 26 28 3eqtr2i
 |-  ( B i^i ( B vH A ) ) = ( B vH ( A i^i B ) )
30 24 29 eqtri
 |-  ( ( B vH A ) i^i B ) = ( B vH ( A i^i B ) )
31 oveq1
 |-  ( x = B -> ( x vH A ) = ( B vH A ) )
32 31 ineq1d
 |-  ( x = B -> ( ( x vH A ) i^i B ) = ( ( B vH A ) i^i B ) )
33 oveq1
 |-  ( x = B -> ( x vH ( A i^i B ) ) = ( B vH ( A i^i B ) ) )
34 30 32 33 3eqtr4a
 |-  ( x = B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) )
35 23 34 jaoi
 |-  ( ( x = ( A i^i B ) \/ x = B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) )
36 13 35 syl6
 |-  ( ( ( A i^i B )  ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) )
37 9 36 syl5bi
 |-  ( ( ( A i^i B )  ( ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) /\ x C_ B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) )
38 37 exp4b
 |-  ( ( A i^i B )  ( x e. CH -> ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) -> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) ) )
39 38 ralrimiv
 |-  ( ( A i^i B )  A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) -> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )
40 1 2 mdsl1i
 |-  ( A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) -> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) <-> A MH B )
41 39 40 sylib
 |-  ( ( A i^i B )  A MH B )