canthp1

Description: A slightly stronger form of Cantor's theorem: For 1 < n , n + 1 < 2 ^ n . Corollary 1.6 of KanamoriPincus p. 417. (Contributed by Mario Carneiro, 18-May-2015)

		Ref	Expression
	Assertion	canthp1	$⊢ 1_{𝑜} ≺ A \to (A ⊔︀ 1_{𝑜}) ≺ 𝒫 A$

Proof

Step	Hyp	Ref	Expression
1		1sdom2	$⊢ 1_{𝑜} ≺ 2_{𝑜}$
2		sdomdom	$⊢ 1_{𝑜} ≺ 2_{𝑜} \to 1_{𝑜} ≼ 2_{𝑜}$
3	1 2	ax-mp	$⊢ 1_{𝑜} ≼ 2_{𝑜}$
4		relsdom	$⊢ Rel ≺$
5	4	brrelex2i	$⊢ 1_{𝑜} ≺ A \to A \in V$
6		djudom2	$⊢ (1_{𝑜} ≼ 2_{𝑜} \land A \in V) \to (A ⊔︀ 1_{𝑜}) ≼ (A ⊔︀ 2_{𝑜})$
7	3 5 6	sylancr	$⊢ 1_{𝑜} ≺ A \to (A ⊔︀ 1_{𝑜}) ≼ (A ⊔︀ 2_{𝑜})$
8		canthp1lem1	$⊢ 1_{𝑜} ≺ A \to (A ⊔︀ 2_{𝑜}) ≼ 𝒫 A$
9		domtr	$⊢ ((A ⊔︀ 1_{𝑜}) ≼ (A ⊔︀ 2_{𝑜}) \land (A ⊔︀ 2_{𝑜}) ≼ 𝒫 A) \to (A ⊔︀ 1_{𝑜}) ≼ 𝒫 A$
10	7 8 9	syl2anc	$⊢ 1_{𝑜} ≺ A \to (A ⊔︀ 1_{𝑜}) ≼ 𝒫 A$
11		fal	$⊢ \neg ⊥$
12		ensym	$⊢ (A ⊔︀ 1_{𝑜}) \approx 𝒫 A \to 𝒫 A \approx (A ⊔︀ 1_{𝑜})$
13		bren	$⊢ 𝒫 A \approx (A ⊔︀ 1_{𝑜}) \leftrightarrow \exists f f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})$
14	12 13	sylib	$⊢ (A ⊔︀ 1_{𝑜}) \approx 𝒫 A \to \exists f f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})$
15		f1of	$⊢ f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜}) \to f : 𝒫 A ⟶ (A ⊔︀ 1_{𝑜})$
16		pwidg	$⊢ A \in V \to A \in 𝒫 A$
17	5 16	syl	$⊢ 1_{𝑜} ≺ A \to A \in 𝒫 A$
18		ffvelrn	$⊢ (f : 𝒫 A ⟶ (A ⊔︀ 1_{𝑜}) \land A \in 𝒫 A) \to f (A) \in (A ⊔︀ 1_{𝑜})$
19	15 17 18	syl2anr	$⊢ (1_{𝑜} ≺ A \land f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})) \to f (A) \in (A ⊔︀ 1_{𝑜})$
20		dju1dif	$⊢ (A \in V \land f (A) \in (A ⊔︀ 1_{𝑜})) \to ((A ⊔︀ 1_{𝑜}) ∖ \{f (A)\}) \approx A$
21	5 19 20	syl2an2r	$⊢ (1_{𝑜} ≺ A \land f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})) \to ((A ⊔︀ 1_{𝑜}) ∖ \{f (A)\}) \approx A$
22		bren	$⊢ ((A ⊔︀ 1_{𝑜}) ∖ \{f (A)\}) \approx A \leftrightarrow \exists g g : (A ⊔︀ 1_{𝑜}) ∖ \{f (A)\} \underset{1-1 onto}{⟶} A$
23	21 22	sylib	$⊢ (1_{𝑜} ≺ A \land f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})) \to \exists g g : (A ⊔︀ 1_{𝑜}) ∖ \{f (A)\} \underset{1-1 onto}{⟶} A$
24		simpll	$⊢ ((1_{𝑜} ≺ A \land f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})) \land g : (A ⊔︀ 1_{𝑜}) ∖ \{f (A)\} \underset{1-1 onto}{⟶} A) \to 1_{𝑜} ≺ A$
25		simplr	$⊢ ((1_{𝑜} ≺ A \land f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})) \land g : (A ⊔︀ 1_{𝑜}) ∖ \{f (A)\} \underset{1-1 onto}{⟶} A) \to f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})$
26		simpr	$⊢ ((1_{𝑜} ≺ A \land f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})) \land g : (A ⊔︀ 1_{𝑜}) ∖ \{f (A)\} \underset{1-1 onto}{⟶} A) \to g : (A ⊔︀ 1_{𝑜}) ∖ \{f (A)\} \underset{1-1 onto}{⟶} A$
27		eqeq1	$⊢ w = x \to (w = A \leftrightarrow x = A)$
28		id	$⊢ w = x \to w = x$
29	27 28	ifbieq2d	$⊢ w = x \to if (w = A, \emptyset, w) = if (x = A, \emptyset, x)$
30	29	cbvmptv	$⊢ (w \in 𝒫 A ⟼ if (w = A, \emptyset, w)) = (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))$
31	30	coeq2i	$⊢ (g \circ f) \circ (w \in 𝒫 A ⟼ if (w = A, \emptyset, w)) = (g \circ f) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))$
32		eqid	$⊢ \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a ((g \circ f) \circ (w \in 𝒫 A ⟼ if (w = A, \emptyset, w))) (s^{-1} [\{z\}]) = z))\} = \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a ((g \circ f) \circ (w \in 𝒫 A ⟼ if (w = A, \emptyset, w))) (s^{-1} [\{z\}]) = z))\}$
33	32	fpwwecbv	$⊢ \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a ((g \circ f) \circ (w \in 𝒫 A ⟼ if (w = A, \emptyset, w))) (s^{-1} [\{z\}]) = z))\} = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x ((g \circ f) \circ (w \in 𝒫 A ⟼ if (w = A, \emptyset, w))) (r^{-1} [\{y\}]) = y))\}$
34		eqid	$⊢ ⋃ dom \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a ((g \circ f) \circ (w \in 𝒫 A ⟼ if (w = A, \emptyset, w))) (s^{-1} [\{z\}]) = z))\} = ⋃ dom \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a ((g \circ f) \circ (w \in 𝒫 A ⟼ if (w = A, \emptyset, w))) (s^{-1} [\{z\}]) = z))\}$
35	24 25 26 31 33 34	canthp1lem2	$⊢ \neg ((1_{𝑜} ≺ A \land f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})) \land g : (A ⊔︀ 1_{𝑜}) ∖ \{f (A)\} \underset{1-1 onto}{⟶} A)$
36	35	pm2.21i	$⊢ ((1_{𝑜} ≺ A \land f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})) \land g : (A ⊔︀ 1_{𝑜}) ∖ \{f (A)\} \underset{1-1 onto}{⟶} A) \to ⊥$
37	23 36	exlimddv	$⊢ (1_{𝑜} ≺ A \land f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})) \to ⊥$
38	37	ex	$⊢ 1_{𝑜} ≺ A \to (f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜}) \to ⊥)$
39	38	exlimdv	$⊢ 1_{𝑜} ≺ A \to (\exists f f : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜}) \to ⊥)$
40	14 39	syl5	$⊢ 1_{𝑜} ≺ A \to ((A ⊔︀ 1_{𝑜}) \approx 𝒫 A \to ⊥)$
41	11 40	mtoi	$⊢ 1_{𝑜} ≺ A \to \neg (A ⊔︀ 1_{𝑜}) \approx 𝒫 A$
42		brsdom	$⊢ (A ⊔︀ 1_{𝑜}) ≺ 𝒫 A \leftrightarrow ((A ⊔︀ 1_{𝑜}) ≼ 𝒫 A \land \neg (A ⊔︀ 1_{𝑜}) \approx 𝒫 A)$
43	10 41 42	sylanbrc	$⊢ 1_{𝑜} ≺ A \to (A ⊔︀ 1_{𝑜}) ≺ 𝒫 A$

Metamath Proof Explorer

Theorem canthp1

Proof