canth4

Description: An "effective" form of Cantor's theorem canth . For any function F from the powerset of A to A , there are two definable sets B and C which witness non-injectivity of F . Corollary 1.3 of KanamoriPincus p. 416. (Contributed by Mario Carneiro, 18-May-2015)

	Ref	Expression
Hypotheses	canth4.1	$⊢ W = \{⟨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))\}$
	canth4.2	$⊢ B = ⋃ dom W$
	canth4.3	$⊢ C = {W (B)}^{-1} [\{F (B)\}]$
Assertion	canth4	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to (B \subseteq A \land C \subset B \land F (B) = F (C))$

Proof

Step	Hyp	Ref	Expression
1		canth4.1	$⊢ W = \{⟨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))\}$
2		canth4.2	$⊢ B = ⋃ dom W$
3		canth4.3	$⊢ C = {W (B)}^{-1} [\{F (B)\}]$
4		eqid	$⊢ B = B$
5		eqid	$⊢ W (B) = W (B)$
6	4 5	pm3.2i	$⊢ (B = B \land W (B) = W (B))$
7		simp1	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to A \in V$
8		simpl2	$⊢ ((A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \land x \in (𝒫 A \cap dom card)) \to F : D ⟶ A$
9		simp3	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to 𝒫 A \cap dom card \subseteq D$
10	9	sselda	$⊢ ((A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \land x \in (𝒫 A \cap dom card)) \to x \in D$
11	8 10	ffvelcdmd	$⊢ ((A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \land x \in (𝒫 A \cap dom card)) \to F (x) \in A$
12	1 7 11 2	fpwwe	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to ((B W W (B) \land F (B) \in B) \leftrightarrow (B = B \land W (B) = W (B)))$
13	6 12	mpbiri	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to (B W W (B) \land F (B) \in B)$
14	13	simpld	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to B W W (B)$
15	1 7	fpwwelem	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to (B W W (B) \leftrightarrow ((B \subseteq A \land W (B) \subseteq B \times B) \land (W (B) We B \land \forall y \in B F ({W (B)}^{-1} [\{y\}]) = y)))$
16	14 15	mpbid	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to ((B \subseteq A \land W (B) \subseteq B \times B) \land (W (B) We B \land \forall y \in B F ({W (B)}^{-1} [\{y\}]) = y))$
17	16	simpld	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to (B \subseteq A \land W (B) \subseteq B \times B)$
18	17	simpld	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to B \subseteq A$
19		cnvimass	$⊢ {W (B)}^{-1} [\{F (B)\}] \subseteq dom W (B)$
20	3 19	eqsstri	$⊢ C \subseteq dom W (B)$
21	17	simprd	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to W (B) \subseteq B \times B$
22		dmss	$⊢ W (B) \subseteq B \times B \to dom W (B) \subseteq dom (B \times B)$
23	21 22	syl	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to dom W (B) \subseteq dom (B \times B)$
24		dmxpid	$⊢ dom (B \times B) = B$
25	23 24	sseqtrdi	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to dom W (B) \subseteq B$
26	20 25	sstrid	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to C \subseteq B$
27	13	simprd	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to F (B) \in B$
28	16	simprd	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to (W (B) We B \land \forall y \in B F ({W (B)}^{-1} [\{y\}]) = y)$
29	28	simpld	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to W (B) We B$
30		weso	$⊢ W (B) We B \to W (B) Or B$
31	29 30	syl	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to W (B) Or B$
32		sonr	$⊢ (W (B) Or B \land F (B) \in B) \to \neg F (B) W (B) F (B)$
33	31 27 32	syl2anc	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to \neg F (B) W (B) F (B)$
34	3	eleq2i	$⊢ F (B) \in C \leftrightarrow F (B) \in {W (B)}^{-1} [\{F (B)\}]$
35		fvex	$⊢ F (B) \in V$
36	35	eliniseg	$⊢ F (B) \in V \to (F (B) \in {W (B)}^{-1} [\{F (B)\}] \leftrightarrow F (B) W (B) F (B))$
37	35 36	ax-mp	$⊢ F (B) \in {W (B)}^{-1} [\{F (B)\}] \leftrightarrow F (B) W (B) F (B)$
38	34 37	bitri	$⊢ F (B) \in C \leftrightarrow F (B) W (B) F (B)$
39	33 38	sylnibr	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to \neg F (B) \in C$
40	26 27 39	ssnelpssd	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to C \subset B$
41		sneq	$⊢ y = F (B) \to \{y\} = \{F (B)\}$
42	41	imaeq2d	$⊢ y = F (B) \to {W (B)}^{-1} [\{y\}] = {W (B)}^{-1} [\{F (B)\}]$
43	42 3	eqtr4di	$⊢ y = F (B) \to {W (B)}^{-1} [\{y\}] = C$
44	43	fveq2d	$⊢ y = F (B) \to F ({W (B)}^{-1} [\{y\}]) = F (C)$
45		id	$⊢ y = F (B) \to y = F (B)$
46	44 45	eqeq12d	$⊢ y = F (B) \to (F ({W (B)}^{-1} [\{y\}]) = y \leftrightarrow F (C) = F (B))$
47	28	simprd	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to \forall y \in B F ({W (B)}^{-1} [\{y\}]) = y$
48	46 47 27	rspcdva	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to F (C) = F (B)$
49	48	eqcomd	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to F (B) = F (C)$
50	18 40 49	3jca	$⊢ (A \in V \land F : D ⟶ A \land 𝒫 A \cap dom card \subseteq D) \to (B \subseteq A \land C \subset B \land F (B) = F (C))$

Metamath Proof Explorer

Theorem canth4

Proof