Description: A part of a Tarski class strictly dominated by the class is an element of the class. JFM CLASSES2 th. 2. (Contributed by FL, 22-Feb-2011) (Proof shortened by Mario Carneiro, 20-Sep-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | tskssel | ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇 ∧ 𝐴 ≺ 𝑇 ) → 𝐴 ∈ 𝑇 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sdomnen | ⊢ ( 𝐴 ≺ 𝑇 → ¬ 𝐴 ≈ 𝑇 ) | |
| 2 | 1 | 3ad2ant3 | ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇 ∧ 𝐴 ≺ 𝑇 ) → ¬ 𝐴 ≈ 𝑇 ) |
| 3 | tsken | ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇 ) → ( 𝐴 ≈ 𝑇 ∨ 𝐴 ∈ 𝑇 ) ) | |
| 4 | 3 | 3adant3 | ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇 ∧ 𝐴 ≺ 𝑇 ) → ( 𝐴 ≈ 𝑇 ∨ 𝐴 ∈ 𝑇 ) ) |
| 5 | 4 | ord | ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇 ∧ 𝐴 ≺ 𝑇 ) → ( ¬ 𝐴 ≈ 𝑇 → 𝐴 ∈ 𝑇 ) ) |
| 6 | 2 5 | mpd | ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇 ∧ 𝐴 ≺ 𝑇 ) → 𝐴 ∈ 𝑇 ) |