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 ( ( 𝐴C𝐵C ) → ( 𝐴 𝑀* 𝐵 ↔ ∀ 𝑥C ( 𝑥 ⊆ ( 𝐴 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 dmdbr4 ( ( 𝐴C𝐵C ) → ( 𝐴 𝑀* 𝐵 ↔ ∀ 𝑥C ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
2 chub1 ( ( 𝑥C𝐵C ) → 𝑥 ⊆ ( 𝑥 𝐵 ) )
3 2 ancoms ( ( 𝐵C𝑥C ) → 𝑥 ⊆ ( 𝑥 𝐵 ) )
4 ssin ( ( 𝑥 ⊆ ( 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝐴 𝐵 ) ) ↔ 𝑥 ⊆ ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) )
5 sstr2 ( 𝑥 ⊆ ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) → ( ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
6 4 5 sylbi ( ( 𝑥 ⊆ ( 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝐴 𝐵 ) ) → ( ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
7 3 6 sylan ( ( ( 𝐵C𝑥C ) ∧ 𝑥 ⊆ ( 𝐴 𝐵 ) ) → ( ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
8 7 ex ( ( 𝐵C𝑥C ) → ( 𝑥 ⊆ ( 𝐴 𝐵 ) → ( ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
9 8 com23 ( ( 𝐵C𝑥C ) → ( ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) → ( 𝑥 ⊆ ( 𝐴 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
10 9 ralimdva ( 𝐵C → ( ∀ 𝑥C ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) → ∀ 𝑥C ( 𝑥 ⊆ ( 𝐴 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
11 10 adantl ( ( 𝐴C𝐵C ) → ( ∀ 𝑥C ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) → ∀ 𝑥C ( 𝑥 ⊆ ( 𝐴 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
12 1 11 sylbid ( ( 𝐴C𝐵C ) → ( 𝐴 𝑀* 𝐵 → ∀ 𝑥C ( 𝑥 ⊆ ( 𝐴 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
13 sseq1 ( 𝑥 = ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) → ( 𝑥 ⊆ ( 𝐴 𝐵 ) ↔ ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( 𝐴 𝐵 ) ) )
14 id ( 𝑥 = ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) → 𝑥 = ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) )
15 oveq1 ( 𝑥 = ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) → ( 𝑥 𝐵 ) = ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) )
16 15 ineq1d ( 𝑥 = ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) → ( ( 𝑥 𝐵 ) ∩ 𝐴 ) = ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) )
17 16 oveq1d ( 𝑥 = ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) → ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) = ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) )
18 14 17 sseq12d ( 𝑥 = ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) → ( 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ↔ ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
19 13 18 imbi12d ( 𝑥 = ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) → ( ( 𝑥 ⊆ ( 𝐴 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ↔ ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( 𝐴 𝐵 ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
20 19 rspccv ( ∀ 𝑥C ( 𝑥 ⊆ ( 𝐴 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) → ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∈ C → ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( 𝐴 𝐵 ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
21 chjcl ( ( 𝑦C𝐵C ) → ( 𝑦 𝐵 ) ∈ C )
22 21 ancoms ( ( 𝐵C𝑦C ) → ( 𝑦 𝐵 ) ∈ C )
23 22 adantll ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → ( 𝑦 𝐵 ) ∈ C )
24 chjcl ( ( 𝐴C𝐵C ) → ( 𝐴 𝐵 ) ∈ C )
25 24 adantr ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → ( 𝐴 𝐵 ) ∈ C )
26 chincl ( ( ( 𝑦 𝐵 ) ∈ C ∧ ( 𝐴 𝐵 ) ∈ C ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∈ C )
27 23 25 26 syl2anc ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∈ C )
28 inss2 ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( 𝐴 𝐵 )
29 pm2.27 ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∈ C → ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∈ C → ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( 𝐴 𝐵 ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) → ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( 𝐴 𝐵 ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
30 28 29 mpii ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∈ C → ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∈ C → ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( 𝐴 𝐵 ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
31 27 30 syl ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∈ C → ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( 𝐴 𝐵 ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
32 chub2 ( ( 𝐵C𝑦C ) → 𝐵 ⊆ ( 𝑦 𝐵 ) )
33 32 adantll ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → 𝐵 ⊆ ( 𝑦 𝐵 ) )
34 chub2 ( ( 𝐵C𝐴C ) → 𝐵 ⊆ ( 𝐴 𝐵 ) )
35 34 ancoms ( ( 𝐴C𝐵C ) → 𝐵 ⊆ ( 𝐴 𝐵 ) )
36 35 adantr ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → 𝐵 ⊆ ( 𝐴 𝐵 ) )
37 33 36 ssind ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → 𝐵 ⊆ ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) )
38 simplr ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → 𝐵C )
39 chlejb2 ( ( 𝐵C ∧ ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∈ C ) → ( 𝐵 ⊆ ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ↔ ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) = ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ) )
40 38 27 39 syl2anc ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → ( 𝐵 ⊆ ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ↔ ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) = ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ) )
41 37 40 mpbid ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) = ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) )
42 41 ineq1d ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) = ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∩ 𝐴 ) )
43 inass ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∩ 𝐴 ) = ( ( 𝑦 𝐵 ) ∩ ( ( 𝐴 𝐵 ) ∩ 𝐴 ) )
44 incom ( ( 𝐴 𝐵 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( 𝐴 𝐵 ) )
45 chabs2 ( ( 𝐴C𝐵C ) → ( 𝐴 ∩ ( 𝐴 𝐵 ) ) = 𝐴 )
46 44 45 syl5eq ( ( 𝐴C𝐵C ) → ( ( 𝐴 𝐵 ) ∩ 𝐴 ) = 𝐴 )
47 46 ineq2d ( ( 𝐴C𝐵C ) → ( ( 𝑦 𝐵 ) ∩ ( ( 𝐴 𝐵 ) ∩ 𝐴 ) ) = ( ( 𝑦 𝐵 ) ∩ 𝐴 ) )
48 43 47 syl5eq ( ( 𝐴C𝐵C ) → ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∩ 𝐴 ) = ( ( 𝑦 𝐵 ) ∩ 𝐴 ) )
49 48 adantr ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∩ 𝐴 ) = ( ( 𝑦 𝐵 ) ∩ 𝐴 ) )
50 42 49 eqtrd ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) = ( ( 𝑦 𝐵 ) ∩ 𝐴 ) )
51 50 oveq1d ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) = ( ( ( 𝑦 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) )
52 51 sseq2d ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ↔ ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑦 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
53 31 52 sylibd ( ( ( 𝐴C𝐵C ) ∧ 𝑦C ) → ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∈ C → ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( 𝐴 𝐵 ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑦 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
54 53 ex ( ( 𝐴C𝐵C ) → ( 𝑦C → ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∈ C → ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( 𝐴 𝐵 ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑦 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
55 54 com23 ( ( 𝐴C𝐵C ) → ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∈ C → ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( 𝐴 𝐵 ) → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ∨ 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) → ( 𝑦C → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑦 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
56 20 55 syl5 ( ( 𝐴C𝐵C ) → ( ∀ 𝑥C ( 𝑥 ⊆ ( 𝐴 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) → ( 𝑦C → ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑦 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
57 56 ralrimdv ( ( 𝐴C𝐵C ) → ( ∀ 𝑥C ( 𝑥 ⊆ ( 𝐴 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) → ∀ 𝑦C ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑦 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
58 dmdbr4 ( ( 𝐴C𝐵C ) → ( 𝐴 𝑀* 𝐵 ↔ ∀ 𝑦C ( ( 𝑦 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑦 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
59 57 58 sylibrd ( ( 𝐴C𝐵C ) → ( ∀ 𝑥C ( 𝑥 ⊆ ( 𝐴 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) → 𝐴 𝑀* 𝐵 ) )
60 12 59 impbid ( ( 𝐴C𝐵C ) → ( 𝐴 𝑀* 𝐵 ↔ ∀ 𝑥C ( 𝑥 ⊆ ( 𝐴 𝐵 ) → 𝑥 ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )