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