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

Metamath Proof Explorer

Theorem sbthlem3

Description: Lemma for sbth . (Contributed by NM, 22-Mar-1998)

Ref Expression
Hypotheses sbthlem.1 ⊢ A ∈ V
sbthlem.2 ⊢ D = x | x ⊆ A ∧ g B ∖ f x ⊆ A ∖ x
Assertion sbthlem3 ⊢ ran ⁡ g ⊆ A → g B ∖ f ⋃ D = A ∖ ⋃ D

Proof

Step Hyp Ref Expression
1 sbthlem.1 ⊢ A ∈ V
2 sbthlem.2 ⊢ D = x | x ⊆ A ∧ g B ∖ f x ⊆ A ∖ x
3 1 2 sbthlem2 ⊢ ran ⁡ g ⊆ A → A ∖ g B ∖ f ⋃ D ⊆ ⋃ D
4 1 2 sbthlem1 ⊢ ⋃ D ⊆ A ∖ g B ∖ f ⋃ D
5 3 4 jctil ⊢ ran ⁡ g ⊆ A → ⋃ D ⊆ A ∖ g B ∖ f ⋃ D ∧ A ∖ g B ∖ f ⋃ D ⊆ ⋃ D
6 eqss ⊢ ⋃ D = A ∖ g B ∖ f ⋃ D ↔ ⋃ D ⊆ A ∖ g B ∖ f ⋃ D ∧ A ∖ g B ∖ f ⋃ D ⊆ ⋃ D
7 5 6 sylibr ⊢ ran ⁡ g ⊆ A → ⋃ D = A ∖ g B ∖ f ⋃ D
8 7 difeq2d ⊢ ran ⁡ g ⊆ A → A ∖ ⋃ D = A ∖ A ∖ g B ∖ f ⋃ D
9 imassrn ⊢ g B ∖ f ⋃ D ⊆ ran ⁡ g
10 sstr2 ⊢ g B ∖ f ⋃ D ⊆ ran ⁡ g → ran ⁡ g ⊆ A → g B ∖ f ⋃ D ⊆ A
11 9 10 ax-mp ⊢ ran ⁡ g ⊆ A → g B ∖ f ⋃ D ⊆ A
12 dfss4 ⊢ g B ∖ f ⋃ D ⊆ A ↔ A ∖ A ∖ g B ∖ f ⋃ D = g B ∖ f ⋃ D
13 11 12 sylib ⊢ ran ⁡ g ⊆ A → A ∖ A ∖ g B ∖ f ⋃ D = g B ∖ f ⋃ D
14 8 13 eqtr2d ⊢ ran ⁡ g ⊆ A → g B ∖ f ⋃ D = A ∖ ⋃ D