# Metamath Proof Explorer

## Theorem ssmd2

Description: Ordering implies the modular pair property. Remark in MaedaMaeda p. 1. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion ssmd2 ( ( 𝐴C𝐵C𝐴𝐵 ) → 𝐵 𝑀 𝐴 )

### Proof

Step Hyp Ref Expression
1 inss2 ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ⊆ 𝐴
2 chub2 ( ( 𝐴C𝑥C ) → 𝐴 ⊆ ( 𝑥 𝐴 ) )
3 1 2 sstrid ( ( 𝐴C𝑥C ) → ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 𝐴 ) )
4 3 adantrl ( ( 𝐴C ∧ ( 𝐴𝐵𝑥C ) ) → ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 𝐴 ) )
5 simpl ( ( 𝐴𝐵𝑥C ) → 𝐴𝐵 )
6 sseqin2 ( 𝐴𝐵 ↔ ( 𝐵𝐴 ) = 𝐴 )
7 5 6 sylib ( ( 𝐴𝐵𝑥C ) → ( 𝐵𝐴 ) = 𝐴 )
8 7 adantl ( ( 𝐴C ∧ ( 𝐴𝐵𝑥C ) ) → ( 𝐵𝐴 ) = 𝐴 )
9 8 oveq2d ( ( 𝐴C ∧ ( 𝐴𝐵𝑥C ) ) → ( 𝑥 ( 𝐵𝐴 ) ) = ( 𝑥 𝐴 ) )
10 4 9 sseqtrrd ( ( 𝐴C ∧ ( 𝐴𝐵𝑥C ) ) → ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ( 𝐵𝐴 ) ) )
11 10 a1d ( ( 𝐴C ∧ ( 𝐴𝐵𝑥C ) ) → ( 𝑥𝐴 → ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ( 𝐵𝐴 ) ) ) )
12 11 exp32 ( 𝐴C → ( 𝐴𝐵 → ( 𝑥C → ( 𝑥𝐴 → ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ( 𝐵𝐴 ) ) ) ) ) )
13 12 ralrimdv ( 𝐴C → ( 𝐴𝐵 → ∀ 𝑥C ( 𝑥𝐴 → ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ( 𝐵𝐴 ) ) ) ) )
14 13 adantr ( ( 𝐴C𝐵C ) → ( 𝐴𝐵 → ∀ 𝑥C ( 𝑥𝐴 → ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ( 𝐵𝐴 ) ) ) ) )
15 mdbr2 ( ( 𝐵C𝐴C ) → ( 𝐵 𝑀 𝐴 ↔ ∀ 𝑥C ( 𝑥𝐴 → ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ( 𝐵𝐴 ) ) ) ) )
16 15 ancoms ( ( 𝐴C𝐵C ) → ( 𝐵 𝑀 𝐴 ↔ ∀ 𝑥C ( 𝑥𝐴 → ( ( 𝑥 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ( 𝐵𝐴 ) ) ) ) )
17 14 16 sylibrd ( ( 𝐴C𝐵C ) → ( 𝐴𝐵𝐵 𝑀 𝐴 ) )
18 17 3impia ( ( 𝐴C𝐵C𝐴𝐵 ) → 𝐵 𝑀 𝐴 )