# 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 ${⊢}¬{A}\prec \mathrm{cf}\left(\mathrm{rank}\left({A}\right)\right)$

### Proof

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