Metamath Proof Explorer

Theorem rankcf

Description: Any set must be at least as large as the cofinality of its rank, because the ranks of the elements of A form a cofinal map into ( rankA ) . (Contributed by Mario Carneiro, 27-May-2013)

Ref Expression
Assertion rankcf ¬ 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 rankon ⊢ ( rank ‘ 𝐴 ) ∈ On
2 onzsl ⊢ ( ( rank ‘ 𝐴 ) ∈ On ↔ ( ( rank ‘ 𝐴 ) = ∅ ∨ ∃ 𝑥 ∈ On ( rank ‘ 𝐴 ) = suc 𝑥 ∨ ( ( rank ‘ 𝐴 ) ∈ V ∧ Lim ( rank ‘ 𝐴 ) ) ) )
3 1 2 mpbi ⊢ ( ( rank ‘ 𝐴 ) = ∅ ∨ ∃ 𝑥 ∈ On ( rank ‘ 𝐴 ) = suc 𝑥 ∨ ( ( rank ‘ 𝐴 ) ∈ V ∧ Lim ( rank ‘ 𝐴 ) ) )
4 sdom0 ⊢ ¬ 𝐴 ≺ ∅
5 fveq2 ⊢ ( ( rank ‘ 𝐴 ) = ∅ → ( cf ‘ ( rank ‘ 𝐴 ) ) = ( cf ‘ ∅ ) )
6 cf0 ⊢ ( cf ‘ ∅ ) = ∅
7 5 6 syl6eq ⊢ ( ( rank ‘ 𝐴 ) = ∅ → ( cf ‘ ( rank ‘ 𝐴 ) ) = ∅ )
8 7 breq2d ⊢ ( ( rank ‘ 𝐴 ) = ∅ → ( 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) ↔ 𝐴 ≺ ∅ ) )
9 4 8 mtbiri ⊢ ( ( rank ‘ 𝐴 ) = ∅ → ¬ 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) )
10 fveq2 ⊢ ( ( rank ‘ 𝐴 ) = suc 𝑥 → ( cf ‘ ( rank ‘ 𝐴 ) ) = ( cf ‘ suc 𝑥 ) )
11 cfsuc ⊢ ( 𝑥 ∈ On → ( cf ‘ suc 𝑥 ) = 1o )
12 10 11 sylan9eqr ⊢ ( ( 𝑥 ∈ On ∧ ( rank ‘ 𝐴 ) = suc 𝑥 ) → ( cf ‘ ( rank ‘ 𝐴 ) ) = 1o )
13 nsuceq0 ⊢ suc 𝑥 ≠ ∅
14 neeq1 ⊢ ( ( rank ‘ 𝐴 ) = suc 𝑥 → ( ( rank ‘ 𝐴 ) ≠ ∅ ↔ suc 𝑥 ≠ ∅ ) )
15 13 14 mpbiri ⊢ ( ( rank ‘ 𝐴 ) = suc 𝑥 → ( rank ‘ 𝐴 ) ≠ ∅ )
16 fveq2 ⊢ ( 𝐴 = ∅ → ( rank ‘ 𝐴 ) = ( rank ‘ ∅ ) )
17 0elon ⊢ ∅ ∈ On
18 r1fnon ⊢ 𝑅1 Fn On
19 fndm ⊢ ( 𝑅1 Fn On → dom 𝑅1 = On )
20 18 19 ax-mp ⊢ dom 𝑅1 = On
21 17 20 eleqtrri ⊢ ∅ ∈ dom 𝑅1
22 rankonid ⊢ ( ∅ ∈ dom 𝑅1 ↔ ( rank ‘ ∅ ) = ∅ )
23 21 22 mpbi ⊢ ( rank ‘ ∅ ) = ∅
24 16 23 syl6eq ⊢ ( 𝐴 = ∅ → ( rank ‘ 𝐴 ) = ∅ )
25 24 necon3i ⊢ ( ( rank ‘ 𝐴 ) ≠ ∅ → 𝐴 ≠ ∅ )
26 rankvaln ⊢ ( ¬ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∅ )
27 26 necon1ai ⊢ ( ( rank ‘ 𝐴 ) ≠ ∅ → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
28 breq2 ⊢ ( 𝑦 = 𝐴 → ( 1o ≼ 𝑦 ↔ 1o ≼ 𝐴 ) )
29 neeq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ≠ ∅ ↔ 𝐴 ≠ ∅ ) )
30 0sdom1dom ⊢ ( ∅ ≺ 𝑦 ↔ 1o ≼ 𝑦 )
31 vex ⊢ 𝑦 ∈ V
32 31 0sdom ⊢ ( ∅ ≺ 𝑦 ↔ 𝑦 ≠ ∅ )
33 30 32 bitr3i ⊢ ( 1o ≼ 𝑦 ↔ 𝑦 ≠ ∅ )
34 28 29 33 vtoclbg ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 1o ≼ 𝐴 ↔ 𝐴 ≠ ∅ ) )
35 27 34 syl ⊢ ( ( rank ‘ 𝐴 ) ≠ ∅ → ( 1o ≼ 𝐴 ↔ 𝐴 ≠ ∅ ) )
36 25 35 mpbird ⊢ ( ( rank ‘ 𝐴 ) ≠ ∅ → 1o ≼ 𝐴 )
37 15 36 syl ⊢ ( ( rank ‘ 𝐴 ) = suc 𝑥 → 1o ≼ 𝐴 )
38 37 adantl ⊢ ( ( 𝑥 ∈ On ∧ ( rank ‘ 𝐴 ) = suc 𝑥 ) → 1o ≼ 𝐴 )
39 12 38 eqbrtrd ⊢ ( ( 𝑥 ∈ On ∧ ( rank ‘ 𝐴 ) = suc 𝑥 ) → ( cf ‘ ( rank ‘ 𝐴 ) ) ≼ 𝐴 )
40 39 rexlimiva ⊢ ( ∃ 𝑥 ∈ On ( rank ‘ 𝐴 ) = suc 𝑥 → ( cf ‘ ( rank ‘ 𝐴 ) ) ≼ 𝐴 )
41 domnsym ⊢ ( ( cf ‘ ( rank ‘ 𝐴 ) ) ≼ 𝐴 → ¬ 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) )
42 40 41 syl ⊢ ( ∃ 𝑥 ∈ On ( rank ‘ 𝐴 ) = suc 𝑥 → ¬ 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) )
43 nlim0 ⊢ ¬ Lim ∅
44 limeq ⊢ ( ( rank ‘ 𝐴 ) = ∅ → ( Lim ( rank ‘ 𝐴 ) ↔ Lim ∅ ) )
45 43 44 mtbiri ⊢ ( ( rank ‘ 𝐴 ) = ∅ → ¬ Lim ( rank ‘ 𝐴 ) )
46 26 45 syl ⊢ ( ¬ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ¬ Lim ( rank ‘ 𝐴 ) )
47 46 con4i ⊢ ( Lim ( rank ‘ 𝐴 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
48 r1elssi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
49 47 48 syl ⊢ ( Lim ( rank ‘ 𝐴 ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
50 49 sselda ⊢ ( ( Lim ( rank ‘ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
51 ranksnb ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝑥 } ) = suc ( rank ‘ 𝑥 ) )
52 50 51 syl ⊢ ( ( Lim ( rank ‘ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( rank ‘ { 𝑥 } ) = suc ( rank ‘ 𝑥 ) )
53 rankelb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ) )
54 47 53 syl ⊢ ( Lim ( rank ‘ 𝐴 ) → ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ) )
55 limsuc ⊢ ( Lim ( rank ‘ 𝐴 ) → ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ↔ suc ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ) )
56 54 55 sylibd ⊢ ( Lim ( rank ‘ 𝐴 ) → ( 𝑥 ∈ 𝐴 → suc ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ) )
57 56 imp ⊢ ( ( Lim ( rank ‘ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → suc ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) )
58 52 57 eqeltrd ⊢ ( ( Lim ( rank ‘ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( rank ‘ { 𝑥 } ) ∈ ( rank ‘ 𝐴 ) )
59 eleq1a ⊢ ( ( rank ‘ { 𝑥 } ) ∈ ( rank ‘ 𝐴 ) → ( 𝑤 = ( rank ‘ { 𝑥 } ) → 𝑤 ∈ ( rank ‘ 𝐴 ) ) )
60 58 59 syl ⊢ ( ( Lim ( rank ‘ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑤 = ( rank ‘ { 𝑥 } ) → 𝑤 ∈ ( rank ‘ 𝐴 ) ) )
61 60 rexlimdva ⊢ ( Lim ( rank ‘ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) → 𝑤 ∈ ( rank ‘ 𝐴 ) ) )
62 61 abssdv ⊢ ( Lim ( rank ‘ 𝐴 ) → { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } ⊆ ( rank ‘ 𝐴 ) )
63 snex ⊢ { 𝑥 } ∈ V
64 63 dfiun2 ⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } }
65 iunid ⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴
66 64 65 eqtr3i ⊢ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } = 𝐴
67 66 fveq2i ⊢ ( rank ‘ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ) = ( rank ‘ 𝐴 )
68 48 sselda ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
69 snwf ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → { 𝑥 } ∈ ∪ ( 𝑅1 “ On ) )
70 eleq1a ⊢ ( { 𝑥 } ∈ ∪ ( 𝑅1 “ On ) → ( 𝑦 = { 𝑥 } → 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) )
71 68 69 70 3syl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = { 𝑥 } → 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) )
72 71 rexlimdva ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } → 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) )
73 72 abssdv ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ⊆ ∪ ( 𝑅1 “ On ) )
74 abrexexg ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ∈ V )
75 eleq1 ⊢ ( 𝑧 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } → ( 𝑧 ∈ ∪ ( 𝑅1 “ On ) ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ∈ ∪ ( 𝑅1 “ On ) ) )
76 sseq1 ⊢ ( 𝑧 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } → ( 𝑧 ⊆ ∪ ( 𝑅1 “ On ) ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ⊆ ∪ ( 𝑅1 “ On ) ) )
77 vex ⊢ 𝑧 ∈ V
78 77 r1elss ⊢ ( 𝑧 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝑧 ⊆ ∪ ( 𝑅1 “ On ) )
79 75 76 78 vtoclbg ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ∈ V → ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ∈ ∪ ( 𝑅1 “ On ) ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ⊆ ∪ ( 𝑅1 “ On ) ) )
80 74 79 syl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ∈ ∪ ( 𝑅1 “ On ) ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ⊆ ∪ ( 𝑅1 “ On ) ) )
81 73 80 mpbird ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ∈ ∪ ( 𝑅1 “ On ) )
82 rankuni2b ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ) = ∪ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ( rank ‘ 𝑧 ) )
83 81 82 syl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ) = ∪ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ( rank ‘ 𝑧 ) )
84 67 83 syl5eqr ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∪ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ( rank ‘ 𝑧 ) )
85 fvex ⊢ ( rank ‘ 𝑧 ) ∈ V
86 85 dfiun2 ⊢ ∪ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ( rank ‘ 𝑧 ) = ∪ { 𝑤 ∣ ∃ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } 𝑤 = ( rank ‘ 𝑧 ) }
87 fveq2 ⊢ ( 𝑧 = { 𝑥 } → ( rank ‘ 𝑧 ) = ( rank ‘ { 𝑥 } ) )
88 63 87 abrexco ⊢ { 𝑤 ∣ ∃ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } 𝑤 = ( rank ‘ 𝑧 ) } = { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) }
89 88 unieqi ⊢ ∪ { 𝑤 ∣ ∃ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } 𝑤 = ( rank ‘ 𝑧 ) } = ∪ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) }
90 86 89 eqtri ⊢ ∪ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = { 𝑥 } } ( rank ‘ 𝑧 ) = ∪ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) }
91 84 90 syl6req ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } = ( rank ‘ 𝐴 ) )
92 47 91 syl ⊢ ( Lim ( rank ‘ 𝐴 ) → ∪ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } = ( rank ‘ 𝐴 ) )
93 fvex ⊢ ( rank ‘ 𝐴 ) ∈ V
94 93 cfslb ⊢ ( ( Lim ( rank ‘ 𝐴 ) ∧ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } ⊆ ( rank ‘ 𝐴 ) ∧ ∪ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } = ( rank ‘ 𝐴 ) ) → ( cf ‘ ( rank ‘ 𝐴 ) ) ≼ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } )
95 62 92 94 mpd3an23 ⊢ ( Lim ( rank ‘ 𝐴 ) → ( cf ‘ ( rank ‘ 𝐴 ) ) ≼ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } )
96 2fveq3 ⊢ ( 𝑦 = 𝐴 → ( cf ‘ ( rank ‘ 𝑦 ) ) = ( cf ‘ ( rank ‘ 𝐴 ) ) )
97 breq12 ⊢ ( ( 𝑦 = 𝐴 ∧ ( cf ‘ ( rank ‘ 𝑦 ) ) = ( cf ‘ ( rank ‘ 𝐴 ) ) ) → ( 𝑦 ≺ ( cf ‘ ( rank ‘ 𝑦 ) ) ↔ 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) ) )
98 96 97 mpdan ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ≺ ( cf ‘ ( rank ‘ 𝑦 ) ) ↔ 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) ) )
99 rexeq ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ 𝑦 𝑤 = ( rank ‘ { 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) ) )
100 99 abbidv ⊢ ( 𝑦 = 𝐴 → { 𝑤 ∣ ∃ 𝑥 ∈ 𝑦 𝑤 = ( rank ‘ { 𝑥 } ) } = { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } )
101 breq12 ⊢ ( ( { 𝑤 ∣ ∃ 𝑥 ∈ 𝑦 𝑤 = ( rank ‘ { 𝑥 } ) } = { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } ∧ 𝑦 = 𝐴 ) → ( { 𝑤 ∣ ∃ 𝑥 ∈ 𝑦 𝑤 = ( rank ‘ { 𝑥 } ) } ≼ 𝑦 ↔ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } ≼ 𝐴 ) )
102 100 101 mpancom ⊢ ( 𝑦 = 𝐴 → ( { 𝑤 ∣ ∃ 𝑥 ∈ 𝑦 𝑤 = ( rank ‘ { 𝑥 } ) } ≼ 𝑦 ↔ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } ≼ 𝐴 ) )
103 98 102 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ≺ ( cf ‘ ( rank ‘ 𝑦 ) ) → { 𝑤 ∣ ∃ 𝑥 ∈ 𝑦 𝑤 = ( rank ‘ { 𝑥 } ) } ≼ 𝑦 ) ↔ ( 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) → { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } ≼ 𝐴 ) ) )
104 eqid ⊢ ( 𝑥 ∈ 𝑦 ↦ ( rank ‘ { 𝑥 } ) ) = ( 𝑥 ∈ 𝑦 ↦ ( rank ‘ { 𝑥 } ) )
105 104 rnmpt ⊢ ran ( 𝑥 ∈ 𝑦 ↦ ( rank ‘ { 𝑥 } ) ) = { 𝑤 ∣ ∃ 𝑥 ∈ 𝑦 𝑤 = ( rank ‘ { 𝑥 } ) }
106 cfon ⊢ ( cf ‘ ( rank ‘ 𝑦 ) ) ∈ On
107 sdomdom ⊢ ( 𝑦 ≺ ( cf ‘ ( rank ‘ 𝑦 ) ) → 𝑦 ≼ ( cf ‘ ( rank ‘ 𝑦 ) ) )
108 ondomen ⊢ ( ( ( cf ‘ ( rank ‘ 𝑦 ) ) ∈ On ∧ 𝑦 ≼ ( cf ‘ ( rank ‘ 𝑦 ) ) ) → 𝑦 ∈ dom card )
109 106 107 108 sylancr ⊢ ( 𝑦 ≺ ( cf ‘ ( rank ‘ 𝑦 ) ) → 𝑦 ∈ dom card )
110 fvex ⊢ ( rank ‘ { 𝑥 } ) ∈ V
111 110 104 fnmpti ⊢ ( 𝑥 ∈ 𝑦 ↦ ( rank ‘ { 𝑥 } ) ) Fn 𝑦
112 dffn4 ⊢ ( ( 𝑥 ∈ 𝑦 ↦ ( rank ‘ { 𝑥 } ) ) Fn 𝑦 ↔ ( 𝑥 ∈ 𝑦 ↦ ( rank ‘ { 𝑥 } ) ) : 𝑦 –onto→ ran ( 𝑥 ∈ 𝑦 ↦ ( rank ‘ { 𝑥 } ) ) )
113 111 112 mpbi ⊢ ( 𝑥 ∈ 𝑦 ↦ ( rank ‘ { 𝑥 } ) ) : 𝑦 –onto→ ran ( 𝑥 ∈ 𝑦 ↦ ( rank ‘ { 𝑥 } ) )
114 fodomnum ⊢ ( 𝑦 ∈ dom card → ( ( 𝑥 ∈ 𝑦 ↦ ( rank ‘ { 𝑥 } ) ) : 𝑦 –onto→ ran ( 𝑥 ∈ 𝑦 ↦ ( rank ‘ { 𝑥 } ) ) → ran ( 𝑥 ∈ 𝑦 ↦ ( rank ‘ { 𝑥 } ) ) ≼ 𝑦 ) )
115 109 113 114 mpisyl ⊢ ( 𝑦 ≺ ( cf ‘ ( rank ‘ 𝑦 ) ) → ran ( 𝑥 ∈ 𝑦 ↦ ( rank ‘ { 𝑥 } ) ) ≼ 𝑦 )
116 105 115 eqbrtrrid ⊢ ( 𝑦 ≺ ( cf ‘ ( rank ‘ 𝑦 ) ) → { 𝑤 ∣ ∃ 𝑥 ∈ 𝑦 𝑤 = ( rank ‘ { 𝑥 } ) } ≼ 𝑦 )
117 103 116 vtoclg ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) → { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } ≼ 𝐴 ) )
118 47 117 syl ⊢ ( Lim ( rank ‘ 𝐴 ) → ( 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) → { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } ≼ 𝐴 ) )
119 domtr ⊢ ( ( ( cf ‘ ( rank ‘ 𝐴 ) ) ≼ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } ∧ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } ≼ 𝐴 ) → ( cf ‘ ( rank ‘ 𝐴 ) ) ≼ 𝐴 )
120 119 41 syl ⊢ ( ( ( cf ‘ ( rank ‘ 𝐴 ) ) ≼ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } ∧ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 = ( rank ‘ { 𝑥 } ) } ≼ 𝐴 ) → ¬ 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) )
121 95 118 120 syl6an ⊢ ( Lim ( rank ‘ 𝐴 ) → ( 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) → ¬ 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) ) )
122 121 pm2.01d ⊢ ( Lim ( rank ‘ 𝐴 ) → ¬ 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) )
123 122 adantl ⊢ ( ( ( rank ‘ 𝐴 ) ∈ V ∧ Lim ( rank ‘ 𝐴 ) ) → ¬ 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) )
124 9 42 123 3jaoi ⊢ ( ( ( rank ‘ 𝐴 ) = ∅ ∨ ∃ 𝑥 ∈ On ( rank ‘ 𝐴 ) = suc 𝑥 ∨ ( ( rank ‘ 𝐴 ) ∈ V ∧ Lim ( rank ‘ 𝐴 ) ) ) → ¬ 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) ) )
125 3 124 ax-mp ⊢ ¬ 𝐴 ≺ ( cf ‘ ( rank ‘ 𝐴 ) )