Metamath Proof Explorer

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 \subseteq On \land A \in V) \to ((A \in Fin \land A \neq \emptyset) \to ⋃ A \in A)$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \subseteq On \land A \in V) \land (A \in Fin \land A \neq \emptyset)) \to A \subseteq On$
2		simprl	$⊢ ((A \subseteq On \land A \in V) \land (A \in Fin \land A \neq \emptyset)) \to A \in Fin$
3		simprr	$⊢ ((A \subseteq On \land A \in V) \land (A \in Fin \land A \neq \emptyset)) \to A \neq \emptyset$
4	1 2 3	3jca	$⊢ ((A \subseteq On \land A \in V) \land (A \in Fin \land A \neq \emptyset)) \to (A \subseteq On \land A \in Fin \land A \neq \emptyset)$
5		ordunifi	$⊢ (A \subseteq On \land A \in Fin \land A \neq \emptyset) \to ⋃ A \in A$
6	4 5	syl	$⊢ ((A \subseteq On \land A \in V) \land (A \in Fin \land A \neq \emptyset)) \to ⋃ A \in A$
7	6	ex	$⊢ (A \subseteq On \land A \in V) \to ((A \in Fin \land A \neq \emptyset) \to ⋃ A \in A)$