Metamath Proof Explorer

Theorem dmdbr5

Description: Binary relation expressing the dual modular pair property. (Contributed by NM, 15-Jan-2005) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 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 ) ) )
2 chub1 
 |-  ( ( x e. CH /\ B e. CH ) -> x C_ ( x vH B ) )
3 2 ancoms 
 |-  ( ( B e. CH /\ x e. CH ) -> x C_ ( x vH B ) )
4 ssin 
 |-  ( ( x C_ ( x vH B ) /\ x C_ ( A vH B ) ) <-> x C_ ( ( x vH B ) i^i ( A vH B ) ) )
5 sstr2 
 |-  ( x C_ ( ( x vH B ) i^i ( A vH B ) ) -> ( ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
6 4 5 sylbi 
 |-  ( ( x C_ ( x vH B ) /\ x C_ ( A vH B ) ) -> ( ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
7 3 6 sylan 
 |-  ( ( ( B e. CH /\ x e. CH ) /\ x C_ ( A vH B ) ) -> ( ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
8 7 ex 
 |-  ( ( B e. CH /\ x e. CH ) -> ( x C_ ( A vH B ) -> ( ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) ) )
9 8 com23 
 |-  ( ( B e. CH /\ x e. CH ) -> ( ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( x C_ ( A vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) ) )
10 9 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 ( x C_ ( A vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) ) )
11 10 adantl 
 |-  ( ( A e. CH /\ 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 ( x C_ ( A vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) ) )
12 1 11 sylbid 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B -> A. x e. CH ( x C_ ( A vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) ) )
13 sseq1 
 |-  ( x = ( ( y vH B ) i^i ( A vH B ) ) -> ( x C_ ( A vH B ) <-> ( ( y vH B ) i^i ( A vH B ) ) C_ ( A vH B ) ) )
14 id 
 |-  ( x = ( ( y vH B ) i^i ( A vH B ) ) -> x = ( ( y vH B ) i^i ( A vH B ) ) )
15 oveq1 
 |-  ( x = ( ( y vH B ) i^i ( A vH B ) ) -> ( x vH B ) = ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) )
16 15 ineq1d 
 |-  ( x = ( ( y vH B ) i^i ( A vH B ) ) -> ( ( x vH B ) i^i A ) = ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) )
17 16 oveq1d 
 |-  ( x = ( ( y vH B ) i^i ( A vH B ) ) -> ( ( ( x vH B ) i^i A ) vH B ) = ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) )
18 14 17 sseq12d 
 |-  ( x = ( ( y vH B ) i^i ( A vH B ) ) -> ( x C_ ( ( ( x vH B ) i^i A ) vH B ) <-> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) ) )
19 13 18 imbi12d 
 |-  ( x = ( ( y vH B ) i^i ( A vH B ) ) -> ( ( x C_ ( A vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) <-> ( ( ( y vH B ) i^i ( A vH B ) ) C_ ( A vH B ) -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) ) ) )
20 19 rspccv 
 |-  ( A. x e. CH ( x C_ ( A vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) -> ( ( ( y vH B ) i^i ( A vH B ) ) e. CH -> ( ( ( y vH B ) i^i ( A vH B ) ) C_ ( A vH B ) -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) ) ) )
21 chjcl 
 |-  ( ( y e. CH /\ B e. CH ) -> ( y vH B ) e. CH )
22 21 ancoms 
 |-  ( ( B e. CH /\ y e. CH ) -> ( y vH B ) e. CH )
23 22 adantll 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( y vH B ) e. CH )
24 chjcl 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A vH B ) e. CH )
25 24 adantr 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( A vH B ) e. CH )
26 chincl 
 |-  ( ( ( y vH B ) e. CH /\ ( A vH B ) e. CH ) -> ( ( y vH B ) i^i ( A vH B ) ) e. CH )
27 23 25 26 syl2anc 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( y vH B ) i^i ( A vH B ) ) e. CH )
28 inss2 
 |-  ( ( y vH B ) i^i ( A vH B ) ) C_ ( A vH B )
29 pm2.27 
 |-  ( ( ( y vH B ) i^i ( A vH B ) ) e. CH -> ( ( ( ( y vH B ) i^i ( A vH B ) ) e. CH -> ( ( ( y vH B ) i^i ( A vH B ) ) C_ ( A vH B ) -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) ) ) -> ( ( ( y vH B ) i^i ( A vH B ) ) C_ ( A vH B ) -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) ) ) )
30 28 29 mpii 
 |-  ( ( ( y vH B ) i^i ( A vH B ) ) e. CH -> ( ( ( ( y vH B ) i^i ( A vH B ) ) e. CH -> ( ( ( y vH B ) i^i ( A vH B ) ) C_ ( A vH B ) -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) ) ) -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) ) )
