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 C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> A = |^| B ) )

Proof

Step Hyp Ref Expression
1 ssint
 |-  ( A C_ |^| B <-> A. x e. B A C_ x )
2 ssel
 |-  ( B C_ On -> ( A e. B -> A e. On ) )
3 ssel
 |-  ( B C_ On -> ( x e. B -> x e. On ) )
4 2 3 anim12d
 |-  ( B C_ On -> ( ( A e. B /\ x e. B ) -> ( A e. On /\ x e. On ) ) )
5 ontri1
 |-  ( ( A e. On /\ x e. On ) -> ( A C_ x <-> -. x e. A ) )
6 4 5 syl6
 |-  ( B C_ On -> ( ( A e. B /\ x e. B ) -> ( A C_ x <-> -. x e. A ) ) )
7 6 expdimp
 |-  ( ( B C_ On /\ A e. B ) -> ( x e. B -> ( A C_ x <-> -. x e. A ) ) )
8 7 pm5.74d
 |-  ( ( B C_ On /\ A e. B ) -> ( ( x e. B -> A C_ x ) <-> ( x e. B -> -. x e. A ) ) )
9 con2b
 |-  ( ( x e. B -> -. x e. A ) <-> ( x e. A -> -. x e. B ) )
10 8 9 syl6bb
 |-  ( ( B C_ On /\ A e. B ) -> ( ( x e. B -> A C_ x ) <-> ( x e. A -> -. x e. B ) ) )
11 10 ralbidv2
 |-  ( ( B C_ On /\ A e. B ) -> ( A. x e. B A C_ x <-> A. x e. A -. x e. B ) )
12 1 11 syl5bb
 |-  ( ( B C_ On /\ A e. B ) -> ( A C_ |^| B <-> A. x e. A -. x e. B ) )
13 12 biimprd
 |-  ( ( B C_ On /\ A e. B ) -> ( A. x e. A -. x e. B -> A C_ |^| B ) )
14 13 expimpd
 |-  ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> A C_ |^| B ) )
15 intss1
 |-  ( A e. B -> |^| B C_ A )
16 15 a1i
 |-  ( B C_ On -> ( A e. B -> |^| B C_ A ) )
17 16 adantrd
 |-  ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> |^| B C_ A ) )
18 14 17 jcad
 |-  ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> ( A C_ |^| B /\ |^| B C_ A ) ) )
19 eqss
 |-  ( A = |^| B <-> ( A C_ |^| B /\ |^| B C_ A ) )
20 18 19 syl6ibr
 |-  ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> A = |^| B ) )