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		oveq2	$⊢ n = k \to A^{n} = A^{k}$
9	8	cbviunv	$⊢ ⋃_{n \in ω} (A^{n}) = ⋃_{k \in ω} (A^{k})$
10		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}))$
11	9 10	ax-mp	$⊢ g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n}) \leftrightarrow g : 𝒫 A \underset{1-1}{⟶} ⋃_{k \in ω} (A^{k})$
12	11	bilani	$⊢ (((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})$
13		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$
14		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$
15		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)$
16		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)$
17		sseq2	$⊢ b = w \to (ω \subseteq b \leftrightarrow ω \subseteq w)$
18		fveq2	$⊢ b = w \to m (b) = m (w)$
19	18	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)$
20		xpeq12	$⊢ (b = w \land b = w) \to b \times b = w \times w$
21	20	anidms	$⊢ b = w \to b \times b = w \times w$
22	21	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)$
23		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)$
24	19 22 23	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)$
25	17 24	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))$
26	25	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)$
27	16 26	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)$
28		eqid	$⊢ OrdIso (r, u) = OrdIso (r, u)$
29		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)⟩)$
30		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}$
31		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)⟩\})$
32		oveq2	$⊢ n = k \to u^{n} = u^{k}$
33	32	cbviunv	$⊢ ⋃_{n \in ω} (u^{n}) = ⋃_{k \in ω} (u^{k})$
34	33	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)⟩)$
35		eqid	$⊢ (x \in ω, y \in u ⟼ ⟨OrdIso (r, u) (x), y⟩) = (x \in ω, y \in u ⟼ ⟨OrdIso (r, u) (x), y⟩)$
36		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)⟩)$
37	12 13 14 15 27 28 29 30 31 34 35 36	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}))$
38	37	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})$
39	38	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})$
40		brdomi	$⊢ 𝒫 A ≼ ⋃_{n \in ω} (A^{n}) \to \exists g g : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
41	39 40	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})$
42	41	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}))$
43	42	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}))$
44	7 43	mpi	$⊢ (h : ω \underset{1-1 onto}{⟶} t \land t \subseteq A) \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n})$
45	44	ex	$⊢ h : ω \underset{1-1 onto}{⟶} t \to (t \subseteq A \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n}))$
46	45	exlimiv	$⊢ \exists h h : ω \underset{1-1 onto}{⟶} t \to (t \subseteq A \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n}))$
47	4 46	sylbi	$⊢ ω \approx t \to (t \subseteq A \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n}))$
48	47	imp	$⊢ (ω \approx t \land t \subseteq A) \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n})$
49	48	exlimiv	$⊢ \exists t (ω \approx t \land t \subseteq A) \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n})$
50	3 49	biimtrdi	$⊢ A \in V \to (ω ≼ A \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n}))$
51	2 50	mpcom	$⊢ ω ≼ A \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n})$

Metamath Proof Explorer

Theorem pwfseq

Proof