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		sseqin2	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐵 ∩ 𝐴 ) = 𝐴 )
6	5	birani	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ Cℋ ) → ( 𝐵 ∩ 𝐴 ) = 𝐴 )
7	6	adantl	⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ Cℋ ) ) → ( 𝐵 ∩ 𝐴 ) = 𝐴 )
8	7	oveq2d	⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ Cℋ ) ) → ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) = ( 𝑥 ∨ℋ 𝐴 ) )
9	4 8	sseqtrrd	⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ Cℋ ) ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) )
10	9	a1d	⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ Cℋ ) ) → ( 𝑥 ⊆ 𝐴 → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) )
11	10	exp32	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ 𝐴 → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) ) ) )
12	11	ralrimdv	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐴 → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) ) )
13	12	adantr	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐴 → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) ) )
14		mdbr2	⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝐵 𝑀ℋ 𝐴 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐴 → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) ) )
15	14	ancoms	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐵 𝑀ℋ 𝐴 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐴 → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ⊆ ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) ) )
16	13 15	sylibrd	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊆ 𝐵 → 𝐵 𝑀ℋ 𝐴 ) )
17	16	3impia	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 𝑀ℋ 𝐴 )