This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Union Ordinals (continued) onsucuni
Description: A class of ordinal numbers is a subclass of the successor of its union.
Similar to Proposition 7.26 of TakeutiZaring p. 41. (Contributed by NM , 19-Sep-2003)
Ref
Expression
Assertion
onsucuni ⊢ ( 𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴 )
Proof
Step
Hyp
Ref
Expression
1
ssorduni ⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )
2
ssid ⊢ ∪ 𝐴 ⊆ ∪ 𝐴
3
ordunisssuc ⊢ ( ( 𝐴 ⊆ On ∧ Ord ∪ 𝐴 ) → ( ∪ 𝐴 ⊆ ∪ 𝐴 ↔ 𝐴 ⊆ suc ∪ 𝐴 ) )
4
2 3
mpbii ⊢ ( ( 𝐴 ⊆ On ∧ Ord ∪ 𝐴 ) → 𝐴 ⊆ suc ∪ 𝐴 )
5
1 4
mpdan ⊢ ( 𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴 )