Theorem acwer1prc

Description: The class of all well-orderings of the stages of the cumulative hierarchy is a proper class. (Contributed by BTernaryTau, 31-Jul-2026)

	Ref	Expression
Hypothesis	acwer1prc.1	|- W = { r | E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) }
Assertion	acwer1prc	|- ( CHOICE -> -. W e. _V )

Proof

Step	Hyp	Ref	Expression
1		acwer1prc.1	|- W = { r | E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) }
2		rncardr1prc	|- ( CHOICE -> -. ran ( card o. R1 ) e. _V )
3		omex	|- _om e. _V
4		difex2	|- ( _om e. _V -> ( ran ( card o. R1 ) e. _V <-> ( ran ( card o. R1 ) \ _om ) e. _V ) )
5	3 4	ax-mp	|- ( ran ( card o. R1 ) e. _V <-> ( ran ( card o. R1 ) \ _om ) e. _V )
6	2 5	sylnib	|- ( CHOICE -> -. ( ran ( card o. R1 ) \ _om ) e. _V )
7		simpl	|- ( ( CHOICE /\ y e. ( ( card " ran R1 ) \ _om ) ) -> CHOICE )
8		eldifn	|- ( y e. ( ( card " ran R1 ) \ _om ) -> -. y e. _om )
9		eldifi	|- ( y e. ( ( card " ran R1 ) \ _om ) -> y e. ( card " ran R1 ) )
10		imassrn	|- ( card " ran R1 ) C_ ran card
11	10	sseli	|- ( y e. ( card " ran R1 ) -> y e. ran card )
12		cardf2	|- card : { u | E. v e. On v ~~ u } --> On
13		frn	|- ( card : { u | E. v e. On v ~~ u } --> On -> ran card C_ On )
14	12 13	ax-mp	|- ran card C_ On
15	14	sseli	|- ( y e. ran card -> y e. On )
16	9 11 15	3syl	|- ( y e. ( ( card " ran R1 ) \ _om ) -> y e. On )
17		onfin	|- ( y e. On -> ( y e. Fin <-> y e. _om ) )
18	16 17	syl	|- ( y e. ( ( card " ran R1 ) \ _om ) -> ( y e. Fin <-> y e. _om ) )
19	8 18	mtbird	|- ( y e. ( ( card " ran R1 ) \ _om ) -> -. y e. Fin )
20		vex	|- y e. _V
21		acnum	|- ( CHOICE -> ( y e. _V -> y e. dom card ) )
22	20 21	mpi	|- ( CHOICE -> y e. dom card )
23		infinfnum	|- ( y e. dom card -> ( -. y e. Fin <-> _om ~<_ y ) )
24	22 23	syl	|- ( CHOICE -> ( -. y e. Fin <-> _om ~<_ y ) )
25	19 24	imbitrid	|- ( CHOICE -> ( y e. ( ( card " ran R1 ) \ _om ) -> _om ~<_ y ) )
26	25	imp	|- ( ( CHOICE /\ y e. ( ( card " ran R1 ) \ _om ) ) -> _om ~<_ y )
27		ffun	|- ( card : { u | E. v e. On v ~~ u } --> On -> Fun card )
28	12 27	ax-mp	|- Fun card
29		fvelima	|- ( ( Fun card /\ y e. ( card " ran R1 ) ) -> E. w e. ran R1 ( card ` w ) = y )
30	28 29	mpan	|- ( y e. ( card " ran R1 ) -> E. w e. ran R1 ( card ` w ) = y )
31		r1fnon	|- R1 Fn On
32		fnfun	|- ( R1 Fn On -> Fun R1 )
33		elrnrexdm	|- ( Fun R1 -> ( w e. ran R1 -> E. z e. dom R1 w = ( R1 ` z ) ) )
34	31 32 33	mp2b	|- ( w e. ran R1 -> E. z e. dom R1 w = ( R1 ` z ) )
35	31	fndmi	|- dom R1 = On
36	35	rexeqi	|- ( E. z e. dom R1 w = ( R1 ` z ) <-> E. z e. On w = ( R1 ` z ) )
37	34 36	sylib	|- ( w e. ran R1 -> E. z e. On w = ( R1 ` z ) )
38		rexex	|- ( E. z e. On w = ( R1 ` z ) -> E. z w = ( R1 ` z ) )
39	37 38	syl	|- ( w e. ran R1 -> E. z w = ( R1 ` z ) )
40		fveqeq2	|- ( w = ( R1 ` z ) -> ( ( card ` w ) = y <-> ( card ` ( R1 ` z ) ) = y ) )
41	40	biimpcd	|- ( ( card ` w ) = y -> ( w = ( R1 ` z ) -> ( card ` ( R1 ` z ) ) = y ) )
42	41	eximdv	|- ( ( card ` w ) = y -> ( E. z w = ( R1 ` z ) -> E. z ( card ` ( R1 ` z ) ) = y ) )
43	39 42	mpan9	|- ( ( w e. ran R1 /\ ( card ` w ) = y ) -> E. z ( card ` ( R1 ` z ) ) = y )
44	43	rexlimiva	|- ( E. w e. ran R1 ( card ` w ) = y -> E. z ( card ` ( R1 ` z ) ) = y )
45	9 30 44	3syl	|- ( y e. ( ( card " ran R1 ) \ _om ) -> E. z ( card ` ( R1 ` z ) ) = y )
46	45	adantl	|- ( ( CHOICE /\ y e. ( ( card " ran R1 ) \ _om ) ) -> E. z ( card ` ( R1 ` z ) ) = y )
47	7 26 46	3jca	|- ( ( CHOICE /\ y e. ( ( card " ran R1 ) \ _om ) ) -> ( CHOICE /\ _om ~<_ y /\ E. z ( card ` ( R1 ` z ) ) = y ) )
48	1	acwer1prclem	|- ( ( CHOICE /\ _om ~<_ y /\ ( card ` ( R1 ` z ) ) = y ) -> E. s ( ( card ` s ) e. ( card " W ) /\ ( card ` s ) = y ) )
49	48	3expia	|- ( ( CHOICE /\ _om ~<_ y ) -> ( ( card ` ( R1 ` z ) ) = y -> E. s ( ( card ` s ) e. ( card " W ) /\ ( card ` s ) = y ) ) )
50	49	exlimdv	|- ( ( CHOICE /\ _om ~<_ y ) -> ( E. z ( card ` ( R1 ` z ) ) = y -> E. s ( ( card ` s ) e. ( card " W ) /\ ( card ` s ) = y ) ) )
51	50	3impia	|- ( ( CHOICE /\ _om ~<_ y /\ E. z ( card ` ( R1 ` z ) ) = y ) -> E. s ( ( card ` s ) e. ( card " W ) /\ ( card ` s ) = y ) )
52		eleq1	|- ( ( card ` s ) = y -> ( ( card ` s ) e. ( card " W ) <-> y e. ( card " W ) ) )
53	52	biimpac	|- ( ( ( card ` s ) e. ( card " W ) /\ ( card ` s ) = y ) -> y e. ( card " W ) )
54	53	exlimiv	|- ( E. s ( ( card ` s ) e. ( card " W ) /\ ( card ` s ) = y ) -> y e. ( card " W ) )
55	47 51 54	3syl	|- ( ( CHOICE /\ y e. ( ( card " ran R1 ) \ _om ) ) -> y e. ( card " W ) )
56	55	ex	|- ( CHOICE -> ( y e. ( ( card " ran R1 ) \ _om ) -> y e. ( card " W ) ) )
57	56	ssrdv	|- ( CHOICE -> ( ( card " ran R1 ) \ _om ) C_ ( card " W ) )
58		rnco2	|- ran ( card o. R1 ) = ( card " ran R1 )
59	58	difeq1i	|- ( ran ( card o. R1 ) \ _om ) = ( ( card " ran R1 ) \ _om )
60		resima	|- ( ( card |` W ) " W ) = ( card " W )
61	57 59 60	3sstr4g	|- ( CHOICE -> ( ran ( card o. R1 ) \ _om ) C_ ( ( card |` W ) " W ) )
62		dfac10	|- ( CHOICE <-> dom card = _V )
63		df-fn	|- ( card Fn _V <-> ( Fun card /\ dom card = _V ) )
64	28 63	mpbiran	|- ( card Fn _V <-> dom card = _V )
65	62 64	sylbb2	|- ( CHOICE -> card Fn _V )
66		dffn2	|- ( card Fn _V <-> card : _V --> _V )
67	65 66	sylib	|- ( CHOICE -> card : _V --> _V )
68		ssv	|- W C_ _V
69		fssres	|- ( ( card : _V --> _V /\ W C_ _V ) -> ( card |` W ) : W --> _V )
70	67 68 69	sylancl	|- ( CHOICE -> ( card |` W ) : W --> _V )
71		fimadmfo	|- ( ( card |` W ) : W --> _V -> ( card |` W ) : W -onto-> ( ( card |` W ) " W ) )
72	70 71	syl	|- ( CHOICE -> ( card |` W ) : W -onto-> ( ( card |` W ) " W ) )
73		focdmex	|- ( W e. _V -> ( ( card |` W ) : W -onto-> ( ( card |` W ) " W ) -> ( ( card |` W ) " W ) e. _V ) )
74	72 73	syl5com	|- ( CHOICE -> ( W e. _V -> ( ( card |` W ) " W ) e. _V ) )
75		ssexg	|- ( ( ( ran ( card o. R1 ) \ _om ) C_ ( ( card |` W ) " W ) /\ ( ( card |` W ) " W ) e. _V ) -> ( ran ( card o. R1 ) \ _om ) e. _V )
76	61 74 75	syl6an	|- ( CHOICE -> ( W e. _V -> ( ran ( card o. R1 ) \ _om ) e. _V ) )
77	6 76	mtod	|- ( CHOICE -> -. W e. _V )