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 𝐴C
mdsl.2 𝐵C
Assertion cvmdi ( ( 𝐴𝐵 ) ⋖ 𝐵𝐴 𝑀 𝐵 )

Proof

Step Hyp Ref Expression
1 mdsl.1 𝐴C
2 mdsl.2 𝐵C
3 anass ( ( ( ( 𝐴𝐵 ) ⊆ 𝑥𝑥 ⊆ ( 𝐴 𝐵 ) ) ∧ 𝑥𝐵 ) ↔ ( ( 𝐴𝐵 ) ⊆ 𝑥 ∧ ( 𝑥 ⊆ ( 𝐴 𝐵 ) ∧ 𝑥𝐵 ) ) )
4 2 1 chub2i 𝐵 ⊆ ( 𝐴 𝐵 )
5 sstr ( ( 𝑥𝐵𝐵 ⊆ ( 𝐴 𝐵 ) ) → 𝑥 ⊆ ( 𝐴 𝐵 ) )
6 4 5 mpan2 ( 𝑥𝐵𝑥 ⊆ ( 𝐴 𝐵 ) )
7 6 pm4.71ri ( 𝑥𝐵 ↔ ( 𝑥 ⊆ ( 𝐴 𝐵 ) ∧ 𝑥𝐵 ) )
8 7 anbi2i ( ( ( 𝐴𝐵 ) ⊆ 𝑥𝑥𝐵 ) ↔ ( ( 𝐴𝐵 ) ⊆ 𝑥 ∧ ( 𝑥 ⊆ ( 𝐴 𝐵 ) ∧ 𝑥𝐵 ) ) )
9 3 8 bitr4i ( ( ( ( 𝐴𝐵 ) ⊆ 𝑥𝑥 ⊆ ( 𝐴 𝐵 ) ) ∧ 𝑥𝐵 ) ↔ ( ( 𝐴𝐵 ) ⊆ 𝑥𝑥𝐵 ) )
10 1 2 chincli ( 𝐴𝐵 ) ∈ C
11 cvnbtwn4 ( ( ( 𝐴𝐵 ) ∈ C𝐵C𝑥C ) → ( ( 𝐴𝐵 ) ⋖ 𝐵 → ( ( ( 𝐴𝐵 ) ⊆ 𝑥𝑥𝐵 ) → ( 𝑥 = ( 𝐴𝐵 ) ∨ 𝑥 = 𝐵 ) ) ) )
12 10 2 11 mp3an12 ( 𝑥C → ( ( 𝐴𝐵 ) ⋖ 𝐵 → ( ( ( 𝐴𝐵 ) ⊆ 𝑥𝑥𝐵 ) → ( 𝑥 = ( 𝐴𝐵 ) ∨ 𝑥 = 𝐵 ) ) ) )
13 12 impcom ( ( ( 𝐴𝐵 ) ⋖ 𝐵𝑥C ) → ( ( ( 𝐴𝐵 ) ⊆ 𝑥𝑥𝐵 ) → ( 𝑥 = ( 𝐴𝐵 ) ∨ 𝑥 = 𝐵 ) ) )
14 10 1 chjcomi ( ( 𝐴𝐵 ) ∨ 𝐴 ) = ( 𝐴 ( 𝐴𝐵 ) )
15 1 2 chabs1i ( 𝐴 ( 𝐴𝐵 ) ) = 𝐴
16 14 15 eqtri ( ( 𝐴𝐵 ) ∨ 𝐴 ) = 𝐴
17 16 ineq1i ( ( ( 𝐴𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) = ( 𝐴𝐵 )
18 10 chjidmi ( ( 𝐴𝐵 ) ∨ ( 𝐴𝐵 ) ) = ( 𝐴𝐵 )
19 17 18 eqtr4i ( ( ( 𝐴𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) = ( ( 𝐴𝐵 ) ∨ ( 𝐴𝐵 ) )
20 oveq1 ( 𝑥 = ( 𝐴𝐵 ) → ( 𝑥 𝐴 ) = ( ( 𝐴𝐵 ) ∨ 𝐴 ) )
21 20 ineq1d ( 𝑥 = ( 𝐴𝐵 ) → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( ( ( 𝐴𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) )
22 oveq1 ( 𝑥 = ( 𝐴𝐵 ) → ( 𝑥 ( 𝐴𝐵 ) ) = ( ( 𝐴𝐵 ) ∨ ( 𝐴𝐵 ) ) )
23 19 21 22 3eqtr4a ( 𝑥 = ( 𝐴𝐵 ) → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) )
24 incom ( ( 𝐵 𝐴 ) ∩ 𝐵 ) = ( 𝐵 ∩ ( 𝐵 𝐴 ) )
25 2 1 chabs2i ( 𝐵 ∩ ( 𝐵 𝐴 ) ) = 𝐵
26 2 1 chabs1i ( 𝐵 ( 𝐵𝐴 ) ) = 𝐵
27 incom ( 𝐵𝐴 ) = ( 𝐴𝐵 )
28 27 oveq2i ( 𝐵 ( 𝐵𝐴 ) ) = ( 𝐵 ( 𝐴𝐵 ) )
29 25 26 28 3eqtr2i ( 𝐵 ∩ ( 𝐵 𝐴 ) ) = ( 𝐵 ( 𝐴𝐵 ) )
30 24 29 eqtri ( ( 𝐵 𝐴 ) ∩ 𝐵 ) = ( 𝐵 ( 𝐴𝐵 ) )
31 oveq1 ( 𝑥 = 𝐵 → ( 𝑥 𝐴 ) = ( 𝐵 𝐴 ) )
32 31 ineq1d ( 𝑥 = 𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( ( 𝐵 𝐴 ) ∩ 𝐵 ) )
33 oveq1 ( 𝑥 = 𝐵 → ( 𝑥 ( 𝐴𝐵 ) ) = ( 𝐵 ( 𝐴𝐵 ) ) )
34 30 32 33 3eqtr4a ( 𝑥 = 𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) )
35 23 34 jaoi ( ( 𝑥 = ( 𝐴𝐵 ) ∨ 𝑥 = 𝐵 ) → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) )
36 13 35 syl6 ( ( ( 𝐴𝐵 ) ⋖ 𝐵𝑥C ) → ( ( ( 𝐴𝐵 ) ⊆ 𝑥𝑥𝐵 ) → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) ) )
37 9 36 syl5bi ( ( ( 𝐴𝐵 ) ⋖ 𝐵𝑥C ) → ( ( ( ( 𝐴𝐵 ) ⊆ 𝑥𝑥 ⊆ ( 𝐴 𝐵 ) ) ∧ 𝑥𝐵 ) → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) ) )
38 37 exp4b ( ( 𝐴𝐵 ) ⋖ 𝐵 → ( 𝑥C → ( ( ( 𝐴𝐵 ) ⊆ 𝑥𝑥 ⊆ ( 𝐴 𝐵 ) ) → ( 𝑥𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) ) ) ) )
39 38 ralrimiv ( ( 𝐴𝐵 ) ⋖ 𝐵 → ∀ 𝑥C ( ( ( 𝐴𝐵 ) ⊆ 𝑥𝑥 ⊆ ( 𝐴 𝐵 ) ) → ( 𝑥𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) ) ) )
40 1 2 mdsl1i ( ∀ 𝑥C ( ( ( 𝐴𝐵 ) ⊆ 𝑥𝑥 ⊆ ( 𝐴 𝐵 ) ) → ( 𝑥𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) ) ) ↔ 𝐴 𝑀 𝐵 )
41 39 40 sylib ( ( 𝐴𝐵 ) ⋖ 𝐵𝐴 𝑀 𝐵 )