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

Metamath Proof Explorer

Theorem pwfseq

Proof