Theorem rncardr1prc

Description: The Axiom of Choice implies that the cardinalities of the layers of the cumulative hierarchy form a proper class. (Contributed by BTernaryTau, 2-Jul-2026)

	Ref	Expression
Assertion	rncardr1prc	|- ( CHOICE -> -. ran ( card o. R1 ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		onprc	|- -. On e. _V
2		dfac10	|- ( CHOICE <-> dom card = _V )
3		df-card	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
4	3	funmpt2	|- Fun card
5		df-fn	|- ( card Fn _V <-> ( Fun card /\ dom card = _V ) )
6	4 5	mpbiran	|- ( card Fn _V <-> dom card = _V )
7	2 6	sylbb2	|- ( CHOICE -> card Fn _V )
8		r111	|- R1 : On -1-1-> _V
9		f1f	|- ( R1 : On -1-1-> _V -> R1 : On --> _V )
10	8 9	ax-mp	|- R1 : On --> _V
11		fnfco	|- ( ( card Fn _V /\ R1 : On --> _V ) -> ( card o. R1 ) Fn On )
12	7 10 11	sylancl	|- ( CHOICE -> ( card o. R1 ) Fn On )
13		dffn3	|- ( ( card o. R1 ) Fn On <-> ( card o. R1 ) : On --> ran ( card o. R1 ) )
14	12 13	sylib	|- ( CHOICE -> ( card o. R1 ) : On --> ran ( card o. R1 ) )
15		smobeth	|- Smo ( card o. R1 )
16		smo11	|- ( ( ( card o. R1 ) : On --> ran ( card o. R1 ) /\ Smo ( card o. R1 ) ) -> ( card o. R1 ) : On -1-1-> ran ( card o. R1 ) )
17	15 16	mpan2	|- ( ( card o. R1 ) : On --> ran ( card o. R1 ) -> ( card o. R1 ) : On -1-1-> ran ( card o. R1 ) )
18		f1dmex	|- ( ( ( card o. R1 ) : On -1-1-> ran ( card o. R1 ) /\ ran ( card o. R1 ) e. _V ) -> On e. _V )
19	18	ex	|- ( ( card o. R1 ) : On -1-1-> ran ( card o. R1 ) -> ( ran ( card o. R1 ) e. _V -> On e. _V ) )
20	14 17 19	3syl	|- ( CHOICE -> ( ran ( card o. R1 ) e. _V -> On e. _V ) )
21	1 20	mtoi	|- ( CHOICE -> -. ran ( card o. R1 ) e. _V )