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 \to \neg ran (card \circ R_{1}) \in V$

Proof

Step	Hyp	Ref	Expression
1		onprc	$⊢ \neg On \in V$
2		dfac10	$⊢ CHOICE \leftrightarrow dom card = V$
3		df-card	$⊢ card = (x \in V ⟼ ⋂ \{y \in On \| y \approx x\})$
4	3	funmpt2	$⊢ Fun card$
5		df-fn	$⊢ card Fn V \leftrightarrow (Fun card \land dom card = V)$
6	4 5	mpbiran	$⊢ card Fn V \leftrightarrow dom card = V$
7	2 6	sylbb2	$⊢ CHOICE \to card Fn V$
8		r111	$⊢ R_{1} : On \underset{1-1}{⟶} V$
9		f1f	$⊢ R_{1} : On \underset{1-1}{⟶} V \to R_{1} : On ⟶ V$
10	8 9	ax-mp	$⊢ R_{1} : On ⟶ V$
11		fnfco	$⊢ (card Fn V \land R_{1} : On ⟶ V) \to (card \circ R_{1}) Fn On$
12	7 10 11	sylancl	$⊢ CHOICE \to (card \circ R_{1}) Fn On$
13		dffn3	$⊢ (card \circ R_{1}) Fn On \leftrightarrow (card \circ R_{1}) : On ⟶ ran (card \circ R_{1})$
14	12 13	sylib	$⊢ CHOICE \to (card \circ R_{1}) : On ⟶ ran (card \circ R_{1})$
15		smobeth	$⊢ Smo (card \circ R_{1})$
16		smo11	$⊢ ((card \circ R_{1}) : On ⟶ ran (card \circ R_{1}) \land Smo (card \circ R_{1})) \to (card \circ R_{1}) : On \underset{1-1}{⟶} ran (card \circ R_{1})$
17	15 16	mpan2	$⊢ (card \circ R_{1}) : On ⟶ ran (card \circ R_{1}) \to (card \circ R_{1}) : On \underset{1-1}{⟶} ran (card \circ R_{1})$
18		f1dmex	$⊢ ((card \circ R_{1}) : On \underset{1-1}{⟶} ran (card \circ R_{1}) \land ran (card \circ R_{1}) \in V) \to On \in V$
19	18	ex	$⊢ (card \circ R_{1}) : On \underset{1-1}{⟶} ran (card \circ R_{1}) \to (ran (card \circ R_{1}) \in V \to On \in V)$
20	14 17 19	3syl	$⊢ CHOICE \to (ran (card \circ R_{1}) \in V \to On \in V)$
21	1 20	mtoi	$⊢ CHOICE \to \neg ran (card \circ R_{1}) \in V$

Metamath Proof Explorer

Theorem rncardr1prc

Proof