This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem onsucssi

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

	Ref	Expression
Hypotheses	onssi.1	⊢ 𝐴 ∈ On
	onsucssi.2	⊢ 𝐵 ∈ On
Assertion	onsucssi	⊢ ( 𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		onssi.1	⊢ 𝐴 ∈ On
2		onsucssi.2	⊢ 𝐵 ∈ On
3	2	onordi	⊢ Ord 𝐵
4		ordelsuc	⊢ ( ( 𝐴 ∈ On ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵 ) )
5	1 3 4	mp2an	⊢ ( 𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵 )