Theorem onsupsucismax

Description: If the union of a set of ordinals is a successor ordinal, then that union is the maximum element of the set. This is not a bijection because sets where the maximum element is zero or a limit ordinal exist. Lemma 2.11 of Schloeder p. 5. (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	onsupsucismax	|- ( ( A C_ On /\ A e. V ) -> ( E. b e. On U. A = suc b -> U. A e. A ) )

Proof

Step	Hyp	Ref	Expression
1		onsupnmax	|- ( A C_ On -> ( -. U. A e. A -> U. A = U. U. A ) )
2		ssorduni	|- ( A C_ On -> Ord U. A )
3		orduninsuc	|- ( Ord U. A -> ( U. A = U. U. A <-> -. E. b e. On U. A = suc b ) )
4	2 3	syl	|- ( A C_ On -> ( U. A = U. U. A <-> -. E. b e. On U. A = suc b ) )
5	1 4	sylibd	|- ( A C_ On -> ( -. U. A e. A -> -. E. b e. On U. A = suc b ) )
6	5	con4d	|- ( A C_ On -> ( E. b e. On U. A = suc b -> U. A e. A ) )
7	6	adantr	|- ( ( A C_ On /\ A e. V ) -> ( E. b e. On U. A = suc b -> U. A e. A ) )