oninfint

Description: The infimum of a non-empty class of ordinals is the intersection of that class. (Contributed by RP, 23-Jan-2025)

		Ref	Expression
	Assertion	oninfint	$⊢ (A \subseteq On \land A \neq \emptyset) \to inf (A, On, E) = ⋂ A$

Step	Hyp	Ref	Expression
1		epweon	$⊢ E We On$
2		weso	$⊢ E We On \to E Or On$
3	1 2	mp1i	$⊢ (A \subseteq On \land A \neq \emptyset) \to E Or On$
4		oninton	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋂ A \in On$
5		onint	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋂ A \in A$
6		intss1	$⊢ x \in A \to ⋂ A \subseteq x$
7	6	adantl	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in A) \to ⋂ A \subseteq x$
8		simpl	$⊢ (A \subseteq On \land A \neq \emptyset) \to A \subseteq On$
9	8	sselda	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in A) \to x \in On$
10		ontri1	$⊢ (⋂ A \in On \land x \in On) \to (⋂ A \subseteq x \leftrightarrow \neg x \in ⋂ A)$
11	4 9 10	syl2an2r	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in A) \to (⋂ A \subseteq x \leftrightarrow \neg x \in ⋂ A)$
12	7 11	mpbid	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in A) \to \neg x \in ⋂ A$
13		epelg	$⊢ ⋂ A \in On \to (x E ⋂ A \leftrightarrow x \in ⋂ A)$
14	4 13	syl	$⊢ (A \subseteq On \land A \neq \emptyset) \to (x E ⋂ A \leftrightarrow x \in ⋂ A)$
15	14	adantr	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in A) \to (x E ⋂ A \leftrightarrow x \in ⋂ A)$
16	12 15	mtbird	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in A) \to \neg x E ⋂ A$
17	3 4 5 16	infmin	$⊢ (A \subseteq On \land A \neq \emptyset) \to inf (A, On, E) = ⋂ A$

Metamath Proof Explorer