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 ( 𝐴𝑉 → ( 𝐵 ∈ ( tarskiMap ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ Tarski ( 𝐴𝑥𝐵𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 tskmval ( 𝐴𝑉 → ( tarskiMap ‘ 𝐴 ) = { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } )
2 1 eleq2d ( 𝐴𝑉 → ( 𝐵 ∈ ( tarskiMap ‘ 𝐴 ) ↔ 𝐵 { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } ) )
3 elex ( 𝐵 { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } → 𝐵 ∈ V )
4 3 a1i ( 𝐴𝑉 → ( 𝐵 { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } → 𝐵 ∈ V ) )
5 tskmid ( 𝐴𝑉𝐴 ∈ ( tarskiMap ‘ 𝐴 ) )
6 tskmcl ( tarskiMap ‘ 𝐴 ) ∈ Tarski
7 eleq2 ( 𝑥 = ( tarskiMap ‘ 𝐴 ) → ( 𝐴𝑥𝐴 ∈ ( tarskiMap ‘ 𝐴 ) ) )
8 eleq2 ( 𝑥 = ( tarskiMap ‘ 𝐴 ) → ( 𝐵𝑥𝐵 ∈ ( tarskiMap ‘ 𝐴 ) ) )
9 7 8 imbi12d ( 𝑥 = ( tarskiMap ‘ 𝐴 ) → ( ( 𝐴𝑥𝐵𝑥 ) ↔ ( 𝐴 ∈ ( tarskiMap ‘ 𝐴 ) → 𝐵 ∈ ( tarskiMap ‘ 𝐴 ) ) ) )
10 9 rspcv ( ( tarskiMap ‘ 𝐴 ) ∈ Tarski → ( ∀ 𝑥 ∈ Tarski ( 𝐴𝑥𝐵𝑥 ) → ( 𝐴 ∈ ( tarskiMap ‘ 𝐴 ) → 𝐵 ∈ ( tarskiMap ‘ 𝐴 ) ) ) )
11 6 10 ax-mp ( ∀ 𝑥 ∈ Tarski ( 𝐴𝑥𝐵𝑥 ) → ( 𝐴 ∈ ( tarskiMap ‘ 𝐴 ) → 𝐵 ∈ ( tarskiMap ‘ 𝐴 ) ) )
12 5 11 syl5com ( 𝐴𝑉 → ( ∀ 𝑥 ∈ Tarski ( 𝐴𝑥𝐵𝑥 ) → 𝐵 ∈ ( tarskiMap ‘ 𝐴 ) ) )
13 elex ( 𝐵 ∈ ( tarskiMap ‘ 𝐴 ) → 𝐵 ∈ V )
14 12 13 syl6 ( 𝐴𝑉 → ( ∀ 𝑥 ∈ Tarski ( 𝐴𝑥𝐵𝑥 ) → 𝐵 ∈ V ) )
15 elintrabg ( 𝐵 ∈ V → ( 𝐵 { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } ↔ ∀ 𝑥 ∈ Tarski ( 𝐴𝑥𝐵𝑥 ) ) )
16 15 a1i ( 𝐴𝑉 → ( 𝐵 ∈ V → ( 𝐵 { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } ↔ ∀ 𝑥 ∈ Tarski ( 𝐴𝑥𝐵𝑥 ) ) ) )
17 4 14 16 pm5.21ndd ( 𝐴𝑉 → ( 𝐵 { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } ↔ ∀ 𝑥 ∈ Tarski ( 𝐴𝑥𝐵𝑥 ) ) )
18 2 17 bitrd ( 𝐴𝑉 → ( 𝐵 ∈ ( tarskiMap ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ Tarski ( 𝐴𝑥𝐵𝑥 ) ) )