Metamath Proof Explorer

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 ⊢ 𝑊 = { 𝑟 ∣ ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) }
Assertion acwer1prc ( CHOICE → ¬ 𝑊 ∈ V )

Proof

Step Hyp Ref Expression
1 acwer1prc.1 ⊢ 𝑊 = { 𝑟 ∣ ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) }
2 rncardr1prc ⊢ ( CHOICE → ¬ ran ( card ∘ 𝑅1 ) ∈ V )
3 omex ⊢ ω ∈ V
4 difex2 ⊢ ( ω ∈ V → ( ran ( card ∘ 𝑅1 ) ∈ V ↔ ( ran ( card ∘ 𝑅1 ) ∖ ω ) ∈ V ) )
5 3 4 ax-mp ⊢ ( ran ( card ∘ 𝑅1 ) ∈ V ↔ ( ran ( card ∘ 𝑅1 ) ∖ ω ) ∈ V )
6 2 5 sylnib ⊢ ( CHOICE → ¬ ( ran ( card ∘ 𝑅1 ) ∖ ω ) ∈ V )
7 simpl ⊢ ( ( CHOICE ∧ 𝑦 ∈ ( ( card “ ran 𝑅1 ) ∖ ω ) ) → CHOICE )
8 eldifn ⊢ ( 𝑦 ∈ ( ( card “ ran 𝑅1 ) ∖ ω ) → ¬ 𝑦 ∈ ω )
9 eldifi ⊢ ( 𝑦 ∈ ( ( card “ ran 𝑅1 ) ∖ ω ) → 𝑦 ∈ ( card “ ran 𝑅1 ) )
10 imassrn ⊢ ( card “ ran 𝑅1 ) ⊆ ran card
11 10 sseli ⊢ ( 𝑦 ∈ ( card “ ran 𝑅1 ) → 𝑦 ∈ ran card )
12 cardf2 ⊢ card : { 𝑢 ∣ ∃ 𝑣 ∈ On 𝑣 ≈ 𝑢 } ⟶ On
13 frn ⊢ ( card : { 𝑢 ∣ ∃ 𝑣 ∈ On 𝑣 ≈ 𝑢 } ⟶ On → ran card ⊆ On )
14 12 13 ax-mp ⊢ ran card ⊆ On
15 14 sseli ⊢ ( 𝑦 ∈ ran card → 𝑦 ∈ On )
16 9 11 15 3syl ⊢ ( 𝑦 ∈ ( ( card “ ran 𝑅1 ) ∖ ω ) → 𝑦 ∈ On )
17 onfin ⊢ ( 𝑦 ∈ On → ( 𝑦 ∈ Fin ↔ 𝑦 ∈ ω ) )
18 16 17 syl ⊢ ( 𝑦 ∈ ( ( card “ ran 𝑅1 ) ∖ ω ) → ( 𝑦 ∈ Fin ↔ 𝑦 ∈ ω ) )
19 8 18 mtbird ⊢ ( 𝑦 ∈ ( ( card “ ran 𝑅1 ) ∖ ω ) → ¬ 𝑦 ∈ Fin )
20 vex ⊢ 𝑦 ∈ V
21 acnum ⊢ ( CHOICE → ( 𝑦 ∈ V → 𝑦 ∈ dom card ) )
22 20 21 mpi ⊢ ( CHOICE → 𝑦 ∈ dom card )
23 infinfnum ⊢ ( 𝑦 ∈ dom card → ( ¬ 𝑦 ∈ Fin ↔ ω ≼ 𝑦 ) )
24 22 23 syl ⊢ ( CHOICE → ( ¬ 𝑦 ∈ Fin ↔ ω ≼ 𝑦 ) )
25 19 24 imbitrid ⊢ ( CHOICE → ( 𝑦 ∈ ( ( card “ ran 𝑅1 ) ∖ ω ) → ω ≼ 𝑦 ) )
26 25 imp ⊢ ( ( CHOICE ∧ 𝑦 ∈ ( ( card “ ran 𝑅1 ) ∖ ω ) ) → ω ≼ 𝑦 )
27 ffun ⊢ ( card : { 𝑢 ∣ ∃ 𝑣 ∈ On 𝑣 ≈ 𝑢 } ⟶ On → Fun card )
28 12 27 ax-mp ⊢ Fun card
29 fvelima ⊢ ( ( Fun card ∧ 𝑦 ∈ ( card “ ran 𝑅1 ) ) → ∃ 𝑤 ∈ ran 𝑅1 ( card ‘ 𝑤 ) = 𝑦 )
30 28 29 mpan ⊢ ( 𝑦 ∈ ( card “ ran 𝑅1 ) → ∃ 𝑤 ∈ ran 𝑅1 ( card ‘ 𝑤 ) = 𝑦 )
31 r1fnon ⊢ 𝑅1 Fn On
32 fnfun ⊢ ( 𝑅1 Fn On → Fun 𝑅1 )
33 elrnrexdm ⊢ ( Fun 𝑅1 → ( 𝑤 ∈ ran 𝑅1 → ∃ 𝑧 ∈ dom 𝑅1 𝑤 = ( 𝑅1 ‘ 𝑧 ) ) )
34 31 32 33 mp2b ⊢ ( 𝑤 ∈ ran 𝑅1 → ∃ 𝑧 ∈ dom 𝑅1 𝑤 = ( 𝑅1 ‘ 𝑧 ) )
35 31 fndmi ⊢ dom 𝑅1 = On
36 35 rexeqi ⊢ ( ∃ 𝑧 ∈ dom 𝑅1 𝑤 = ( 𝑅1 ‘ 𝑧 ) ↔ ∃ 𝑧 ∈ On 𝑤 = ( 𝑅1 ‘ 𝑧 ) )
37 34 36 sylib ⊢ ( 𝑤 ∈ ran 𝑅1 → ∃ 𝑧 ∈ On 𝑤 = ( 𝑅1 ‘ 𝑧 ) )
38 rexex ⊢ ( ∃ 𝑧 ∈ On 𝑤 = ( 𝑅1 ‘ 𝑧 ) → ∃ 𝑧 𝑤 = ( 𝑅1 ‘ 𝑧 ) )
39 37 38 syl ⊢ ( 𝑤 ∈ ran 𝑅1 → ∃ 𝑧 𝑤 = ( 𝑅1 ‘ 𝑧 ) )
40 fveqeq2 ⊢ ( 𝑤 = ( 𝑅1 ‘ 𝑧 ) → ( ( card ‘ 𝑤 ) = 𝑦 ↔ ( card ‘ ( 𝑅1 ‘ 𝑧 ) ) = 𝑦 ) )
41 40 biimpcd ⊢ ( ( card ‘ 𝑤 ) = 𝑦 → ( 𝑤 = ( 𝑅1 ‘ 𝑧 ) → ( card ‘ ( 𝑅1 ‘ 𝑧 ) ) = 𝑦 ) )
42 41 eximdv ⊢ ( ( card ‘ 𝑤 ) = 𝑦 → ( ∃ 𝑧 𝑤 = ( 𝑅1 ‘ 𝑧 ) → ∃ 𝑧 ( card ‘ ( 𝑅1 ‘ 𝑧 ) ) = 𝑦 ) )
43 39 42 mpan9 ⊢ ( ( 𝑤 ∈ ran 𝑅1 ∧ ( card ‘ 𝑤 ) = 𝑦 ) → ∃ 𝑧 ( card ‘ ( 𝑅1 ‘ 𝑧 ) ) = 𝑦 )
44 43 rexlimiva ⊢ ( ∃ 𝑤 ∈ ran 𝑅1 ( card ‘ 𝑤 ) = 𝑦 → ∃ 𝑧 ( card ‘ ( 𝑅1 ‘ 𝑧 ) ) = 𝑦 )
45 9 30 44 3syl ⊢ ( 𝑦 ∈ ( ( card “ ran 𝑅1 ) ∖ ω ) → ∃ 𝑧 ( card ‘ ( 𝑅1 ‘ 𝑧 ) ) = 𝑦 )
46 45 adantl ⊢ ( ( CHOICE ∧ 𝑦 ∈ ( ( card “ ran 𝑅1 ) ∖ ω ) ) → ∃ 𝑧 ( card ‘ ( 𝑅1 ‘ 𝑧 ) ) = 𝑦 )
47 7 26 46 3jca ⊢ ( ( CHOICE ∧ 𝑦 ∈ ( ( card “ ran 𝑅1 ) ∖ ω ) ) → ( CHOICE ∧ ω ≼ 𝑦 ∧ ∃ 𝑧 ( card ‘ ( 𝑅1 ‘ 𝑧 ) ) = 𝑦 ) )
48 1 acwer1prclem ⊢ ( ( CHOICE ∧ ω ≼ 𝑦 ∧ ( card ‘ ( 𝑅1 ‘ 𝑧 ) ) = 𝑦 ) → ∃ 𝑠 ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ∧ ( card ‘ 𝑠 ) = 𝑦 ) )
49 48 3expia ⊢ ( ( CHOICE ∧ ω ≼ 𝑦 ) → ( ( card ‘ ( 𝑅1 ‘ 𝑧 ) ) = 𝑦 → ∃ 𝑠 ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ∧ ( card ‘ 𝑠 ) = 𝑦 ) ) )
50 49 exlimdv ⊢ ( ( CHOICE ∧ ω ≼ 𝑦 ) → ( ∃ 𝑧 ( card ‘ ( 𝑅1 ‘ 𝑧 ) ) = 𝑦 → ∃ 𝑠 ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ∧ ( card ‘ 𝑠 ) = 𝑦 ) ) )
51 50 3impia ⊢ ( ( CHOICE ∧ ω ≼ 𝑦 ∧ ∃ 𝑧 ( card ‘ ( 𝑅1 ‘ 𝑧 ) ) = 𝑦 ) → ∃ 𝑠 ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ∧ ( card ‘ 𝑠 ) = 𝑦 ) )
52 eleq1 ⊢ ( ( card ‘ 𝑠 ) = 𝑦 → ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ↔ 𝑦 ∈ ( card “ 𝑊 ) ) )
53 52 biimpac ⊢ ( ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ∧ ( card ‘ 𝑠 ) = 𝑦 ) → 𝑦 ∈ ( card “ 𝑊 ) )
54 53 exlimiv ⊢ ( ∃ 𝑠 ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ∧ ( card ‘ 𝑠 ) = 𝑦 ) → 𝑦 ∈ ( card “ 𝑊 ) )
55 47 51 54 3syl ⊢ ( ( CHOICE ∧ 𝑦 ∈ ( ( card “ ran 𝑅1 ) ∖ ω ) ) → 𝑦 ∈ ( card “ 𝑊 ) )
56 55 ex ⊢ ( CHOICE → ( 𝑦 ∈ ( ( card “ ran 𝑅1 ) ∖ ω ) → 𝑦 ∈ ( card “ 𝑊 ) ) )
57 56 ssrdv ⊢ ( CHOICE → ( ( card “ ran 𝑅1 ) ∖ ω ) ⊆ ( card “ 𝑊 ) )
58 rnco2 ⊢ ran ( card ∘ 𝑅1 ) = ( card “ ran 𝑅1 )
59 58 difeq1i ⊢ ( ran ( card ∘ 𝑅1 ) ∖ ω ) = ( ( card “ ran 𝑅1 ) ∖ ω )
60 resima ⊢ ( ( card ↾ 𝑊 ) “ 𝑊 ) = ( card “ 𝑊 )
61 57 59 60 3sstr4g ⊢ ( CHOICE → ( ran ( card ∘ 𝑅1 ) ∖ ω ) ⊆ ( ( card ↾ 𝑊 ) “ 𝑊 ) )
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 ⊢ 𝑊 ⊆ V
69 fssres ⊢ ( ( card : V ⟶ V ∧ 𝑊 ⊆ V ) → ( card ↾ 𝑊 ) : 𝑊 ⟶ V )
70 67 68 69 sylancl ⊢ ( CHOICE → ( card ↾ 𝑊 ) : 𝑊 ⟶ V )
71 fimadmfo ⊢ ( ( card ↾ 𝑊 ) : 𝑊 ⟶ V → ( card ↾ 𝑊 ) : 𝑊 –onto→ ( ( card ↾ 𝑊 ) “ 𝑊 ) )
72 70 71 syl ⊢ ( CHOICE → ( card ↾ 𝑊 ) : 𝑊 –onto→ ( ( card ↾ 𝑊 ) “ 𝑊 ) )
73 focdmex ⊢ ( 𝑊 ∈ V → ( ( card ↾ 𝑊 ) : 𝑊 –onto→ ( ( card ↾ 𝑊 ) “ 𝑊 ) → ( ( card ↾ 𝑊 ) “ 𝑊 ) ∈ V ) )
74 72 73 syl5com ⊢ ( CHOICE → ( 𝑊 ∈ V → ( ( card ↾ 𝑊 ) “ 𝑊 ) ∈ V ) )
75 ssexg ⊢ ( ( ( ran ( card ∘ 𝑅1 ) ∖ ω ) ⊆ ( ( card ↾ 𝑊 ) “ 𝑊 ) ∧ ( ( card ↾ 𝑊 ) “ 𝑊 ) ∈ V ) → ( ran ( card ∘ 𝑅1 ) ∖ ω ) ∈ V )
76 61 74 75 syl6an ⊢ ( CHOICE → ( 𝑊 ∈ V → ( ran ( card ∘ 𝑅1 ) ∖ ω ) ∈ V ) )
77 6 76 mtod ⊢ ( CHOICE → ¬ 𝑊 ∈ V )