Metamath Proof Explorer

Theorem cardne

Description: No member of a cardinal number of a set is equinumerous to the set. Proposition 10.6(2) of TakeutiZaring p. 85. (Contributed by Mario Carneiro, 9-Jan-2013)

		Ref	Expression
	Assertion	cardne	$⊢ A \in card (B) \to \neg A \approx B$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$⊢ A \in card (B) \to B \in dom card$
2		cardon	$⊢ card (B) \in On$
3	2	oneli	$⊢ A \in card (B) \to A \in On$
4		breq1	$⊢ x = A \to (x \approx B \leftrightarrow A \approx B)$
5	4	onintss	$⊢ A \in On \to (A \approx B \to ⋂ \{x \in On \| x \approx B\} \subseteq A)$
6	3 5	syl	$⊢ A \in card (B) \to (A \approx B \to ⋂ \{x \in On \| x \approx B\} \subseteq A)$
7	6	adantl	$⊢ (B \in dom card \land A \in card (B)) \to (A \approx B \to ⋂ \{x \in On \| x \approx B\} \subseteq A)$
8		cardval3	$⊢ B \in dom card \to card (B) = ⋂ \{x \in On \| x \approx B\}$
9	8	sseq1d	$⊢ B \in dom card \to (card (B) \subseteq A \leftrightarrow ⋂ \{x \in On \| x \approx B\} \subseteq A)$
10	9	adantr	$⊢ (B \in dom card \land A \in card (B)) \to (card (B) \subseteq A \leftrightarrow ⋂ \{x \in On \| x \approx B\} \subseteq A)$
11	7 10	sylibrd	$⊢ (B \in dom card \land A \in card (B)) \to (A \approx B \to card (B) \subseteq A)$
12		ontri1	$⊢ (card (B) \in On \land A \in On) \to (card (B) \subseteq A \leftrightarrow \neg A \in card (B))$
13	2 3 12	sylancr	$⊢ A \in card (B) \to (card (B) \subseteq A \leftrightarrow \neg A \in card (B))$
14	13	adantl	$⊢ (B \in dom card \land A \in card (B)) \to (card (B) \subseteq A \leftrightarrow \neg A \in card (B))$
15	11 14	sylibd	$⊢ (B \in dom card \land A \in card (B)) \to (A \approx B \to \neg A \in card (B))$
16	15	con2d	$⊢ (B \in dom card \land A \in card (B)) \to (A \in card (B) \to \neg A \approx B)$
17	16	ex	$⊢ B \in dom card \to (A \in card (B) \to (A \in card (B) \to \neg A \approx B))$
18	17	pm2.43d	$⊢ B \in dom card \to (A \in card (B) \to \neg A \approx B)$
19	1 18	mpcom	$⊢ A \in card (B) \to \neg A \approx B$