31 27 30 syl 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( ( y vH B ) i^i ( A vH B ) ) e. CH -> ( ( ( y vH B ) i^i ( A vH B ) ) C_ ( A vH B ) -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) ) ) -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) ) )
32 chub2 
 |-  ( ( B e. CH /\ y e. CH ) -> B C_ ( y vH B ) )
33 32 adantll 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> B C_ ( y vH B ) )
34 chub2 
 |-  ( ( B e. CH /\ A e. CH ) -> B C_ ( A vH B ) )
35 34 ancoms 
 |-  ( ( A e. CH /\ B e. CH ) -> B C_ ( A vH B ) )
36 35 adantr 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> B C_ ( A vH B ) )
37 33 36 ssind 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> B C_ ( ( y vH B ) i^i ( A vH B ) ) )
38 simplr 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> B e. CH )
39 chlejb2 
 |-  ( ( B e. CH /\ ( ( y vH B ) i^i ( A vH B ) ) e. CH ) -> ( B C_ ( ( y vH B ) i^i ( A vH B ) ) <-> ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) = ( ( y vH B ) i^i ( A vH B ) ) ) )
40 38 27 39 syl2anc 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( B C_ ( ( y vH B ) i^i ( A vH B ) ) <-> ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) = ( ( y vH B ) i^i ( A vH B ) ) ) )
41 37 40 mpbid 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) = ( ( y vH B ) i^i ( A vH B ) ) )
42 41 ineq1d 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) = ( ( ( y vH B ) i^i ( A vH B ) ) i^i A ) )
43 inass 
 |-  ( ( ( y vH B ) i^i ( A vH B ) ) i^i A ) = ( ( y vH B ) i^i ( ( A vH B ) i^i A ) )
44 incom 
 |-  ( ( A vH B ) i^i A ) = ( A i^i ( A vH B ) )
45 chabs2 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A i^i ( A vH B ) ) = A )
46 44 45 eqtrid 
 |-  ( ( A e. CH /\ B e. CH ) -> ( ( A vH B ) i^i A ) = A )
47 46 ineq2d 
 |-  ( ( A e. CH /\ B e. CH ) -> ( ( y vH B ) i^i ( ( A vH B ) i^i A ) ) = ( ( y vH B ) i^i A ) )
48 43 47 eqtrid 
 |-  ( ( A e. CH /\ B e. CH ) -> ( ( ( y vH B ) i^i ( A vH B ) ) i^i A ) = ( ( y vH B ) i^i A ) )
49 48 adantr 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( y vH B ) i^i ( A vH B ) ) i^i A ) = ( ( y vH B ) i^i A ) )
50 42 49 eqtrd 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) = ( ( y vH B ) i^i A ) )
51 50 oveq1d 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) = ( ( ( y vH B ) i^i A ) vH B ) )
52 51 sseq2d 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) <-> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( y vH B ) i^i A ) vH B ) ) )
53 31 52 sylibd 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( ( y vH B ) i^i ( A vH B ) ) e. CH -> ( ( ( y vH B ) i^i ( A vH B ) ) C_ ( A vH B ) -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) ) ) -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( y vH B ) i^i A ) vH B ) ) )
54 53 ex 
 |-  ( ( A e. CH /\ B e. CH ) -> ( y e. CH -> ( ( ( ( y vH B ) i^i ( A vH B ) ) e. CH -> ( ( ( y vH B ) i^i ( A vH B ) ) C_ ( A vH B ) -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) ) ) -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( y vH B ) i^i A ) vH B ) ) ) )
55 54 com23 
 |-  ( ( A e. CH /\ B e. CH ) -> ( ( ( ( y vH B ) i^i ( A vH B ) ) e. CH -> ( ( ( y vH B ) i^i ( A vH B ) ) C_ ( A vH B ) -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( ( ( y vH B ) i^i ( A vH B ) ) vH B ) i^i A ) vH B ) ) ) -> ( y e. CH -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( y vH B ) i^i A ) vH B ) ) ) )
56 20 55 syl5 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A. x e. CH ( x C_ ( A vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) -> ( y e. CH -> ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( y vH B ) i^i A ) vH B ) ) ) )
57 56 ralrimdv 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A. x e. CH ( x C_ ( A vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) -> A. y e. CH ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( y vH B ) i^i A ) vH B ) ) )
58 dmdbr4 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> A. y e. CH ( ( y vH B ) i^i ( A vH B ) ) C_ ( ( ( y vH B ) i^i A ) vH B ) ) )
59 57 58 sylibrd 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A. x e. CH ( x C_ ( A vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) -> A MH* B ) )
60 12 59 impbid 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> A. x e. CH ( x C_ ( A vH B ) -> x C_ ( ( ( x vH B ) i^i A ) vH B ) ) ) )