This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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