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 On B A = B A B x A ¬ x B

Proof

Step Hyp Ref Expression
1 onint B On B B B
2 eleq1 A = B A B B B
3 1 2 syl5ibrcom B On B A = B A B
4 eleq2 A = B x A x B
5 4 biimpd A = B x A x B
6 onnmin B On x B ¬ x B
7 6 ex B On x B ¬ x B
8 7 con2d B On x B ¬ x B
9 5 8 syl9r B On A = B x A ¬ x B
10 9 ralrimdv B On A = B x A ¬ x B
11 10 adantr B On B A = B x A ¬ x B
12 3 11 jcad B On B A = B A B x A ¬ x B
13 oneqmini B On A B x A ¬ x B A = B
14 13 adantr B On B A B x A ¬ x B A = B
15 12 14 impbid B On B A = B A B x A ¬ x B