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	|- ( ( A C_ On /\ A e. V ) -> ( ( A e. Fin /\ A =/= (/) ) -> U. A e. A ) )

Proof

Step	Hyp	Ref	Expression
1		simpll	|- ( ( ( A C_ On /\ A e. V ) /\ ( A e. Fin /\ A =/= (/) ) ) -> A C_ On )
2		simprl	|- ( ( ( A C_ On /\ A e. V ) /\ ( A e. Fin /\ A =/= (/) ) ) -> A e. Fin )
3		simprr	|- ( ( ( A C_ On /\ A e. V ) /\ ( A e. Fin /\ A =/= (/) ) ) -> A =/= (/) )
4	1 2 3	3jca	|- ( ( ( A C_ On /\ A e. V ) /\ ( A e. Fin /\ A =/= (/) ) ) -> ( A C_ On /\ A e. Fin /\ A =/= (/) ) )
5		ordunifi	|- ( ( A C_ On /\ A e. Fin /\ A =/= (/) ) -> U. A e. A )
6	4 5	syl	|- ( ( ( A C_ On /\ A e. V ) /\ ( A e. Fin /\ A =/= (/) ) ) -> U. A e. A )
7	6	ex	|- ( ( A C_ On /\ A e. V ) -> ( ( A e. Fin /\ A =/= (/) ) -> U. A e. A ) )