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

Proof

Step Hyp Ref Expression
1 mdbr2 ( ( 𝐴C𝐵C ) → ( 𝐴 𝑀 𝐵 ↔ ∀ 𝑦C ( 𝑦𝐵 → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) ) )
2 chincl ( ( 𝑥C𝐵C ) → ( 𝑥𝐵 ) ∈ C )
3 inss2 ( 𝑥𝐵 ) ⊆ 𝐵
4 sseq1 ( 𝑦 = ( 𝑥𝐵 ) → ( 𝑦𝐵 ↔ ( 𝑥𝐵 ) ⊆ 𝐵 ) )
5 oveq1 ( 𝑦 = ( 𝑥𝐵 ) → ( 𝑦 𝐴 ) = ( ( 𝑥𝐵 ) ∨ 𝐴 ) )
6 5 ineq1d ( 𝑦 = ( 𝑥𝐵 ) → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) = ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) )
7 oveq1 ( 𝑦 = ( 𝑥𝐵 ) → ( 𝑦 ( 𝐴𝐵 ) ) = ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) )
8 6 7 sseq12d ( 𝑦 = ( 𝑥𝐵 ) → ( ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ↔ ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) ) )
9 4 8 imbi12d ( 𝑦 = ( 𝑥𝐵 ) → ( ( 𝑦𝐵 → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) ↔ ( ( 𝑥𝐵 ) ⊆ 𝐵 → ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) ) ) )
10 9 rspcv ( ( 𝑥𝐵 ) ∈ C → ( ∀ 𝑦C ( 𝑦𝐵 → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) → ( ( 𝑥𝐵 ) ⊆ 𝐵 → ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) ) ) )
11 3 10 mpii ( ( 𝑥𝐵 ) ∈ C → ( ∀ 𝑦C ( 𝑦𝐵 → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) → ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) ) )
12 2 11 syl ( ( 𝑥C𝐵C ) → ( ∀ 𝑦C ( 𝑦𝐵 → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) → ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) ) )
13 12 ex ( 𝑥C → ( 𝐵C → ( ∀ 𝑦C ( 𝑦𝐵 → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) → ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) ) ) )
14 13 com3l ( 𝐵C → ( ∀ 𝑦C ( 𝑦𝐵 → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) → ( 𝑥C → ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) ) ) )
15 14 ralrimdv ( 𝐵C → ( ∀ 𝑦C ( 𝑦𝐵 → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) → ∀ 𝑥C ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) ) )
16 dfss ( 𝑥𝐵𝑥 = ( 𝑥𝐵 ) )
17 16 biimpi ( 𝑥𝐵𝑥 = ( 𝑥𝐵 ) )
18 17 oveq1d ( 𝑥𝐵 → ( 𝑥 𝐴 ) = ( ( 𝑥𝐵 ) ∨ 𝐴 ) )
19 18 ineq1d ( 𝑥𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) )
20 17 oveq1d ( 𝑥𝐵 → ( 𝑥 ( 𝐴𝐵 ) ) = ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) )
21 19 20 sseq12d ( 𝑥𝐵 → ( ( ( 𝑥 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ( 𝐴𝐵 ) ) ↔ ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) ) )
22 21 biimprcd ( ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) → ( 𝑥𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ( 𝐴𝐵 ) ) ) )
23 22 ralimi ( ∀ 𝑥C ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) → ∀ 𝑥C ( 𝑥𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ( 𝐴𝐵 ) ) ) )
24 sseq1 ( 𝑥 = 𝑦 → ( 𝑥𝐵𝑦𝐵 ) )
25 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 𝐴 ) = ( 𝑦 𝐴 ) )
26 25 ineq1d ( 𝑥 = 𝑦 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 𝐴 ) ∩ 𝐵 ) )
27 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 ( 𝐴𝐵 ) ) = ( 𝑦 ( 𝐴𝐵 ) ) )
28 26 27 sseq12d ( 𝑥 = 𝑦 → ( ( ( 𝑥 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ( 𝐴𝐵 ) ) ↔ ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) )
29 24 28 imbi12d ( 𝑥 = 𝑦 → ( ( 𝑥𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ( 𝐴𝐵 ) ) ) ↔ ( 𝑦𝐵 → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) ) )
30 29 cbvralvw ( ∀ 𝑥C ( 𝑥𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ( 𝐴𝐵 ) ) ) ↔ ∀ 𝑦C ( 𝑦𝐵 → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) )
31 23 30 sylib ( ∀ 𝑥C ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) → ∀ 𝑦C ( 𝑦𝐵 → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) )
32 15 31 impbid1 ( 𝐵C → ( ∀ 𝑦C ( 𝑦𝐵 → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) ↔ ∀ 𝑥C ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) ) )
33 32 adantl ( ( 𝐴C𝐵C ) → ( ∀ 𝑦C ( 𝑦𝐵 → ( ( 𝑦 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ( 𝐴𝐵 ) ) ) ↔ ∀ 𝑥C ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) ) )
34 1 33 bitrd ( ( 𝐴C𝐵C ) → ( 𝐴 𝑀 𝐵 ↔ ∀ 𝑥C ( ( ( 𝑥𝐵 ) ∨ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥𝐵 ) ∨ ( 𝐴𝐵 ) ) ) )