Metamath Proof Explorer

Theorem cardsdomel

Description: A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of TakeutiZaring p. 93. (Contributed by Mario Carneiro, 15-Jan-2013) (Revised by Mario Carneiro, 4-Jun-2015)

		Ref	Expression
	Assertion	cardsdomel	$⊢ (A \in On \land B \in dom card) \to (A ≺ B \leftrightarrow A \in card (B))$

Proof

Step	Hyp	Ref	Expression
1		cardid2	$⊢ B \in dom card \to card (B) \approx B$
2	1	ensymd	$⊢ B \in dom card \to B \approx card (B)$
3		sdomentr	$⊢ (A ≺ B \land B \approx card (B)) \to A ≺ card (B)$
4	2 3	sylan2	$⊢ (A ≺ B \land B \in dom card) \to A ≺ card (B)$
5		ssdomg	$⊢ A \in On \to (card (B) \subseteq A \to card (B) ≼ A)$
6		cardon	$⊢ card (B) \in On$
7		domtriord	$⊢ (card (B) \in On \land A \in On) \to (card (B) ≼ A \leftrightarrow \neg A ≺ card (B))$
8	6 7	mpan	$⊢ A \in On \to (card (B) ≼ A \leftrightarrow \neg A ≺ card (B))$
9	5 8	sylibd	$⊢ A \in On \to (card (B) \subseteq A \to \neg A ≺ card (B))$
10	9	con2d	$⊢ A \in On \to (A ≺ card (B) \to \neg card (B) \subseteq A)$
11		ontri1	$⊢ (card (B) \in On \land A \in On) \to (card (B) \subseteq A \leftrightarrow \neg A \in card (B))$
12	6 11	mpan	$⊢ A \in On \to (card (B) \subseteq A \leftrightarrow \neg A \in card (B))$
13	12	con2bid	$⊢ A \in On \to (A \in card (B) \leftrightarrow \neg card (B) \subseteq A)$
14	10 13	sylibrd	$⊢ A \in On \to (A ≺ card (B) \to A \in card (B))$
15	4 14	syl5	$⊢ A \in On \to ((A ≺ B \land B \in dom card) \to A \in card (B))$
16	15	expcomd	$⊢ A \in On \to (B \in dom card \to (A ≺ B \to A \in card (B)))$
17	16	imp	$⊢ (A \in On \land B \in dom card) \to (A ≺ B \to A \in card (B))$
18		cardsdomelir	$⊢ A \in card (B) \to A ≺ B$
19	17 18	impbid1	$⊢ (A \in On \land B \in dom card) \to (A ≺ B \leftrightarrow A \in card (B))$