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

Metamath Proof Explorer

Theorem disjss2

Description: If each element of a collection is contained in a disjoint collection, the original collection is also disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Assertion disjss2 ⊢ ∀ x ∈ A B ⊆ C → Disj x ∈ A C → Disj x ∈ A B

Proof

Step Hyp Ref Expression
1 ssel ⊢ B ⊆ C → y ∈ B → y ∈ C
2 1 ralimi ⊢ ∀ x ∈ A B ⊆ C → ∀ x ∈ A y ∈ B → y ∈ C
3 rmoim ⊢ ∀ x ∈ A y ∈ B → y ∈ C → ∃* x ∈ A y ∈ C → ∃* x ∈ A y ∈ B
4 2 3 syl ⊢ ∀ x ∈ A B ⊆ C → ∃* x ∈ A y ∈ C → ∃* x ∈ A y ∈ B
5 4 alimdv ⊢ ∀ x ∈ A B ⊆ C → ∀ y ∃* x ∈ A y ∈ C → ∀ y ∃* x ∈ A y ∈ B
6 df-disj ⊢ Disj x ∈ A C ↔ ∀ y ∃* x ∈ A y ∈ C
7 df-disj ⊢ Disj x ∈ A B ↔ ∀ y ∃* x ∈ A y ∈ B
8 5 6 7 3imtr4g ⊢ ∀ x ∈ A B ⊆ C → Disj x ∈ A C → Disj x ∈ A B