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	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 ) )