# Metamath Proof Explorer

## 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}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}\right)\to {A}=\bigcap {B}\right)$

### Proof

Step Hyp Ref Expression
1 ssint ${⊢}{A}\subseteq \bigcap {B}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{A}\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}↔¬{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}↔¬{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}↔¬{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)↔\left({x}\in {B}\to ¬{x}\in {A}\right)\right)$
9 con2b ${⊢}\left({x}\in {B}\to ¬{x}\in {A}\right)↔\left({x}\in {A}\to ¬{x}\in {B}\right)$
10 8 9 syl6bb ${⊢}\left({B}\subseteq \mathrm{On}\wedge {A}\in {B}\right)\to \left(\left({x}\in {B}\to {A}\subseteq {x}\right)↔\left({x}\in {A}\to ¬{x}\in {B}\right)\right)$
11 10 ralbidv2 ${⊢}\left({B}\subseteq \mathrm{On}\wedge {A}\in {B}\right)\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{A}\subseteq {x}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}\right)$
12 1 11 syl5bb ${⊢}\left({B}\subseteq \mathrm{On}\wedge {A}\in {B}\right)\to \left({A}\subseteq \bigcap {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}\right)$
13 12 biimprd ${⊢}\left({B}\subseteq \mathrm{On}\wedge {A}\in {B}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{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}\phantom{\rule{.4em}{0ex}}¬{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}\phantom{\rule{.4em}{0ex}}¬{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}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}\right)\to \left({A}\subseteq \bigcap {B}\wedge \bigcap {B}\subseteq {A}\right)\right)$
19 eqss ${⊢}{A}=\bigcap {B}↔\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}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}\right)\to {A}=\bigcap {B}\right)$