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

Proof

Step Hyp Ref Expression
1 ssint A B x B A x
2 ssel B On A B A On
3 ssel B On x B x On
4 2 3 anim12d B On A B x B A On x On
5 ontri1 A On x On A x ¬ x A
6 4 5 syl6 B On A B x B A x ¬ x A
7 6 expdimp B On A B x B A x ¬ x A
8 7 pm5.74d B On A B x B A x x B ¬ x A
9 con2b x B ¬ x A x A ¬ x B
10 8 9 bitrdi B On A B x B A x x A ¬ x B
11 10 ralbidv2 B On A B x B A x x A ¬ x B
12 1 11 syl5bb B On A B A B x A ¬ x B
13 12 biimprd B On A B x A ¬ x B A B
14 13 expimpd B On A B x A ¬ x B A B
15 intss1 A B B A
16 15 a1i B On A B B A
17 16 adantrd B On A B x A ¬ x B B A
18 14 17 jcad B On A B x A ¬ x B A B B A
19 eqss A = B A B B A
20 18 19 syl6ibr B On A B x A ¬ x B A = B