Theorem rankkardu

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

	Ref	Expression
Assertion	rankkardu	⊢ ( rank ‘ ( kard ‘ 𝐴 ) ) ⊆ suc ( rank ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		kardval	⊢ ( kard ‘ 𝐴 ) = Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 }
2	1	fveq2i	⊢ ( rank ‘ ( kard ‘ 𝐴 ) ) = ( rank ‘ Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } )
3		enrefg	⊢ ( 𝐴 ∈ V → 𝐴 ≈ 𝐴 )
4		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≈ 𝐴 ↔ 𝐴 ≈ 𝐴 ) )
5	4	elabg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐴 } ↔ 𝐴 ≈ 𝐴 ) )
6	3 5	mpbird	⊢ ( 𝐴 ∈ V → 𝐴 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐴 } )
7		rankscottu	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐴 } → ( rank ‘ Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } ) ⊆ suc ( rank ‘ 𝐴 ) )
8	6 7	syl	⊢ ( 𝐴 ∈ V → ( rank ‘ Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } ) ⊆ suc ( rank ‘ 𝐴 ) )
9	2 8	eqsstrid	⊢ ( 𝐴 ∈ V → ( rank ‘ ( kard ‘ 𝐴 ) ) ⊆ suc ( rank ‘ 𝐴 ) )
10		kardeq0	⊢ ( ( kard ‘ 𝐴 ) = ∅ ↔ ¬ 𝐴 ∈ V )
11		fvex	⊢ ( kard ‘ 𝐴 ) ∈ V
12	11	rankeq0	⊢ ( ( kard ‘ 𝐴 ) = ∅ ↔ ( rank ‘ ( kard ‘ 𝐴 ) ) = ∅ )
13		0ss	⊢ ∅ ⊆ suc ( rank ‘ 𝐴 )
14		sseq1	⊢ ( ( rank ‘ ( kard ‘ 𝐴 ) ) = ∅ → ( ( rank ‘ ( kard ‘ 𝐴 ) ) ⊆ suc ( rank ‘ 𝐴 ) ↔ ∅ ⊆ suc ( rank ‘ 𝐴 ) ) )
15	13 14	mpbiri	⊢ ( ( rank ‘ ( kard ‘ 𝐴 ) ) = ∅ → ( rank ‘ ( kard ‘ 𝐴 ) ) ⊆ suc ( rank ‘ 𝐴 ) )
16	12 15	sylbi	⊢ ( ( kard ‘ 𝐴 ) = ∅ → ( rank ‘ ( kard ‘ 𝐴 ) ) ⊆ suc ( rank ‘ 𝐴 ) )
17	10 16	sylbir	⊢ ( ¬ 𝐴 ∈ V → ( rank ‘ ( kard ‘ 𝐴 ) ) ⊆ suc ( rank ‘ 𝐴 ) )
18	9 17	pm2.61i	⊢ ( rank ‘ ( kard ‘ 𝐴 ) ) ⊆ suc ( rank ‘ 𝐴 )