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