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