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	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ On ∪ 𝐴 = suc 𝑏 → ∪ 𝐴 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		onsupnmax	⊢ ( 𝐴 ⊆ On → ( ¬ ∪ 𝐴 ∈ 𝐴 → ∪ 𝐴 = ∪ ∪ 𝐴 ) )
2		ssorduni	⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )
3		orduninsuc	⊢ ( Ord ∪ 𝐴 → ( ∪ 𝐴 = ∪ ∪ 𝐴 ↔ ¬ ∃ 𝑏 ∈ On ∪ 𝐴 = suc 𝑏 ) )
4	2 3	syl	⊢ ( 𝐴 ⊆ On → ( ∪ 𝐴 = ∪ ∪ 𝐴 ↔ ¬ ∃ 𝑏 ∈ On ∪ 𝐴 = suc 𝑏 ) )
5	1 4	sylibd	⊢ ( 𝐴 ⊆ On → ( ¬ ∪ 𝐴 ∈ 𝐴 → ¬ ∃ 𝑏 ∈ On ∪ 𝐴 = suc 𝑏 ) )
6	5	con4d	⊢ ( 𝐴 ⊆ On → ( ∃ 𝑏 ∈ On ∪ 𝐴 = suc 𝑏 → ∪ 𝐴 ∈ 𝐴 ) )
7	6	adantr	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ On ∪ 𝐴 = suc 𝑏 → ∪ 𝐴 ∈ 𝐴 ) )