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

Proof

Step Hyp Ref Expression
1 dmdbr2 ( ( 𝐴C𝐵C ) → ( 𝐴 𝑀* 𝐵 ↔ ∀ 𝑦C ( 𝐵𝑦 → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) ) )
2 chub2 ( ( 𝐵C𝑥C ) → 𝐵 ⊆ ( 𝑥 𝐵 ) )
3 2 ancoms ( ( 𝑥C𝐵C ) → 𝐵 ⊆ ( 𝑥 𝐵 ) )
4 chjcl ( ( 𝑥C𝐵C ) → ( 𝑥 𝐵 ) ∈ C )
5 sseq2 ( 𝑦 = ( 𝑥 𝐵 ) → ( 𝐵𝑦𝐵 ⊆ ( 𝑥 𝐵 ) ) )
6 ineq1 ( 𝑦 = ( 𝑥 𝐵 ) → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) = ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) )
7 ineq1 ( 𝑦 = ( 𝑥 𝐵 ) → ( 𝑦𝐴 ) = ( ( 𝑥 𝐵 ) ∩ 𝐴 ) )
8 7 oveq1d ( 𝑦 = ( 𝑥 𝐵 ) → ( ( 𝑦𝐴 ) ∨ 𝐵 ) = ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) )
9 6 8 sseq12d ( 𝑦 = ( 𝑥 𝐵 ) → ( ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ↔ ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
10 5 9 imbi12d ( 𝑦 = ( 𝑥 𝐵 ) → ( ( 𝐵𝑦 → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) ↔ ( 𝐵 ⊆ ( 𝑥 𝐵 ) → ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
11 10 rspcv ( ( 𝑥 𝐵 ) ∈ C → ( ∀ 𝑦C ( 𝐵𝑦 → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) → ( 𝐵 ⊆ ( 𝑥 𝐵 ) → ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
12 4 11 syl ( ( 𝑥C𝐵C ) → ( ∀ 𝑦C ( 𝐵𝑦 → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) → ( 𝐵 ⊆ ( 𝑥 𝐵 ) → ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
13 3 12 mpid ( ( 𝑥C𝐵C ) → ( ∀ 𝑦C ( 𝐵𝑦 → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) → ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
14 13 ex ( 𝑥C → ( 𝐵C → ( ∀ 𝑦C ( 𝐵𝑦 → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) → ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
15 14 com3l ( 𝐵C → ( ∀ 𝑦C ( 𝐵𝑦 → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) → ( 𝑥C → ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) ) )
16 15 ralrimdv ( 𝐵C → ( ∀ 𝑦C ( 𝐵𝑦 → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) → ∀ 𝑥C ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
17 chlejb2 ( ( 𝐵C𝑥C ) → ( 𝐵𝑥 ↔ ( 𝑥 𝐵 ) = 𝑥 ) )
18 17 biimpa ( ( ( 𝐵C𝑥C ) ∧ 𝐵𝑥 ) → ( 𝑥 𝐵 ) = 𝑥 )
19 18 ineq1d ( ( ( 𝐵C𝑥C ) ∧ 𝐵𝑥 ) → ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) = ( 𝑥 ∩ ( 𝐴 𝐵 ) ) )
20 18 ineq1d ( ( ( 𝐵C𝑥C ) ∧ 𝐵𝑥 ) → ( ( 𝑥 𝐵 ) ∩ 𝐴 ) = ( 𝑥𝐴 ) )
21 20 oveq1d ( ( ( 𝐵C𝑥C ) ∧ 𝐵𝑥 ) → ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) = ( ( 𝑥𝐴 ) ∨ 𝐵 ) )
22 19 21 sseq12d ( ( ( 𝐵C𝑥C ) ∧ 𝐵𝑥 ) → ( ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ↔ ( 𝑥 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑥𝐴 ) ∨ 𝐵 ) ) )
23 22 biimpd ( ( ( 𝐵C𝑥C ) ∧ 𝐵𝑥 ) → ( ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) → ( 𝑥 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑥𝐴 ) ∨ 𝐵 ) ) )
24 23 ex ( ( 𝐵C𝑥C ) → ( 𝐵𝑥 → ( ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) → ( 𝑥 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑥𝐴 ) ∨ 𝐵 ) ) ) )
25 24 com23 ( ( 𝐵C𝑥C ) → ( ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) → ( 𝐵𝑥 → ( 𝑥 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑥𝐴 ) ∨ 𝐵 ) ) ) )
26 25 ralimdva ( 𝐵C → ( ∀ 𝑥C ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) → ∀ 𝑥C ( 𝐵𝑥 → ( 𝑥 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑥𝐴 ) ∨ 𝐵 ) ) ) )
27 sseq2 ( 𝑥 = 𝑦 → ( 𝐵𝑥𝐵𝑦 ) )
28 ineq1 ( 𝑥 = 𝑦 → ( 𝑥 ∩ ( 𝐴 𝐵 ) ) = ( 𝑦 ∩ ( 𝐴 𝐵 ) ) )
29 ineq1 ( 𝑥 = 𝑦 → ( 𝑥𝐴 ) = ( 𝑦𝐴 ) )
30 29 oveq1d ( 𝑥 = 𝑦 → ( ( 𝑥𝐴 ) ∨ 𝐵 ) = ( ( 𝑦𝐴 ) ∨ 𝐵 ) )
31 28 30 sseq12d ( 𝑥 = 𝑦 → ( ( 𝑥 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑥𝐴 ) ∨ 𝐵 ) ↔ ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) )
32 27 31 imbi12d ( 𝑥 = 𝑦 → ( ( 𝐵𝑥 → ( 𝑥 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑥𝐴 ) ∨ 𝐵 ) ) ↔ ( 𝐵𝑦 → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) ) )
33 32 cbvralvw ( ∀ 𝑥C ( 𝐵𝑥 → ( 𝑥 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑥𝐴 ) ∨ 𝐵 ) ) ↔ ∀ 𝑦C ( 𝐵𝑦 → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) )
34 26 33 syl6ib ( 𝐵C → ( ∀ 𝑥C ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) → ∀ 𝑦C ( 𝐵𝑦 → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) ) )
35 16 34 impbid ( 𝐵C → ( ∀ 𝑦C ( 𝐵𝑦 → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) ↔ ∀ 𝑥C ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
36 35 adantl ( ( 𝐴C𝐵C ) → ( ∀ 𝑦C ( 𝐵𝑦 → ( 𝑦 ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( 𝑦𝐴 ) ∨ 𝐵 ) ) ↔ ∀ 𝑥C ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )
37 1 36 bitrd ( ( 𝐴C𝐵C ) → ( 𝐴 𝑀* 𝐵 ↔ ∀ 𝑥C ( ( 𝑥 𝐵 ) ∩ ( 𝐴 𝐵 ) ) ⊆ ( ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ∨ 𝐵 ) ) )