Description: The set A is an element of the smallest Tarski class that contains A . CLASSES1 th. 5. (Contributed by FL, 30-Dec-2010) (Proof shortened by Mario Carneiro, 21-Sep-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | tskmid | ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ ( tarskiMap ‘ 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | ⊢ ( 𝐴 ∈ 𝑥 → 𝐴 ∈ 𝑥 ) | |
| 2 | 1 | rgenw | ⊢ ∀ 𝑥 ∈ Tarski ( 𝐴 ∈ 𝑥 → 𝐴 ∈ 𝑥 ) |
| 3 | elintrabg | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } ↔ ∀ 𝑥 ∈ Tarski ( 𝐴 ∈ 𝑥 → 𝐴 ∈ 𝑥 ) ) ) | |
| 4 | 2 3 | mpbiri | ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ ∩ { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } ) |
| 5 | tskmval | ⊢ ( 𝐴 ∈ 𝑉 → ( tarskiMap ‘ 𝐴 ) = ∩ { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } ) | |
| 6 | 4 5 | eleqtrrd | ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ ( tarskiMap ‘ 𝐴 ) ) |