fseqen

Description: A set that is equinumerous to its Cartesian product is equinumerous to the set of finite sequences on it. (This can be proven more easily using some choice but this proof avoids it.) (Contributed by Mario Carneiro, 18-Nov-2014)

		Ref	Expression
	Assertion	fseqen	$⊢ ((A \times A) \approx A \land A \neq \emptyset) \to ⋃_{n \in ω} (A^{n}) \approx (ω \times A)$

Proof

Step	Hyp	Ref	Expression
1		bren	$⊢ (A \times A) \approx A \leftrightarrow \exists f f : A \times A \underset{1-1 onto}{⟶} A$
2		n0	$⊢ A \neq \emptyset \leftrightarrow \exists b b \in A$
3		exdistrv	$⊢ \exists f \exists b (f : A \times A \underset{1-1 onto}{⟶} A \land b \in A) \leftrightarrow (\exists f f : A \times A \underset{1-1 onto}{⟶} A \land \exists b b \in A)$
4		omex	$⊢ ω \in V$
5		simpl	$⊢ (f : A \times A \underset{1-1 onto}{⟶} A \land b \in A) \to f : A \times A \underset{1-1 onto}{⟶} A$
6		f1ofo	$⊢ f : A \times A \underset{1-1 onto}{⟶} A \to f : A \times A \underset{onto}{⟶} A$
7		forn	$⊢ f : A \times A \underset{onto}{⟶} A \to ran f = A$
8	5 6 7	3syl	$⊢ (f : A \times A \underset{1-1 onto}{⟶} A \land b \in A) \to ran f = A$
9		vex	$⊢ f \in V$
10	9	rnex	$⊢ ran f \in V$
11	8 10	eqeltrrdi	$⊢ (f : A \times A \underset{1-1 onto}{⟶} A \land b \in A) \to A \in V$
12		xpexg	$⊢ (ω \in V \land A \in V) \to ω \times A \in V$
13	4 11 12	sylancr	$⊢ (f : A \times A \underset{1-1 onto}{⟶} A \land b \in A) \to ω \times A \in V$
14		simpr	$⊢ (f : A \times A \underset{1-1 onto}{⟶} A \land b \in A) \to b \in A$
15		eqid	$⊢ {seq}_{ω} ((k \in V, g \in V ⟼ (y \in (A^{suc k}) ⟼ g ({y ↾}_{k}) f y (k))), \{⟨\emptyset, b⟩\}) = {seq}_{ω} ((k \in V, g \in V ⟼ (y \in (A^{suc k}) ⟼ g ({y ↾}_{k}) f y (k))), \{⟨\emptyset, b⟩\})$
16		eqid	$⊢ (x \in ⋃_{n \in ω} (A^{n}) ⟼ ⟨dom x, {seq}_{ω} ((k \in V, g \in V ⟼ (y \in (A^{suc k}) ⟼ g ({y ↾}_{k}) f y (k))), \{⟨\emptyset, b⟩\}) (dom x) (x)⟩) = (x \in ⋃_{n \in ω} (A^{n}) ⟼ ⟨dom x, {seq}_{ω} ((k \in V, g \in V ⟼ (y \in (A^{suc k}) ⟼ g ({y ↾}_{k}) f y (k))), \{⟨\emptyset, b⟩\}) (dom x) (x)⟩)$
17	11 14 5 15 16	fseqenlem2	$⊢ (f : A \times A \underset{1-1 onto}{⟶} A \land b \in A) \to (x \in ⋃_{n \in ω} (A^{n}) ⟼ ⟨dom x, {seq}_{ω} ((k \in V, g \in V ⟼ (y \in (A^{suc k}) ⟼ g ({y ↾}_{k}) f y (k))), \{⟨\emptyset, b⟩\}) (dom x) (x)⟩) : ⋃_{n \in ω} (A^{n}) \underset{1-1}{⟶} ω \times A$
18		f1domg	$⊢ ω \times A \in V \to ((x \in ⋃_{n \in ω} (A^{n}) ⟼ ⟨dom x, {seq}_{ω} ((k \in V, g \in V ⟼ (y \in (A^{suc k}) ⟼ g ({y ↾}_{k}) f y (k))), \{⟨\emptyset, b⟩\}) (dom x) (x)⟩) : ⋃_{n \in ω} (A^{n}) \underset{1-1}{⟶} ω \times A \to ⋃_{n \in ω} (A^{n}) ≼ (ω \times A))$
19	13 17 18	sylc	$⊢ (f : A \times A \underset{1-1 onto}{⟶} A \land b \in A) \to ⋃_{n \in ω} (A^{n}) ≼ (ω \times A)$
20		fseqdom	$⊢ A \in V \to (ω \times A) ≼ ⋃_{n \in ω} (A^{n})$
21	11 20	syl	$⊢ (f : A \times A \underset{1-1 onto}{⟶} A \land b \in A) \to (ω \times A) ≼ ⋃_{n \in ω} (A^{n})$
22		sbth	$⊢ (⋃_{n \in ω} (A^{n}) ≼ (ω \times A) \land (ω \times A) ≼ ⋃_{n \in ω} (A^{n})) \to ⋃_{n \in ω} (A^{n}) \approx (ω \times A)$
23	19 21 22	syl2anc	$⊢ (f : A \times A \underset{1-1 onto}{⟶} A \land b \in A) \to ⋃_{n \in ω} (A^{n}) \approx (ω \times A)$
24	23	exlimivv	$⊢ \exists f \exists b (f : A \times A \underset{1-1 onto}{⟶} A \land b \in A) \to ⋃_{n \in ω} (A^{n}) \approx (ω \times A)$
25	3 24	sylbir	$⊢ (\exists f f : A \times A \underset{1-1 onto}{⟶} A \land \exists b b \in A) \to ⋃_{n \in ω} (A^{n}) \approx (ω \times A)$
26	1 2 25	syl2anb	$⊢ ((A \times A) \approx A \land A \neq \emptyset) \to ⋃_{n \in ω} (A^{n}) \approx (ω \times A)$

Metamath Proof Explorer

Theorem fseqen

Proof