Theorem ssmd1

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	ssmd1	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 𝑀ℋ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		inss1	⊢ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ 𝐴 )
2		dfss	⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝐴 = ( 𝐴 ∩ 𝐵 ) )
3	2	biimpi	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( 𝐴 ∩ 𝐵 ) )
4	3	oveq2d	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∨ℋ 𝐴 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
5	1 4	sseqtrid	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
6	5	a1d	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
7	6	ralrimivw	⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
8		mdbr2	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
9	7 8	imbitrrid	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊆ 𝐵 → 𝐴 𝑀ℋ 𝐵 ) )
10	9	3impia	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 𝑀ℋ 𝐵 )