Metamath Proof Explorer

Theorem cardid2

Description: Any numerable set is equinumerous to its cardinal number. Proposition 10.5 of TakeutiZaring p. 85. (Contributed by Mario Carneiro, 7-Jan-2013)

		Ref	Expression
	Assertion	cardid2	$⊢ A \in dom card \to card (A) \approx A$

Proof

Step	Hyp	Ref	Expression
1		cardval3	$⊢ A \in dom card \to card (A) = ⋂ \{y \in On \| y \approx A\}$
2		ssrab2	$⊢ \{y \in On \| y \approx A\} \subseteq On$
3		fvex	$⊢ card (A) \in V$
4	1 3	eqeltrrdi	$⊢ A \in dom card \to ⋂ \{y \in On \| y \approx A\} \in V$
5		intex	$⊢ \{y \in On \| y \approx A\} \neq \emptyset \leftrightarrow ⋂ \{y \in On \| y \approx A\} \in V$
6	4 5	sylibr	$⊢ A \in dom card \to \{y \in On \| y \approx A\} \neq \emptyset$
7		onint	$⊢ (\{y \in On \| y \approx A\} \subseteq On \land \{y \in On \| y \approx A\} \neq \emptyset) \to ⋂ \{y \in On \| y \approx A\} \in \{y \in On \| y \approx A\}$
8	2 6 7	sylancr	$⊢ A \in dom card \to ⋂ \{y \in On \| y \approx A\} \in \{y \in On \| y \approx A\}$
9	1 8	eqeltrd	$⊢ A \in dom card \to card (A) \in \{y \in On \| y \approx A\}$
10		breq1	$⊢ y = card (A) \to (y \approx A \leftrightarrow card (A) \approx A)$
11	10	elrab	$⊢ card (A) \in \{y \in On \| y \approx A\} \leftrightarrow (card (A) \in On \land card (A) \approx A)$
12	11	simprbi	$⊢ card (A) \in \{y \in On \| y \approx A\} \to card (A) \approx A$
13	9 12	syl	$⊢ A \in dom card \to card (A) \approx A$