Theorem ordelsuc

Description: A set belongs to an ordinal iff its successor is a subset of the ordinal. Exercise 8 of TakeutiZaring p. 42 and its converse. (Contributed by NM, 29-Nov-2003)

	Ref	Expression
Assertion	ordelsuc	⊢ ( ( 𝐴 ∈ 𝐶 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ordsucss	⊢ ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
2	1	adantl	⊢ ( ( 𝐴 ∈ 𝐶 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
3		sucssel	⊢ ( 𝐴 ∈ 𝐶 → ( suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵 ) )
4	3	adantr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ Ord 𝐵 ) → ( suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵 ) )
5	2 4	impbid	⊢ ( ( 𝐴 ∈ 𝐶 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵 ) )