Theorem cossss

Description: Subclass theorem for the classes of cosets by A and B . (Contributed by Peter Mazsa, 11-Nov-2019)

	Ref	Expression
Assertion	cossss	⊢ ( 𝐴 ⊆ 𝐵 → ≀ 𝐴 ⊆ ≀ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ssbr	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑦 ) )
2		ssbr	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 𝐴 𝑧 → 𝑥 𝐵 𝑧 ) )
3	1 2	anim12d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → ( 𝑥 𝐵 𝑦 ∧ 𝑥 𝐵 𝑧 ) ) )
4	3	eximdv	⊢ ( 𝐴 ⊆ 𝐵 → ( ∃ 𝑥 ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → ∃ 𝑥 ( 𝑥 𝐵 𝑦 ∧ 𝑥 𝐵 𝑧 ) ) )
5	4	ssopab2dv	⊢ ( 𝐴 ⊆ 𝐵 → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) } ⊆ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑥 𝐵 𝑦 ∧ 𝑥 𝐵 𝑧 ) } )
6		df-coss	⊢ ≀ 𝐴 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) }
7		df-coss	⊢ ≀ 𝐵 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑥 𝐵 𝑦 ∧ 𝑥 𝐵 𝑧 ) }
8	5 6 7	3sstr4g	⊢ ( 𝐴 ⊆ 𝐵 → ≀ 𝐴 ⊆ ≀ 𝐵 )