Metamath Proof Explorer

Theorem mdbr4

Description: Binary relation expressing the 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 mdbr4 
|- ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) ) )

Proof

Step Hyp Ref Expression
1 mdbr2 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. y e. CH ( y C_ B -> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) ) )
2 chincl 
 |-  ( ( x e. CH /\ B e. CH ) -> ( x i^i B ) e. CH )
3 inss2 
 |-  ( x i^i B ) C_ B
4 sseq1 
 |-  ( y = ( x i^i B ) -> ( y C_ B <-> ( x i^i B ) C_ B ) )
5 oveq1 
 |-  ( y = ( x i^i B ) -> ( y vH A ) = ( ( x i^i B ) vH A ) )
6 5 ineq1d 
 |-  ( y = ( x i^i B ) -> ( ( y vH A ) i^i B ) = ( ( ( x i^i B ) vH A ) i^i B ) )
7 oveq1 
 |-  ( y = ( x i^i B ) -> ( y vH ( A i^i B ) ) = ( ( x i^i B ) vH ( A i^i B ) ) )
8 6 7 sseq12d 
 |-  ( y = ( x i^i B ) -> ( ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) <-> ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) ) )
9 4 8 imbi12d 
 |-  ( y = ( x i^i B ) -> ( ( y C_ B -> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) <-> ( ( x i^i B ) C_ B -> ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) ) ) )
10 9 rspcv 
 |-  ( ( x i^i B ) e. CH -> ( A. y e. CH ( y C_ B -> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) -> ( ( x i^i B ) C_ B -> ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) ) ) )
11 3 10 mpii 
 |-  ( ( x i^i B ) e. CH -> ( A. y e. CH ( y C_ B -> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) -> ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) ) )
12 2 11 syl 
 |-  ( ( x e. CH /\ B e. CH ) -> ( A. y e. CH ( y C_ B -> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) -> ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) ) )
13 12 ex 
 |-  ( x e. CH -> ( B e. CH -> ( A. y e. CH ( y C_ B -> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) -> ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) ) ) )
14 13 com3l 
 |-  ( B e. CH -> ( A. y e. CH ( y C_ B -> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) -> ( x e. CH -> ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) ) ) )
15 14 ralrimdv 
 |-  ( B e. CH -> ( A. y e. CH ( y C_ B -> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) -> A. x e. CH ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) ) )
16 dfss 
 |-  ( x C_ B <-> x = ( x i^i B ) )
17 16 biimpi 
 |-  ( x C_ B -> x = ( x i^i B ) )
18 17 oveq1d 
 |-  ( x C_ B -> ( x vH A ) = ( ( x i^i B ) vH A ) )
19 18 ineq1d 
 |-  ( x C_ B -> ( ( x vH A ) i^i B ) = ( ( ( x i^i B ) vH A ) i^i B ) )
20 17 oveq1d 
 |-  ( x C_ B -> ( x vH ( A i^i B ) ) = ( ( x i^i B ) vH ( A i^i B ) ) )
21 19 20 sseq12d 
 |-  ( x C_ B -> ( ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) <-> ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) ) )
22 21 biimprcd 
 |-  ( ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) -> ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) )
23 22 ralimi 
 |-  ( A. x e. CH ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) -> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) )
24 sseq1 
 |-  ( x = y -> ( x C_ B <-> y C_ B ) )
25 oveq1 
 |-  ( x = y -> ( x vH A ) = ( y vH A ) )
26 25 ineq1d 
 |-  ( x = y -> ( ( x vH A ) i^i B ) = ( ( y vH A ) i^i B ) )
27 oveq1 
 |-  ( x = y -> ( x vH ( A i^i B ) ) = ( y vH ( A i^i B ) ) )
28 26 27 sseq12d 
 |-  ( x = y -> ( ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) <-> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) )
29 24 28 imbi12d 
 |-  ( x = y -> ( ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) <-> ( y C_ B -> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) ) )
30 29 cbvralvw 
 |-  ( A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) <-> A. y e. CH ( y C_ B -> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) )
31 23 30 sylib 
 |-  ( A. x e. CH ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) -> A. y e. CH ( y C_ B -> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) )
32 15 31 impbid1 
 |-  ( B e. CH -> ( A. y e. CH ( y C_ B -> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) <-> A. x e. CH ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) ) )
33 32 adantl 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A. y e. CH ( y C_ B -> ( ( y vH A ) i^i B ) C_ ( y vH ( A i^i B ) ) ) <-> A. x e. CH ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) ) )
34 1 33 bitrd 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( ( ( x i^i B ) vH A ) i^i B ) C_ ( ( x i^i B ) vH ( A i^i B ) ) ) )