pwfseq

Description: The powerset of a Dedekind-infinite set does not inject into the set of finite sequences. The proof is due to Halbeisen and Shelah. Proposition 1.7 of KanamoriPincus p. 418. (Contributed by Mario Carneiro, 31-May-2015)

		Ref	Expression
	Assertion	pwfseq	$⊢ ω ≼ A \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n})$

Proof

Step	Hyp	Ref	Expression
1		reldom	$⊢ Rel ≼$
2	1	brrelex2i	$⊢ ω ≼ A \to A \in V$
3		domeng	$⊢ A \in V \to (ω ≼ A \leftrightarrow \exists t (ω \approx t \land t \subseteq A))$
4		bren	$⊢ ω \approx t \leftrightarrow \exists h h : ω \underset{1-1 onto}{⟶} t$
5		harcl	$⊢ har (𝒫 A) \in On$
6		infxpenc2	$⊢ har (𝒫 A) \in On \to \exists m \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b)$
7	5 6	ax-mp	$⊢ \exists m \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b)$
8		simpr	$⊢ (((h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \land \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b)) \land g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})) \to g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
9		oveq2	$⊢ n = k \to A^{n} = A^{k}$
10	9	cbviunv	$⊢ ⋃_{n \in ω} (A^{n}) = ⋃_{k \in ω} (A^{k})$
11		f1eq3	$⊢ ⋃_{n \in ω} (A^{n}) = ⋃_{k \in ω} (A^{k}) \to (g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n}) \leftrightarrow g : 𝒫 A \underset{1-1}{⟶} ⋃_{k \in ω} (A^{k}))$
12	10 11	ax-mp	$⊢ g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n}) \leftrightarrow g : 𝒫 A \underset{1-1}{⟶} ⋃_{k \in ω} (A^{k})$
13	8 12	sylib	$⊢ (((h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \land \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b)) \land g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})) \to g : 𝒫 A \underset{1-1}{⟶} ⋃_{k \in ω} (A^{k})$
14		simpllr	$⊢ (((h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \land \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b)) \land g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})) \to t \subseteq A$
15		simplll	$⊢ (((h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \land \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b)) \land g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})) \to h : ω \underset{1-1 onto}{⟶} t$
16		biid	$⊢ ((u \subseteq A \land r \subseteq u \times u \land r We u) \land ω ≼ u) \leftrightarrow ((u \subseteq A \land r \subseteq u \times u \land r We u) \land ω ≼ u)$
17		simplr	$⊢ (((h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \land \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b)) \land g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})) \to \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b)$
18		sseq2	$⊢ b = w \to (ω \subseteq b \leftrightarrow ω \subseteq w)$
19		fveq2	$⊢ b = w \to m (b) = m (w)$
20	19	f1oeq1d	$⊢ b = w \to (m (b) : b \times b \underset{1-1 onto}{⟶} b \leftrightarrow m (w) : b \times b \underset{1-1 onto}{⟶} b)$
21		xpeq12	$⊢ (b = w \land b = w) \to b \times b = w \times w$
22	21	anidms	$⊢ b = w \to b \times b = w \times w$
23	22	f1oeq2d	$⊢ b = w \to (m (w) : b \times b \underset{1-1 onto}{⟶} b \leftrightarrow m (w) : w \times w \underset{1-1 onto}{⟶} b)$
24		f1oeq3	$⊢ b = w \to (m (w) : w \times w \underset{1-1 onto}{⟶} b \leftrightarrow m (w) : w \times w \underset{1-1 onto}{⟶} w)$
25	20 23 24	3bitrd	$⊢ b = w \to (m (b) : b \times b \underset{1-1 onto}{⟶} b \leftrightarrow m (w) : w \times w \underset{1-1 onto}{⟶} w)$
26	18 25	imbi12d	$⊢ b = w \to ((ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b) \leftrightarrow (ω \subseteq w \to m (w) : w \times w \underset{1-1 onto}{⟶} w))$
27	26	cbvralvw	$⊢ \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b) \leftrightarrow \forall w \in har (𝒫 A) (ω \subseteq w \to m (w) : w \times w \underset{1-1 onto}{⟶} w)$
28	17 27	sylib	$⊢ (((h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \land \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b)) \land g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})) \to \forall w \in har (𝒫 A) (ω \subseteq w \to m (w) : w \times w \underset{1-1 onto}{⟶} w)$
29		eqid	$⊢ OrdIso (r, u) = OrdIso (r, u)$
30		eqid	$⊢ (s \in dom OrdIso (r, u), z \in dom OrdIso (r, u) ⟼ ⟨OrdIso (r, u) (s), OrdIso (r, u) (z)⟩) = (s \in dom OrdIso (r, u), z \in dom OrdIso (r, u) ⟼ ⟨OrdIso (r, u) (s), OrdIso (r, u) (z)⟩)$
31		eqid	$⊢ (OrdIso (r, u) \circ m (dom OrdIso (r, u))) \circ {(s \in dom OrdIso (r, u), z \in dom OrdIso (r, u) ⟼ ⟨OrdIso (r, u) (s), OrdIso (r, u) (z)⟩)}^{-1} = (OrdIso (r, u) \circ m (dom OrdIso (r, u))) \circ {(s \in dom OrdIso (r, u), z \in dom OrdIso (r, u) ⟼ ⟨OrdIso (r, u) (s), OrdIso (r, u) (z)⟩)}^{-1}$
32		eqid	$⊢ {seq}_{ω} ((p \in V, f \in V ⟼ (x \in (u^{suc p}) ⟼ f ({x ↾}_{p}) ((OrdIso (r, u) \circ m (dom OrdIso (r, u))) \circ {(s \in dom OrdIso (r, u), z \in dom OrdIso (r, u) ⟼ ⟨OrdIso (r, u) (s), OrdIso (r, u) (z)⟩)}^{-1}) x (p))), \{⟨\emptyset, OrdIso (r, u) (\emptyset)⟩\}) = {seq}_{ω} ((p \in V, f \in V ⟼ (x \in (u^{suc p}) ⟼ f ({x ↾}_{p}) ((OrdIso (r, u) \circ m (dom OrdIso (r, u))) \circ {(s \in dom OrdIso (r, u), z \in dom OrdIso (r, u) ⟼ ⟨OrdIso (r, u) (s), OrdIso (r, u) (z)⟩)}^{-1}) x (p))), \{⟨\emptyset, OrdIso (r, u) (\emptyset)⟩\})$
33		oveq2	$⊢ n = k \to u^{n} = u^{k}$
34	33	cbviunv	$⊢ ⋃_{n \in ω} (u^{n}) = ⋃_{k \in ω} (u^{k})$
35	34	mpteq1i	$⊢ (y \in ⋃_{n \in ω} (u^{n}) ⟼ ⟨dom y, {seq}_{ω} ((p \in V, f \in V ⟼ (x \in (u^{suc p}) ⟼ f ({x ↾}_{p}) ((OrdIso (r, u) \circ m (dom OrdIso (r, u))) \circ {(s \in dom OrdIso (r, u), z \in dom OrdIso (r, u) ⟼ ⟨OrdIso (r, u) (s), OrdIso (r, u) (z)⟩)}^{-1}) x (p))), \{⟨\emptyset, OrdIso (r, u) (\emptyset)⟩\}) (dom y) (y)⟩) = (y \in ⋃_{k \in ω} (u^{k}) ⟼ ⟨dom y, {seq}_{ω} ((p \in V, f \in V ⟼ (x \in (u^{suc p}) ⟼ f ({x ↾}_{p}) ((OrdIso (r, u) \circ m (dom OrdIso (r, u))) \circ {(s \in dom OrdIso (r, u), z \in dom OrdIso (r, u) ⟼ ⟨OrdIso (r, u) (s), OrdIso (r, u) (z)⟩)}^{-1}) x (p))), \{⟨\emptyset, OrdIso (r, u) (\emptyset)⟩\}) (dom y) (y)⟩)$
36		eqid	$⊢ (x \in ω, y \in u ⟼ ⟨OrdIso (r, u) (x), y⟩) = (x \in ω, y \in u ⟼ ⟨OrdIso (r, u) (x), y⟩)$
37		eqid	$⊢ (((OrdIso (r, u) \circ m (dom OrdIso (r, u))) \circ {(s \in dom OrdIso (r, u), z \in dom OrdIso (r, u) ⟼ ⟨OrdIso (r, u) (s), OrdIso (r, u) (z)⟩)}^{-1}) \circ (x \in ω, y \in u ⟼ ⟨OrdIso (r, u) (x), y⟩)) \circ (y \in ⋃_{n \in ω} (u^{n}) ⟼ ⟨dom y, {seq}_{ω} ((p \in V, f \in V ⟼ (x \in (u^{suc p}) ⟼ f ({x ↾}_{p}) ((OrdIso (r, u) \circ m (dom OrdIso (r, u))) \circ {(s \in dom OrdIso (r, u), z \in dom OrdIso (r, u) ⟼ ⟨OrdIso (r, u) (s), OrdIso (r, u) (z)⟩)}^{-1}) x (p))), \{⟨\emptyset, OrdIso (r, u) (\emptyset)⟩\}) (dom y) (y)⟩) = (((OrdIso (r, u) \circ m (dom OrdIso (r, u))) \circ {(s \in dom OrdIso (r, u), z \in dom OrdIso (r, u) ⟼ ⟨OrdIso (r, u) (s), OrdIso (r, u) (z)⟩)}^{-1}) \circ (x \in ω, y \in u ⟼ ⟨OrdIso (r, u) (x), y⟩)) \circ (y \in ⋃_{n \in ω} (u^{n}) ⟼ ⟨dom y, {seq}_{ω} ((p \in V, f \in V ⟼ (x \in (u^{suc p}) ⟼ f ({x ↾}_{p}) ((OrdIso (r, u) \circ m (dom OrdIso (r, u))) \circ {(s \in dom OrdIso (r, u), z \in dom OrdIso (r, u) ⟼ ⟨OrdIso (r, u) (s), OrdIso (r, u) (z)⟩)}^{-1}) x (p))), \{⟨\emptyset, OrdIso (r, u) (\emptyset)⟩\}) (dom y) (y)⟩)$
38	13 14 15 16 28 29 30 31 32 35 36 37	pwfseqlem5	$⊢ \neg (((h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \land \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b)) \land g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n}))$
39	38	imnani	$⊢ ((h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \land \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b)) \to \neg g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
40	39	nexdv	$⊢ ((h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \land \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b)) \to \neg \exists g g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
41		brdomi	$⊢ 𝒫 A ≼ ⋃_{n \in ω} (A^{n}) \to \exists g g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
42	40 41	nsyl	$⊢ ((h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \land \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b)) \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n})$
43	42	ex	$⊢ (h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \to (\forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b) \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n}))$
44	43	exlimdv	$⊢ (h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \to (\exists m \forall b \in har (𝒫 A) (ω \subseteq b \to m (b) : b \times b \underset{1-1 onto}{⟶} b) \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n}))$
45	7 44	mpi	$⊢ (h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n})$
46	45	ex	$⊢ h : ω \underset{1-1 onto}{⟶} t \to (t \subseteq A \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n}))$
47	46	exlimiv	$⊢ \exists h h : ω \underset{1-1 onto}{⟶} t \to (t \subseteq A \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n}))$
48	4 47	sylbi	$⊢ ω \approx t \to (t \subseteq A \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n}))$
49	48	imp	$⊢ (ω \approx t \land t \subseteq A) \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n})$
50	49	exlimiv	$⊢ \exists t (ω \approx t \land t \subseteq A) \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n})$
51	3 50	syl6bi	$⊢ A \in V \to (ω ≼ A \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n}))$
52	2 51	mpcom	$⊢ ω ≼ A \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n})$

Metamath Proof Explorer

Theorem pwfseq

Proof