Theorem oneqmini

Description: A way to show that an ordinal number equals the minimum of a 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	oneqmini	$$⊢B\subseteq \mathrm{On}\to \left(\left(A\in B\wedge \forall x\in A\neg x\in B\right)\to A=\bigcap B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssint	$$⊢A\subseteq \bigcap B\leftrightarrow \forall x\in BA\subseteq x$$
2		ssel	$$⊢B\subseteq \mathrm{On}\to \left(A\in B\to A\in \mathrm{On}\right)$$
3		ssel	$$⊢B\subseteq \mathrm{On}\to \left(x\in B\to x\in \mathrm{On}\right)$$
4	2 3	anim12d	$$⊢B\subseteq \mathrm{On}\to \left(\left(A\in B\wedge x\in B\right)\to \left(A\in \mathrm{On}\wedge x\in \mathrm{On}\right)\right)$$
5		ontri1	$$⊢\left(A\in \mathrm{On}\wedge x\in \mathrm{On}\right)\to \left(A\subseteq x\leftrightarrow \neg x\in A\right)$$
6	4 5	syl6	$$⊢B\subseteq \mathrm{On}\to \left(\left(A\in B\wedge x\in B\right)\to \left(A\subseteq x\leftrightarrow \neg x\in A\right)\right)$$
7	6	expdimp	$$⊢\left(B\subseteq \mathrm{On}\wedge A\in B\right)\to \left(x\in B\to \left(A\subseteq x\leftrightarrow \neg x\in A\right)\right)$$
8	7	pm5.74d	$$⊢\left(B\subseteq \mathrm{On}\wedge A\in B\right)\to \left(\left(x\in B\to A\subseteq x\right)\leftrightarrow \left(x\in B\to \neg x\in A\right)\right)$$
9		con2b	$$⊢\left(x\in B\to \neg x\in A\right)\leftrightarrow \left(x\in A\to \neg x\in B\right)$$
10	8 9	bitrdi	$$⊢\left(B\subseteq \mathrm{On}\wedge A\in B\right)\to \left(\left(x\in B\to A\subseteq x\right)\leftrightarrow \left(x\in A\to \neg x\in B\right)\right)$$
11	10	ralbidv2	$$⊢\left(B\subseteq \mathrm{On}\wedge A\in B\right)\to \left(\forall x\in BA\subseteq x\leftrightarrow \forall x\in A\neg x\in B\right)$$
12	1 11	bitrid	$$⊢\left(B\subseteq \mathrm{On}\wedge A\in B\right)\to \left(A\subseteq \bigcap B\leftrightarrow \forall x\in A\neg x\in B\right)$$
13	12	biimprd	$$⊢\left(B\subseteq \mathrm{On}\wedge A\in B\right)\to \left(\forall x\in A\neg x\in B\to A\subseteq \bigcap B\right)$$
14	13	expimpd	$$⊢B\subseteq \mathrm{On}\to \left(\left(A\in B\wedge \forall x\in A\neg x\in B\right)\to A\subseteq \bigcap B\right)$$
15		intss1	$$⊢A\in B\to \bigcap B\subseteq A$$
16	15	a1i	$$⊢B\subseteq \mathrm{On}\to \left(A\in B\to \bigcap B\subseteq A\right)$$
17	16	adantrd	$$⊢B\subseteq \mathrm{On}\to \left(\left(A\in B\wedge \forall x\in A\neg x\in B\right)\to \bigcap B\subseteq A\right)$$
18	14 17	jcad	$$⊢B\subseteq \mathrm{On}\to \left(\left(A\in B\wedge \forall x\in A\neg x\in B\right)\to \left(A\subseteq \bigcap B\wedge \bigcap B\subseteq A\right)\right)$$
19		eqss	$$⊢A=\bigcap B\leftrightarrow \left(A\subseteq \bigcap B\wedge \bigcap B\subseteq A\right)$$
20	18 19	syl6ibr	$$⊢B\subseteq \mathrm{On}\to \left(\left(A\in B\wedge \forall x\in A\neg x\in B\right)\to A=\bigcap B\right)$$