Metamath Proof Explorer

Theorem dmdbr4

Description: Binary relation expressing the dual modular pair property. This version quantifies an ordering instead of an inference. (Contributed by NM, 6-Jul-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dmdbr2 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> A. y e. CH ( B C_ y -> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) ) )
2 chub2 
 |-  ( ( B e. CH /\ x e. CH ) -> B C_ ( x vH B ) )
3 2 ancoms 
 |-  ( ( x e. CH /\ B e. CH ) -> B C_ ( x vH B ) )
4 chjcl 
 |-  ( ( x e. CH /\ B e. CH ) -> ( x vH B ) e. CH )
5 sseq2 
 |-  ( y = ( x vH B ) -> ( B C_ y <-> B C_ ( x vH B ) ) )
6 ineq1 
 |-  ( y = ( x vH B ) -> ( y i^i ( A vH B ) ) = ( ( x vH B ) i^i ( A vH B ) ) )
7 ineq1 
 |-  ( y = ( x vH B ) -> ( y i^i A ) = ( ( x vH B ) i^i A ) )
8 7 oveq1d 
 |-  ( y = ( x vH B ) -> ( ( y i^i A ) vH B ) = ( ( ( x vH B ) i^i A ) vH B ) )
9 6 8 sseq12d 
 |-  ( y = ( x vH B ) -> ( ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) <-> ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
10 5 9 imbi12d 
 |-  ( y = ( x vH B ) -> ( ( B C_ y -> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) <-> ( B C_ ( x vH B ) -> ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) ) )
11 10 rspcv 
 |-  ( ( x vH B ) e. CH -> ( A. y e. CH ( B C_ y -> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) -> ( B C_ ( x vH B ) -> ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) ) )
12 4 11 syl 
 |-  ( ( x e. CH /\ B e. CH ) -> ( A. y e. CH ( B C_ y -> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) -> ( B C_ ( x vH B ) -> ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) ) )
13 3 12 mpid 
 |-  ( ( x e. CH /\ B e. CH ) -> ( A. y e. CH ( B C_ y -> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) -> ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
14 13 ex 
 |-  ( x e. CH -> ( B e. CH -> ( A. y e. CH ( B C_ y -> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) -> ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) ) )
15 14 com3l 
 |-  ( B e. CH -> ( A. y e. CH ( B C_ y -> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) -> ( x e. CH -> ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) ) )
16 15 ralrimdv 
 |-  ( B e. CH -> ( A. y e. CH ( B C_ y -> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) -> A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
17 chlejb2 
 |-  ( ( B e. CH /\ x e. CH ) -> ( B C_ x <-> ( x vH B ) = x ) )
18 17 biimpa 
 |-  ( ( ( B e. CH /\ x e. CH ) /\ B C_ x ) -> ( x vH B ) = x )
19 18 ineq1d 
 |-  ( ( ( B e. CH /\ x e. CH ) /\ B C_ x ) -> ( ( x vH B ) i^i ( A vH B ) ) = ( x i^i ( A vH B ) ) )
20 18 ineq1d 
 |-  ( ( ( B e. CH /\ x e. CH ) /\ B C_ x ) -> ( ( x vH B ) i^i A ) = ( x i^i A ) )
21 20 oveq1d 
 |-  ( ( ( B e. CH /\ x e. CH ) /\ B C_ x ) -> ( ( ( x vH B ) i^i A ) vH B ) = ( ( x i^i A ) vH B ) )
22 19 21 sseq12d 
 |-  ( ( ( B e. CH /\ x e. CH ) /\ B C_ x ) -> ( ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) <-> ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) vH B ) ) )
23 22 biimpd 
 |-  ( ( ( B e. CH /\ x e. CH ) /\ B C_ x ) -> ( ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) vH B ) ) )
24 23 ex 
 |-  ( ( B e. CH /\ x e. CH ) -> ( B C_ x -> ( ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) vH B ) ) ) )
25 24 com23 
 |-  ( ( B e. CH /\ x e. CH ) -> ( ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( B C_ x -> ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) vH B ) ) ) )
26 25 ralimdva 
 |-  ( B e. CH -> ( A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> A. x e. CH ( B C_ x -> ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) vH B ) ) ) )
27 sseq2 
 |-  ( x = y -> ( B C_ x <-> B C_ y ) )
28 ineq1 
 |-  ( x = y -> ( x i^i ( A vH B ) ) = ( y i^i ( A vH B ) ) )
29 ineq1 
 |-  ( x = y -> ( x i^i A ) = ( y i^i A ) )
30 29 oveq1d 
 |-  ( x = y -> ( ( x i^i A ) vH B ) = ( ( y i^i A ) vH B ) )
31 28 30 sseq12d 
 |-  ( x = y -> ( ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) vH B ) <-> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) )
32 27 31 imbi12d 
 |-  ( x = y -> ( ( B C_ x -> ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) vH B ) ) <-> ( B C_ y -> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) ) )
33 32 cbvralvw 
 |-  ( A. x e. CH ( B C_ x -> ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) vH B ) ) <-> A. y e. CH ( B C_ y -> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) )
34 26 33 imbitrdi 
 |-  ( B e. CH -> ( A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> A. y e. CH ( B C_ y -> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) ) )
35 16 34 impbid 
 |-  ( B e. CH -> ( A. y e. CH ( B C_ y -> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) <-> A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
36 35 adantl 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A. y e. CH ( B C_ y -> ( y i^i ( A vH B ) ) C_ ( ( y i^i A ) vH B ) ) <-> A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
37 1 36 bitrd 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) )