Metamath Proof Explorer

Theorem sstskm

Description: Being a part of ( tarskiMapA ) . (Contributed by FL, 17-Apr-2011) (Proof shortened by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion sstskm ⊢ A ∈ V → B ⊆ tarskiMap ⁡ A ↔ ∀ x ∈ Tarski A ∈ x → B ⊆ x

Proof

Step Hyp Ref Expression
1 tskmval ⊢ A ∈ V → tarskiMap ⁡ A = ⋂ x ∈ Tarski | A ∈ x
2 df-rab ⊢ x ∈ Tarski | A ∈ x = x | x ∈ Tarski ∧ A ∈ x
3 2 inteqi ⊢ ⋂ x ∈ Tarski | A ∈ x = ⋂ x | x ∈ Tarski ∧ A ∈ x
4 1 3 eqtrdi ⊢ A ∈ V → tarskiMap ⁡ A = ⋂ x | x ∈ Tarski ∧ A ∈ x
5 4 sseq2d ⊢ A ∈ V → B ⊆ tarskiMap ⁡ A ↔ B ⊆ ⋂ x | x ∈ Tarski ∧ A ∈ x
6 impexp ⊢ x ∈ Tarski ∧ A ∈ x → B ⊆ x ↔ x ∈ Tarski → A ∈ x → B ⊆ x
7 6 albii ⊢ ∀ x x ∈ Tarski ∧ A ∈ x → B ⊆ x ↔ ∀ x x ∈ Tarski → A ∈ x → B ⊆ x
8 ssintab ⊢ B ⊆ ⋂ x | x ∈ Tarski ∧ A ∈ x ↔ ∀ x x ∈ Tarski ∧ A ∈ x → B ⊆ x
9 df-ral ⊢ ∀ x ∈ Tarski A ∈ x → B ⊆ x ↔ ∀ x x ∈ Tarski → A ∈ x → B ⊆ x
10 7 8 9 3bitr4i ⊢ B ⊆ ⋂ x | x ∈ Tarski ∧ A ∈ x ↔ ∀ x ∈ Tarski A ∈ x → B ⊆ x
11 5 10 bitrdi ⊢ A ∈ V → B ⊆ tarskiMap ⁡ A ↔ ∀ x ∈ Tarski A ∈ x → B ⊆ x