Theorem oneqmini 4871

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

Assertion

Ref	Expression
oneqmini	|- ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> A = |^| B ) )

Distinct variable groups:   x, A   x, B

Proof of Theorem oneqmini

Step	Hyp	Ref	Expression
1		ssint 4245	. . . . . 6 |- ( A C_ |^| B <-> A. x e. B A C_ x )
2		ssel 3451	. . . . . . . . . . . 12 |- ( B C_ On -> ( A e. B -> A e. On ) )
3		ssel 3451	. . . . . . . . . . . 12 |- ( B C_ On -> ( x e. B -> x e. On ) )
4	2, 3	anim12d 563	. . . . . . . . . . 11 |- ( B C_ On -> ( ( A e. B /\ x e. B ) -> ( A e. On /\ x e. On ) ) )
5		ontri1 4854	. . . . . . . . . . 11 |- ( ( A e. On /\ x e. On ) -> ( A C_ x <-> -. x e. A ) )
6	4, 5	syl6 33	. . . . . . . . . 10 |- ( B C_ On -> ( ( A e. B /\ x e. B ) -> ( A C_ x <-> -. x e. A ) ) )
7	6	expdimp 437	. . . . . . . . 9 |- ( ( B C_ On /\ A e. B ) -> ( x e. B -> ( A C_ x <-> -. x e. A ) ) )
8	7	pm5.74d 247	. . . . . . . 8 |- ( ( B C_ On /\ A e. B ) -> ( ( x e. B -> A C_ x ) <-> ( x e. B -> -. x e. A ) ) )
9		con2b 334	. . . . . . . 8 |- ( ( x e. B -> -. x e. A ) <-> ( x e. A -> -. x e. B ) )
10	8, 9	syl6bb 261	. . . . . . 7 |- ( ( B C_ On /\ A e. B ) -> ( ( x e. B -> A C_ x ) <-> ( x e. A -> -. x e. B ) ) )
11	10	ralbidv2 2830	. . . . . 6 |- ( ( B C_ On /\ A e. B ) -> ( A. x e. B A C_ x <-> A. x e. A -. x e. B ) )
12	1, 11	syl5bb 257	. . . . 5 |- ( ( B C_ On /\ A e. B ) -> ( A C_ |^| B <-> A. x e. A -. x e. B ) )
13	12	biimprd 223	. . . 4 |- ( ( B C_ On /\ A e. B ) -> ( A. x e. A -. x e. B -> A C_ |^| B ) )
14	13	expimpd 603	. . 3 |- ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> A C_ |^| B ) )
15		intss1 4244	. . . . 5 |- ( A e. B -> |^| B C_ A )
16	15	a1i 11	. . . 4 |- ( B C_ On -> ( A e. B -> |^| B C_ A ) )
17	16	adantrd 468	. . 3 |- ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> |^| B C_ A ) )
18	14, 17	jcad 533	. 2 |- ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> ( A C_ |^| B /\ |^| B C_ A ) ) )
19		eqss 3472	. 2 |- ( A = |^| B <-> ( A C_ |^| B /\ |^| B C_ A ) )
20	18, 19	syl6ibr 227	1 |- ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> A = |^| B ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1370   e. wcel 1758   A.wral 2795   C_ wss 3429   |^|cint 4229   Oncon0 4820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pr 4632

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-pss 3445  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-int 4230  df-br 4394  df-opab 4452  df-tr 4487  df-eprel 4733  df-po 4742  df-so 4743  df-fr 4780  df-we 4782  df-ord 4823  df-on 4824

This theorem is referenced by:  oneqmin  6519  alephval3  8384  cfsuc  8530  alephval2  8840