Theorem kardval2

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 kardval . (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	kardval2	Could not format assertion : No typesetting found for |- ( kard ` A ) = { x | ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) } 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		breq1	$$⊢x=y\to \left(x\approx A\leftrightarrow y\approx A\right)$$
3	2	scottab	$$⊢Scott\left\{x|x\approx A\right\}=\left\{x|\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}$$
4	1 3	eqtri	Could not format ( kard ` A ) = { x | ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) } : No typesetting found for |- ( kard ` A ) = { x | ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) } with typecode |-