Theorem kardval

Description: The value of the kard function. This theorem depends on the Axiom of Regularity and the Axiom of Infinity, but it does not depend on the Axiom of Choice. See also kardval2 . (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	kardval	⊢ ( kard ‘ 𝐴 ) = Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 ≈ 𝑦 ↔ 𝑥 ≈ 𝐴 ) )
2	1	abbidv	⊢ ( 𝑦 = 𝐴 → { 𝑥 ∣ 𝑥 ≈ 𝑦 } = { 𝑥 ∣ 𝑥 ≈ 𝐴 } )
3	2	scotteqd	⊢ ( 𝑦 = 𝐴 → Scott { 𝑥 ∣ 𝑥 ≈ 𝑦 } = Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } )
4		df-kard	⊢ kard = ( 𝑦 ∈ V ↦ Scott { 𝑥 ∣ 𝑥 ≈ 𝑦 } )
5		scottex2	⊢ Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } ∈ V
6	3 4 5	fvmpt	⊢ ( 𝐴 ∈ V → ( kard ‘ 𝐴 ) = Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } )
7		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( kard ‘ 𝐴 ) = ∅ )
8		scott0i	⊢ Scott ∅ = ∅
9	7 8	eqtr4di	⊢ ( ¬ 𝐴 ∈ V → ( kard ‘ 𝐴 ) = Scott ∅ )
10		simpr	⊢ ( ( 𝑥 ∈ V ∧ 𝐴 ∈ V ) → 𝐴 ∈ V )
11	10	con3i	⊢ ( ¬ 𝐴 ∈ V → ¬ ( 𝑥 ∈ V ∧ 𝐴 ∈ V ) )
12		encv	⊢ ( 𝑥 ≈ 𝐴 → ( 𝑥 ∈ V ∧ 𝐴 ∈ V ) )
13	11 12	nsyl	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝑥 ≈ 𝐴 )
14	13	alrimiv	⊢ ( ¬ 𝐴 ∈ V → ∀ 𝑥 ¬ 𝑥 ≈ 𝐴 )
15		ab0	⊢ ( { 𝑥 ∣ 𝑥 ≈ 𝐴 } = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ≈ 𝐴 )
16	14 15	sylibr	⊢ ( ¬ 𝐴 ∈ V → { 𝑥 ∣ 𝑥 ≈ 𝐴 } = ∅ )
17	16	scotteqd	⊢ ( ¬ 𝐴 ∈ V → Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } = Scott ∅ )
18	9 17	eqtr4d	⊢ ( ¬ 𝐴 ∈ V → ( kard ‘ 𝐴 ) = Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } )
19	6 18	pm2.61i	⊢ ( kard ‘ 𝐴 ) = Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 }