This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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ℋ ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 𝑀ℋ 𝐴 )