Theorem iscard5

Description: Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023)

	Ref	Expression
Assertion	iscard5	|- ( ( card ` A ) = A <-> ( A e. On /\ A. x e. A -. x ~~ A ) )

Proof

Step	Hyp	Ref	Expression
1		iscard	|- ( ( card ` A ) = A <-> ( A e. On /\ A. x e. A x ~< A ) )
2		sdomnen	|- ( x ~< A -> -. x ~~ A )
3		onelss	|- ( A e. On -> ( x e. A -> x C_ A ) )
4		ssdomg	|- ( A e. On -> ( x C_ A -> x ~<_ A ) )
5	3 4	syld	|- ( A e. On -> ( x e. A -> x ~<_ A ) )
6	5	imp	|- ( ( A e. On /\ x e. A ) -> x ~<_ A )
7		brsdom	|- ( x ~< A <-> ( x ~<_ A /\ -. x ~~ A ) )
8	7	biimpri	|- ( ( x ~<_ A /\ -. x ~~ A ) -> x ~< A )
9	8	a1i	|- ( ( A e. On /\ x e. A ) -> ( ( x ~<_ A /\ -. x ~~ A ) -> x ~< A ) )
10	6 9	mpand	|- ( ( A e. On /\ x e. A ) -> ( -. x ~~ A -> x ~< A ) )
11	2 10	impbid2	|- ( ( A e. On /\ x e. A ) -> ( x ~< A <-> -. x ~~ A ) )
12	11	ralbidva	|- ( A e. On -> ( A. x e. A x ~< A <-> A. x e. A -. x ~~ A ) )
13	12	pm5.32i	|- ( ( A e. On /\ A. x e. A x ~< A ) <-> ( A e. On /\ A. x e. A -. x ~~ A ) )
14	1 13	bitri	|- ( ( card ` A ) = A <-> ( A e. On /\ A. x e. A -. x ~~ A ) )