Theorem onfisupcl

Description: Sufficient condition when the supremum of a set of ordinals is the maximum element of that set. See ordunifi . (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	onfisupcl	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∪ 𝐴 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ) → 𝐴 ⊆ On )
2		simprl	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ) → 𝐴 ∈ Fin )
3		simprr	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ) → 𝐴 ≠ ∅ )
4	1 2 3	3jca	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ) → ( 𝐴 ⊆ On ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) )
5		ordunifi	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∪ 𝐴 ∈ 𝐴 )
6	4 5	syl	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ) → ∪ 𝐴 ∈ 𝐴 )
7	6	ex	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∪ 𝐴 ∈ 𝐴 ) )