Metamath Proof Explorer

Theorem eltskm

Description: Belonging to ( tarskiMapA ) . (Contributed by FL, 17-Apr-2011) (Proof shortened by Mario Carneiro, 21-Sep-2014)

Ref Expression
Assertion eltskm ⊢ 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 1 eleq2d ⊢ A ∈ V → B ∈ tarskiMap ⁡ A ↔ B ∈ ⋂ x ∈ Tarski | A ∈ x
3 elex ⊢ B ∈ ⋂ x ∈ Tarski | A ∈ x → B ∈ V
4 3 a1i ⊢ A ∈ V → B ∈ ⋂ x ∈ Tarski | A ∈ x → B ∈ V
5 tskmid ⊢ A ∈ V → A ∈ tarskiMap ⁡ A
6 tskmcl ⊢ tarskiMap ⁡ A ∈ Tarski
7 eleq2 ⊢ x = tarskiMap ⁡ A → A ∈ x ↔ A ∈ tarskiMap ⁡ A
8 eleq2 ⊢ x = tarskiMap ⁡ A → B ∈ x ↔ B ∈ tarskiMap ⁡ A
9 7 8 imbi12d ⊢ x = tarskiMap ⁡ A → A ∈ x → B ∈ x ↔ A ∈ tarskiMap ⁡ A → B ∈ tarskiMap ⁡ A
10 9 rspcv ⊢ tarskiMap ⁡ A ∈ Tarski → ∀ x ∈ Tarski A ∈ x → B ∈ x → A ∈ tarskiMap ⁡ A → B ∈ tarskiMap ⁡ A
11 6 10 ax-mp ⊢ ∀ x ∈ Tarski A ∈ x → B ∈ x → A ∈ tarskiMap ⁡ A → B ∈ tarskiMap ⁡ A
12 5 11 syl5com ⊢ A ∈ V → ∀ x ∈ Tarski A ∈ x → B ∈ x → B ∈ tarskiMap ⁡ A
13 elex ⊢ B ∈ tarskiMap ⁡ A → B ∈ V
14 12 13 syl6 ⊢ A ∈ V → ∀ x ∈ Tarski A ∈ x → B ∈ x → B ∈ V
15 elintrabg ⊢ B ∈ V → B ∈ ⋂ x ∈ Tarski | A ∈ x ↔ ∀ x ∈ Tarski A ∈ x → B ∈ x
16 15 a1i ⊢ A ∈ V → B ∈ V → B ∈ ⋂ x ∈ Tarski | A ∈ x ↔ ∀ x ∈ Tarski A ∈ x → B ∈ x
17 4 14 16 pm5.21ndd ⊢ A ∈ V → B ∈ ⋂ x ∈ Tarski | A ∈ x ↔ ∀ x ∈ Tarski A ∈ x → B ∈ x
18 2 17 bitrd ⊢ A ∈ V → B ∈ tarskiMap ⁡ A ↔ ∀ x ∈ Tarski A ∈ x → B ∈ x