Metamath Proof Explorer

Theorem oneqmin

Description: A way to show that an ordinal number equals the minimum of a nonempty collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection. (Contributed by NM, 14-Nov-2003)

		Ref	Expression
	Assertion	oneqmin	$⊢ (B \subseteq On \land B \neq \emptyset) \to (A = ⋂ B \leftrightarrow (A \in B \land \forall x \in A \neg x \in B))$

Proof

Step	Hyp	Ref	Expression
1		onint	$⊢ (B \subseteq On \land B \neq \emptyset) \to ⋂ B \in B$
2		eleq1	$⊢ A = ⋂ B \to (A \in B \leftrightarrow ⋂ B \in B)$
3	1 2	syl5ibrcom	$⊢ (B \subseteq On \land B \neq \emptyset) \to (A = ⋂ B \to A \in B)$
4		eleq2	$⊢ A = ⋂ B \to (x \in A \leftrightarrow x \in ⋂ B)$
5	4	biimpd	$⊢ A = ⋂ B \to (x \in A \to x \in ⋂ B)$
6		onnmin	$⊢ (B \subseteq On \land x \in B) \to \neg x \in ⋂ B$
7	6	ex	$⊢ B \subseteq On \to (x \in B \to \neg x \in ⋂ B)$
8	7	con2d	$⊢ B \subseteq On \to (x \in ⋂ B \to \neg x \in B)$
9	5 8	syl9r	$⊢ B \subseteq On \to (A = ⋂ B \to (x \in A \to \neg x \in B))$
10	9	ralrimdv	$⊢ B \subseteq On \to (A = ⋂ B \to \forall x \in A \neg x \in B)$
11	10	adantr	$⊢ (B \subseteq On \land B \neq \emptyset) \to (A = ⋂ B \to \forall x \in A \neg x \in B)$
12	3 11	jcad	$⊢ (B \subseteq On \land B \neq \emptyset) \to (A = ⋂ B \to (A \in B \land \forall x \in A \neg x \in B))$
13		oneqmini	$⊢ B \subseteq On \to ((A \in B \land \forall x \in A \neg x \in B) \to A = ⋂ B)$
14	13	adantr	$⊢ (B \subseteq On \land B \neq \emptyset) \to ((A \in B \land \forall x \in A \neg x \in B) \to A = ⋂ B)$
15	12 14	impbid	$⊢ (B \subseteq On \land B \neq \emptyset) \to (A = ⋂ B \leftrightarrow (A \in B \land \forall x \in A \neg x \in B))$