Description: A set whose successor belongs to a transitive class also belongs. (Contributed by NM, 5-Sep-2003) (Proof shortened by Andrew Salmon, 12-Aug-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | trsuc | ⊢ ( ( Tr 𝐴 ∧ suc 𝐵 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | trel | ⊢ ( Tr 𝐴 → ( ( 𝐵 ∈ suc 𝐵 ∧ suc 𝐵 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 ) ) | |
| 2 | sssucid | ⊢ 𝐵 ⊆ suc 𝐵 | |
| 3 | ssexg | ⊢ ( ( 𝐵 ⊆ suc 𝐵 ∧ suc 𝐵 ∈ 𝐴 ) → 𝐵 ∈ V ) | |
| 4 | 2 3 | mpan | ⊢ ( suc 𝐵 ∈ 𝐴 → 𝐵 ∈ V ) |
| 5 | sucidg | ⊢ ( 𝐵 ∈ V → 𝐵 ∈ suc 𝐵 ) | |
| 6 | 4 5 | syl | ⊢ ( suc 𝐵 ∈ 𝐴 → 𝐵 ∈ suc 𝐵 ) |
| 7 | 6 | ancri | ⊢ ( suc 𝐵 ∈ 𝐴 → ( 𝐵 ∈ suc 𝐵 ∧ suc 𝐵 ∈ 𝐴 ) ) |
| 8 | 1 7 | impel | ⊢ ( ( Tr 𝐴 ∧ suc 𝐵 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 ) |