Theorem card2on 7486

Description: Proof that the alternate definition cardval2 7842 is always a set, and indeed is an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013.)

Assertion

Ref	Expression
card2on	|- { x e. On | x ~< A } e. On

Distinct variable group:   x, A

Proof of Theorem card2on

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		onelon 4574	. . . . . . . . . . . . 13 |- ( ( z e. On /\ y e. z ) -> y e. On )
2		vex 2927	. . . . . . . . . . . . . 14 |- z e. _V
3		onelss 4591	. . . . . . . . . . . . . . 15 |- ( z e. On -> ( y e. z -> y C_ z ) )
4	3	imp 419	. . . . . . . . . . . . . 14 |- ( ( z e. On /\ y e. z ) -> y C_ z )
5		ssdomg 7120	. . . . . . . . . . . . . 14 |- ( z e. _V -> ( y C_ z -> y ~<_ z ) )
6	2, 4, 5	mpsyl 61	. . . . . . . . . . . . 13 |- ( ( z e. On /\ y e. z ) -> y ~<_ z )
7	1, 6	jca 519	. . . . . . . . . . . 12 |- ( ( z e. On /\ y e. z ) -> ( y e. On /\ y ~<_ z ) )
8		domsdomtr 7209	. . . . . . . . . . . . . 14 |- ( ( y ~<_ z /\ z ~< A ) -> y ~< A )
9	8	anim2i 553	. . . . . . . . . . . . 13 |- ( ( y e. On /\ ( y ~<_ z /\ z ~< A ) ) -> ( y e. On /\ y ~< A ) )
10	9	anassrs 630	. . . . . . . . . . . 12 |- ( ( ( y e. On /\ y ~<_ z ) /\ z ~< A ) -> ( y e. On /\ y ~< A ) )
11	7, 10	sylan 458	. . . . . . . . . . 11 |- ( ( ( z e. On /\ y e. z ) /\ z ~< A ) -> ( y e. On /\ y ~< A ) )
12	11	exp31 588	. . . . . . . . . 10 |- ( z e. On -> ( y e. z -> ( z ~< A -> ( y e. On /\ y ~< A ) ) ) )
13	12	com12 29	. . . . . . . . 9 |- ( y e. z -> ( z e. On -> ( z ~< A -> ( y e. On /\ y ~< A ) ) ) )
14	13	imp3a 421	. . . . . . . 8 |- ( y e. z -> ( ( z e. On /\ z ~< A ) -> ( y e. On /\ y ~< A ) ) )
15		breq1 4183	. . . . . . . . 9 |- ( x = z -> ( x ~< A <-> z ~< A ) )
16	15	elrab 3060	. . . . . . . 8 |- ( z e. { x e. On | x ~< A } <-> ( z e. On /\ z ~< A ) )
17		breq1 4183	. . . . . . . . 9 |- ( x = y -> ( x ~< A <-> y ~< A ) )
18	17	elrab 3060	. . . . . . . 8 |- ( y e. { x e. On | x ~< A } <-> ( y e. On /\ y ~< A ) )
19	14, 16, 18	3imtr4g 262	. . . . . . 7 |- ( y e. z -> ( z e. { x e. On | x ~< A } -> y e. { x e. On | x ~< A } ) )
20	19	imp 419	. . . . . 6 |- ( ( y e. z /\ z e. { x e. On | x ~< A } ) -> y e. { x e. On | x ~< A } )
21	20	gen2 1553	. . . . 5 |- A. y A. z ( ( y e. z /\ z e. { x e. On | x ~< A } ) -> y e. { x e. On | x ~< A } )
22		dftr2 4272	. . . . 5 |- ( Tr { x e. On | x ~< A } <-> A. y A. z ( ( y e. z /\ z e. { x e. On | x ~< A } ) -> y e. { x e. On | x ~< A } ) )
23	21, 22	mpbir 201	. . . 4 |- Tr { x e. On | x ~< A }
24		ssrab2 3396	. . . 4 |- { x e. On | x ~< A } C_ On
25		ordon 4730	. . . 4 |- Ord On
26		trssord 4566	. . . 4 |- ( ( Tr { x e. On | x ~< A } /\ { x e. On | x ~< A } C_ On /\ Ord On ) -> Ord { x e. On | x ~< A } )
27	23, 24, 25, 26	mp3an 1279	. . 3 |- Ord { x e. On | x ~< A }
28		hartogs 7477	. . . 4 |- ( A e. _V -> { x e. On | x ~<_ A } e. On )
29		sdomdom 7102	. . . . . . 7 |- ( x ~< A -> x ~<_ A )
30	29	a1i 11	. . . . . 6 |- ( x e. On -> ( x ~< A -> x ~<_ A ) )
31	30	ss2rabi 3393	. . . . 5 |- { x e. On | x ~< A } C_ { x e. On | x ~<_ A }
32		ssexg 4317	. . . . 5 |- ( ( { x e. On | x ~< A } C_ { x e. On | x ~<_ A } /\ { x e. On | x ~<_ A } e. On ) -> { x e. On | x ~< A } e. _V )
33	31, 32	mpan 652	. . . 4 |- ( { x e. On | x ~<_ A } e. On -> { x e. On | x ~< A } e. _V )
34		elong 4557	. . . 4 |- ( { x e. On | x ~< A } e. _V -> ( { x e. On | x ~< A } e. On <-> Ord { x e. On | x ~< A } ) )
35	28, 33, 34	3syl 19	. . 3 |- ( A e. _V -> ( { x e. On | x ~< A } e. On <-> Ord { x e. On | x ~< A } ) )
36	27, 35	mpbiri 225	. 2 |- ( A e. _V -> { x e. On | x ~< A } e. On )
37		0elon 4602	. . . 4 |- (/) e. On
38		eleq1 2472	. . . 4 |- ( { x e. On | x ~< A } = (/) -> ( { x e. On | x ~< A } e. On <-> (/) e. On ) )
39	37, 38	mpbiri 225	. . 3 |- ( { x e. On | x ~< A } = (/) -> { x e. On | x ~< A } e. On )
40		df-ne 2577	. . . . 5 |- ( { x e. On | x ~< A } =/= (/) <-> -. { x e. On | x ~< A } = (/) )
41		rabn0 3615	. . . . 5 |- ( { x e. On | x ~< A } =/= (/) <-> E. x e. On x ~< A )
42	40, 41	bitr3i 243	. . . 4 |- ( -. { x e. On | x ~< A } = (/) <-> E. x e. On x ~< A )
43		relsdom 7083	. . . . . 6 |- Rel ~<
44	43	brrelex2i 4886	. . . . 5 |- ( x ~< A -> A e. _V )
45	44	rexlimivw 2794	. . . 4 |- ( E. x e. On x ~< A -> A e. _V )
46	42, 45	sylbi 188	. . 3 |- ( -. { x e. On | x ~< A } = (/) -> A e. _V )
47	39, 46	nsyl4 136	. 2 |- ( -. A e. _V -> { x e. On | x ~< A } e. On )
48	36, 47	pm2.61i 158	1 |- { x e. On | x ~< A } e. On

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   A.wal 1546   = wceq 1649   e. wcel 1721   =/= wne 2575   E.wrex 2675   {crab 2678   _Vcvv 2924   C_ wss 3288   (/)c0 3596   class class class wbr 4180   Tr wtr 4270   Ord word 4548   Oncon0 4549   ~<_ cdom 7074   ~< csdm 7075

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-rep 4288  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-rmo 2682  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-se 4510  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-isom 5430  df-riota 6516  df-recs 6600  df-er 6872  df-en 7077  df-dom 7078  df-sdom 7079  df-oi 7443