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 ∘ 𝑅1 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		onprc	⊢ ¬ On ∈ V
2		dfac10	⊢ ( CHOICE ↔ dom card = V )
3		df-card	⊢ card = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ 𝑥 } )
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	⊢ 𝑅1 : On –1-1→ V
9		f1f	⊢ ( 𝑅1 : On –1-1→ V → 𝑅1 : On ⟶ V )
10	8 9	ax-mp	⊢ 𝑅1 : On ⟶ V
11		fnfco	⊢ ( ( card Fn V ∧ 𝑅1 : On ⟶ V ) → ( card ∘ 𝑅1 ) Fn On )
12	7 10 11	sylancl	⊢ ( CHOICE → ( card ∘ 𝑅1 ) Fn On )
13		dffn3	⊢ ( ( card ∘ 𝑅1 ) Fn On ↔ ( card ∘ 𝑅1 ) : On ⟶ ran ( card ∘ 𝑅1 ) )
14	12 13	sylib	⊢ ( CHOICE → ( card ∘ 𝑅1 ) : On ⟶ ran ( card ∘ 𝑅1 ) )
15		smobeth	⊢ Smo ( card ∘ 𝑅1 )
16		smo11	⊢ ( ( ( card ∘ 𝑅1 ) : On ⟶ ran ( card ∘ 𝑅1 ) ∧ Smo ( card ∘ 𝑅1 ) ) → ( card ∘ 𝑅1 ) : On –1-1→ ran ( card ∘ 𝑅1 ) )
17	15 16	mpan2	⊢ ( ( card ∘ 𝑅1 ) : On ⟶ ran ( card ∘ 𝑅1 ) → ( card ∘ 𝑅1 ) : On –1-1→ ran ( card ∘ 𝑅1 ) )
18		f1dmex	⊢ ( ( ( card ∘ 𝑅1 ) : On –1-1→ ran ( card ∘ 𝑅1 ) ∧ ran ( card ∘ 𝑅1 ) ∈ V ) → On ∈ V )
19	18	ex	⊢ ( ( card ∘ 𝑅1 ) : On –1-1→ ran ( card ∘ 𝑅1 ) → ( ran ( card ∘ 𝑅1 ) ∈ V → On ∈ V ) )
20	14 17 19	3syl	⊢ ( CHOICE → ( ran ( card ∘ 𝑅1 ) ∈ V → On ∈ V ) )
21	1 20	mtoi	⊢ ( CHOICE → ¬ ran ( card ∘ 𝑅1 ) ∈ V )