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 \| \exists x \in On (r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x))\}$
	Assertion	acwer1prc	$⊢ CHOICE \to \neg W \in V$

Proof

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

Metamath Proof Explorer

Theorem acwer1prc

Proof