Theorem rankkardu

Description: An upper bound on the rank of a kard cardinal. (Contributed by BTernaryTau, 4-Jul-2026)

	Ref	Expression
Assertion	rankkardu	Could not format assertion : No typesetting found for |- ( rank ` ( kard ` A ) ) C_ suc ( rank ` A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		kardval	Could not format ( kard ` A ) = Scott { x | x ~~ A } : No typesetting found for |- ( kard ` A ) = Scott { x | x ~~ A } with typecode |-
2	1	fveq2i	Could not format ( rank ` ( kard ` A ) ) = ( rank ` Scott { x | x ~~ A } ) : No typesetting found for |- ( rank ` ( kard ` A ) ) = ( rank ` Scott { x | x ~~ A } ) with typecode |-
3		enrefg	$$⊢A\in \mathrm{V}\to A\approx A$$
4		breq1	$$⊢x=A\to \left(x\approx A\leftrightarrow A\approx A\right)$$
5	4	elabg	$$⊢A\in \mathrm{V}\to \left(A\in \left\{x|x\approx A\right\}\leftrightarrow A\approx A\right)$$
6	3 5	mpbird	$$⊢A\in \mathrm{V}\to A\in \left\{x|x\approx A\right\}$$
7		rankscottu	$$⊢A\in \left\{x|x\approx A\right\}\to \mathrm{rank}\left(Scott\left\{x|x\approx A\right\}\right)\subseteq \mathrm{suc}\mathrm{rank}\left(A\right)$$
8	6 7	syl	$$⊢A\in \mathrm{V}\to \mathrm{rank}\left(Scott\left\{x|x\approx A\right\}\right)\subseteq \mathrm{suc}\mathrm{rank}\left(A\right)$$
9	2 8	eqsstrid	Could not format ( A e. _V -> ( rank ` ( kard ` A ) ) C_ suc ( rank ` A ) ) : No typesetting found for |- ( A e. _V -> ( rank ` ( kard ` A ) ) C_ suc ( rank ` A ) ) with typecode |-
10		kardeq0	Could not format ( ( kard ` A ) = (/) <-> -. A e. _V ) : No typesetting found for |- ( ( kard ` A ) = (/) <-> -. A e. _V ) with typecode |-
11		fvex	Could not format ( kard ` A ) e. _V : No typesetting found for |- ( kard ` A ) e. _V with typecode |-
12	11	rankeq0	Could not format ( ( kard ` A ) = (/) <-> ( rank ` ( kard ` A ) ) = (/) ) : No typesetting found for |- ( ( kard ` A ) = (/) <-> ( rank ` ( kard ` A ) ) = (/) ) with typecode |-
13		0ss	$$⊢\varnothing \subseteq \mathrm{suc}\mathrm{rank}\left(A\right)$$
14		sseq1	Could not format ( ( rank ` ( kard ` A ) ) = (/) -> ( ( rank ` ( kard ` A ) ) C_ suc ( rank ` A ) <-> (/) C_ suc ( rank ` A ) ) ) : No typesetting found for |- ( ( rank ` ( kard ` A ) ) = (/) -> ( ( rank ` ( kard ` A ) ) C_ suc ( rank ` A ) <-> (/) C_ suc ( rank ` A ) ) ) with typecode |-
15	13 14	mpbiri	Could not format ( ( rank ` ( kard ` A ) ) = (/) -> ( rank ` ( kard ` A ) ) C_ suc ( rank ` A ) ) : No typesetting found for |- ( ( rank ` ( kard ` A ) ) = (/) -> ( rank ` ( kard ` A ) ) C_ suc ( rank ` A ) ) with typecode |-
16	12 15	sylbi	Could not format ( ( kard ` A ) = (/) -> ( rank ` ( kard ` A ) ) C_ suc ( rank ` A ) ) : No typesetting found for |- ( ( kard ` A ) = (/) -> ( rank ` ( kard ` A ) ) C_ suc ( rank ` A ) ) with typecode |-
17	10 16	sylbir	Could not format ( -. A e. _V -> ( rank ` ( kard ` A ) ) C_ suc ( rank ` A ) ) : No typesetting found for |- ( -. A e. _V -> ( rank ` ( kard ` A ) ) C_ suc ( rank ` A ) ) with typecode |-
18	9 17	pm2.61i	Could not format ( rank ` ( kard ` A ) ) C_ suc ( rank ` A ) : No typesetting found for |- ( rank ` ( kard ` A ) ) C_ suc ( rank ` A ) with typecode |-