canthnum

Description: The set of well-orderable subsets of a set A strictly dominates A . A stronger form of canth2 . Corollary 1.4(a) of KanamoriPincus p. 417. (Contributed by Mario Carneiro, 19-May-2015)

		Ref	Expression
	Assertion	canthnum	$⊢ A \in V \to A ≺ (𝒫 A \cap dom card)$

Proof

Step	Hyp	Ref	Expression
1		pwexg	$⊢ A \in V \to 𝒫 A \in V$
2		inex1g	$⊢ 𝒫 A \in V \to 𝒫 A \cap Fin \in V$
3		infpwfidom	$⊢ 𝒫 A \cap Fin \in V \to A ≼ (𝒫 A \cap Fin)$
4	1 2 3	3syl	$⊢ A \in V \to A ≼ (𝒫 A \cap Fin)$
5		inex1g	$⊢ 𝒫 A \in V \to 𝒫 A \cap dom card \in V$
6	1 5	syl	$⊢ A \in V \to 𝒫 A \cap dom card \in V$
7		finnum	$⊢ x \in Fin \to x \in dom card$
8	7	ssriv	$⊢ Fin \subseteq dom card$
9		sslin	$⊢ Fin \subseteq dom card \to 𝒫 A \cap Fin \subseteq 𝒫 A \cap dom card$
10	8 9	ax-mp	$⊢ 𝒫 A \cap Fin \subseteq 𝒫 A \cap dom card$
11		ssdomg	$⊢ 𝒫 A \cap dom card \in V \to (𝒫 A \cap Fin \subseteq 𝒫 A \cap dom card \to (𝒫 A \cap Fin) ≼ (𝒫 A \cap dom card))$
12	6 10 11	mpisyl	$⊢ A \in V \to (𝒫 A \cap Fin) ≼ (𝒫 A \cap dom card)$
13		domtr	$⊢ (A ≼ (𝒫 A \cap Fin) \land (𝒫 A \cap Fin) ≼ (𝒫 A \cap dom card)) \to A ≼ (𝒫 A \cap dom card)$
14	4 12 13	syl2anc	$⊢ A \in V \to A ≼ (𝒫 A \cap dom card)$
15		eqid	$⊢ \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x f (r^{-1} [\{y\}]) = y))\} = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x f (r^{-1} [\{y\}]) = y))\}$
16	15	fpwwecbv	$⊢ \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x f (r^{-1} [\{y\}]) = y))\} = \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a f (s^{-1} [\{z\}]) = z))\}$
17		eqid	$⊢ ⋃ dom \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x f (r^{-1} [\{y\}]) = y))\} = ⋃ dom \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x f (r^{-1} [\{y\}]) = y))\}$
18		eqid	$⊢ {\{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x f (r^{-1} [\{y\}]) = y))\} (⋃ dom \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x f (r^{-1} [\{y\}]) = y))\})}^{-1} [\{f (⋃ dom \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x f (r^{-1} [\{y\}]) = y))\})\}] = {\{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x f (r^{-1} [\{y\}]) = y))\} (⋃ dom \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x f (r^{-1} [\{y\}]) = y))\})}^{-1} [\{f (⋃ dom \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x f (r^{-1} [\{y\}]) = y))\})\}]$
19	16 17 18	canthnumlem	$⊢ A \in V \to \neg f : 𝒫 A \cap dom card \underset{1-1}{⟶} A$
20		f1of1	$⊢ f : 𝒫 A \cap dom card \underset{1-1 onto}{⟶} A \to f : 𝒫 A \cap dom card \underset{1-1}{⟶} A$
21	19 20	nsyl	$⊢ A \in V \to \neg f : 𝒫 A \cap dom card \underset{1-1 onto}{⟶} A$
22	21	nexdv	$⊢ A \in V \to \neg \exists f f : 𝒫 A \cap dom card \underset{1-1 onto}{⟶} A$
23		ensym	$⊢ A \approx (𝒫 A \cap dom card) \to (𝒫 A \cap dom card) \approx A$
24		bren	$⊢ (𝒫 A \cap dom card) \approx A \leftrightarrow \exists f f : 𝒫 A \cap dom card \underset{1-1 onto}{⟶} A$
25	23 24	sylib	$⊢ A \approx (𝒫 A \cap dom card) \to \exists f f : 𝒫 A \cap dom card \underset{1-1 onto}{⟶} A$
26	22 25	nsyl	$⊢ A \in V \to \neg A \approx (𝒫 A \cap dom card)$
27		brsdom	$⊢ A ≺ (𝒫 A \cap dom card) \leftrightarrow (A ≼ (𝒫 A \cap dom card) \land \neg A \approx (𝒫 A \cap dom card))$
28	14 26 27	sylanbrc	$⊢ A \in V \to A ≺ (𝒫 A \cap dom card)$

Metamath Proof Explorer

Theorem canthnum

Proof