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

Metamath Proof Explorer

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 ⊢ ( 𝐴 ⊆ 𝐵 → ≀ 𝐴 ⊆ ≀ 𝐵 )