Metamath Proof Explorer

Theorem mdsl2bi

Description: If the modular pair property holds in a sublattice, it holds in the whole lattice. Lemma 1.4 of MaedaMaeda p. 2. (Contributed by NM, 24-Dec-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mdsl.1 
|- A e. CH
mdsl.2 
|- B e. CH
Assertion mdsl2bi 
|- ( A MH B <-> A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) )

Proof

Step Hyp Ref Expression
1 mdsl.1 
 |-  A e. CH
2 mdsl.2 
 |-  B e. CH
3 1 2 mdsl2i 
 |-  ( A MH B <-> A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) )
4 1 2 chincli 
 |-  ( A i^i B ) e. CH
5 inss1 
 |-  ( A i^i B ) C_ A
6 chlej2 
 |-  ( ( ( ( A i^i B ) e. CH /\ A e. CH /\ x e. CH ) /\ ( A i^i B ) C_ A ) -> ( x vH ( A i^i B ) ) C_ ( x vH A ) )
7 5 6 mpan2 
 |-  ( ( ( A i^i B ) e. CH /\ A e. CH /\ x e. CH ) -> ( x vH ( A i^i B ) ) C_ ( x vH A ) )
8 4 1 7 mp3an12 
 |-  ( x e. CH -> ( x vH ( A i^i B ) ) C_ ( x vH A ) )
9 8 adantr 
 |-  ( ( x e. CH /\ x C_ B ) -> ( x vH ( A i^i B ) ) C_ ( x vH A ) )
10 simpr 
 |-  ( ( x e. CH /\ x C_ B ) -> x C_ B )
11 inss2 
 |-  ( A i^i B ) C_ B
12 10 11 jctir 
 |-  ( ( x e. CH /\ x C_ B ) -> ( x C_ B /\ ( A i^i B ) C_ B ) )
13 chlub 
 |-  ( ( x e. CH /\ ( A i^i B ) e. CH /\ B e. CH ) -> ( ( x C_ B /\ ( A i^i B ) C_ B ) <-> ( x vH ( A i^i B ) ) C_ B ) )
14 4 2 13 mp3an23 
 |-  ( x e. CH -> ( ( x C_ B /\ ( A i^i B ) C_ B ) <-> ( x vH ( A i^i B ) ) C_ B ) )
15 14 adantr 
 |-  ( ( x e. CH /\ x C_ B ) -> ( ( x C_ B /\ ( A i^i B ) C_ B ) <-> ( x vH ( A i^i B ) ) C_ B ) )
16 12 15 mpbid 
 |-  ( ( x e. CH /\ x C_ B ) -> ( x vH ( A i^i B ) ) C_ B )
17 9 16 ssind 
 |-  ( ( x e. CH /\ x C_ B ) -> ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) )
18 17 biantrud 
 |-  ( ( x e. CH /\ x C_ 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 ) ) /\ ( x vH ( A i^i B ) ) C_ ( ( x vH A ) i^i B ) ) ) )
19 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 ) ) )
20 18 19 bitr4di 
 |-  ( ( x e. CH /\ x C_ B ) -> ( ( ( 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 ) ) ) )
21 20 ex 
 |-  ( x e. CH -> ( x C_ B -> ( ( ( 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 ) ) ) ) )
22 21 adantld 
 |-  ( x e. CH -> ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( ( 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 ) ) ) ) )
23 22 pm5.74d 
 |-  ( x e. CH -> ( ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) C_ ( x vH ( 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 ) ) ) ) )
24 23 ralbiia 
 |-  ( A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) <-> A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) )
25 3 24 bitri 
 |-  ( A MH B <-> A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) )