infpwfien

Description: Any infinite well-orderable set is equinumerous to its set of finite subsets. (Contributed by Mario Carneiro, 18-May-2015)

		Ref	Expression
	Assertion	infpwfien	$⊢ (A \in dom card \land ω ≼ A) \to (𝒫 A \cap Fin) \approx A$

Proof

Step	Hyp	Ref	Expression
1		infxpidm2	$⊢ (A \in dom card \land ω ≼ A) \to (A \times A) \approx A$
2		infn0	$⊢ ω ≼ A \to A \neq \emptyset$
3	2	adantl	$⊢ (A \in dom card \land ω ≼ A) \to A \neq \emptyset$
4		fseqen	$⊢ ((A \times A) \approx A \land A \neq \emptyset) \to ⋃_{n \in ω} (A^{n}) \approx (ω \times A)$
5	1 3 4	syl2anc	$⊢ (A \in dom card \land ω ≼ A) \to ⋃_{n \in ω} (A^{n}) \approx (ω \times A)$
6		xpdom1g	$⊢ (A \in dom card \land ω ≼ A) \to (ω \times A) ≼ (A \times A)$
7		domentr	$⊢ ((ω \times A) ≼ (A \times A) \land (A \times A) \approx A) \to (ω \times A) ≼ A$
8	6 1 7	syl2anc	$⊢ (A \in dom card \land ω ≼ A) \to (ω \times A) ≼ A$
9		endomtr	$⊢ (⋃_{n \in ω} (A^{n}) \approx (ω \times A) \land (ω \times A) ≼ A) \to ⋃_{n \in ω} (A^{n}) ≼ A$
10	5 8 9	syl2anc	$⊢ (A \in dom card \land ω ≼ A) \to ⋃_{n \in ω} (A^{n}) ≼ A$
11		numdom	$⊢ (A \in dom card \land ⋃_{n \in ω} (A^{n}) ≼ A) \to ⋃_{n \in ω} (A^{n}) \in dom card$
12	10 11	syldan	$⊢ (A \in dom card \land ω ≼ A) \to ⋃_{n \in ω} (A^{n}) \in dom card$
13		eliun	$⊢ x \in ⋃_{n \in ω} (A^{n}) \leftrightarrow \exists n \in ω x \in (A^{n})$
14		elmapi	$⊢ x \in (A^{n}) \to x : n ⟶ A$
15	14	ad2antll	$⊢ ((A \in dom card \land ω ≼ A) \land (n \in ω \land x \in (A^{n}))) \to x : n ⟶ A$
16	15	frnd	$⊢ ((A \in dom card \land ω ≼ A) \land (n \in ω \land x \in (A^{n}))) \to ran x \subseteq A$
17		vex	$⊢ x \in V$
18	17	rnex	$⊢ ran x \in V$
19	18	elpw	$⊢ ran x \in 𝒫 A \leftrightarrow ran x \subseteq A$
20	16 19	sylibr	$⊢ ((A \in dom card \land ω ≼ A) \land (n \in ω \land x \in (A^{n}))) \to ran x \in 𝒫 A$
21		simprl	$⊢ ((A \in dom card \land ω ≼ A) \land (n \in ω \land x \in (A^{n}))) \to n \in ω$
22		ssid	$⊢ n \subseteq n$
23		ssnnfi	$⊢ (n \in ω \land n \subseteq n) \to n \in Fin$
24	21 22 23	sylancl	$⊢ ((A \in dom card \land ω ≼ A) \land (n \in ω \land x \in (A^{n}))) \to n \in Fin$
25		ffn	$⊢ x : n ⟶ A \to x Fn n$
26		dffn4	$⊢ x Fn n \leftrightarrow x : n \underset{onto}{⟶} ran x$
27	25 26	sylib	$⊢ x : n ⟶ A \to x : n \underset{onto}{⟶} ran x$
28	15 27	syl	$⊢ ((A \in dom card \land ω ≼ A) \land (n \in ω \land x \in (A^{n}))) \to x : n \underset{onto}{⟶} ran x$
29		fofi	$⊢ (n \in Fin \land x : n \underset{onto}{⟶} ran x) \to ran x \in Fin$
30	24 28 29	syl2anc	$⊢ ((A \in dom card \land ω ≼ A) \land (n \in ω \land x \in (A^{n}))) \to ran x \in Fin$
31	20 30	elind	$⊢ ((A \in dom card \land ω ≼ A) \land (n \in ω \land x \in (A^{n}))) \to ran x \in (𝒫 A \cap Fin)$
32	31	expr	$⊢ ((A \in dom card \land ω ≼ A) \land n \in ω) \to (x \in (A^{n}) \to ran x \in (𝒫 A \cap Fin))$
33	32	rexlimdva	$⊢ (A \in dom card \land ω ≼ A) \to (\exists n \in ω x \in (A^{n}) \to ran x \in (𝒫 A \cap Fin))$
34	13 33	biimtrid	$⊢ (A \in dom card \land ω ≼ A) \to (x \in ⋃_{n \in ω} (A^{n}) \to ran x \in (𝒫 A \cap Fin))$
35	34	imp	$⊢ ((A \in dom card \land ω ≼ A) \land x \in ⋃_{n \in ω} (A^{n})) \to ran x \in (𝒫 A \cap Fin)$
36	35	fmpttd	$⊢ (A \in dom card \land ω ≼ A) \to (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x) : ⋃_{n \in ω} (A^{n}) ⟶ 𝒫 A \cap Fin$
37	36	ffnd	$⊢ (A \in dom card \land ω ≼ A) \to (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x) Fn ⋃_{n \in ω} (A^{n})$
38	36	frnd	$⊢ (A \in dom card \land ω ≼ A) \to ran (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x) \subseteq 𝒫 A \cap Fin$
39		simpr	$⊢ ((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \to y \in (𝒫 A \cap Fin)$
40	39	elin2d	$⊢ ((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \to y \in Fin$
41		isfi	$⊢ y \in Fin \leftrightarrow \exists m \in ω y \approx m$
42	40 41	sylib	$⊢ ((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \to \exists m \in ω y \approx m$
43		ensym	$⊢ y \approx m \to m \approx y$
44		bren	$⊢ m \approx y \leftrightarrow \exists x x : m \underset{1-1 onto}{⟶} y$
45	43 44	sylib	$⊢ y \approx m \to \exists x x : m \underset{1-1 onto}{⟶} y$
46		simprl	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to m \in ω$
47		f1of	$⊢ x : m \underset{1-1 onto}{⟶} y \to x : m ⟶ y$
48	47	ad2antll	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to x : m ⟶ y$
49		simplr	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to y \in (𝒫 A \cap Fin)$
50	49	elin1d	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to y \in 𝒫 A$
51	50	elpwid	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to y \subseteq A$
52	48 51	fssd	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to x : m ⟶ A$
53		simplll	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to A \in dom card$
54		vex	$⊢ m \in V$
55		elmapg	$⊢ (A \in dom card \land m \in V) \to (x \in (A^{m}) \leftrightarrow x : m ⟶ A)$
56	53 54 55	sylancl	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to (x \in (A^{m}) \leftrightarrow x : m ⟶ A)$
57	52 56	mpbird	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to x \in (A^{m})$
58		oveq2	$⊢ n = m \to A^{n} = A^{m}$
59	58	eleq2d	$⊢ n = m \to (x \in (A^{n}) \leftrightarrow x \in (A^{m}))$
60	59	rspcev	$⊢ (m \in ω \land x \in (A^{m})) \to \exists n \in ω x \in (A^{n})$
61	46 57 60	syl2anc	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to \exists n \in ω x \in (A^{n})$
62	61 13	sylibr	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to x \in ⋃_{n \in ω} (A^{n})$
63		f1ofo	$⊢ x : m \underset{1-1 onto}{⟶} y \to x : m \underset{onto}{⟶} y$
64	63	ad2antll	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to x : m \underset{onto}{⟶} y$
65		forn	$⊢ x : m \underset{onto}{⟶} y \to ran x = y$
66	64 65	syl	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to ran x = y$
67	66	eqcomd	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to y = ran x$
68	62 67	jca	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land (m \in ω \land x : m \underset{1-1 onto}{⟶} y)) \to (x \in ⋃_{n \in ω} (A^{n}) \land y = ran x)$
69	68	expr	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land m \in ω) \to (x : m \underset{1-1 onto}{⟶} y \to (x \in ⋃_{n \in ω} (A^{n}) \land y = ran x))$
70	69	eximdv	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land m \in ω) \to (\exists x x : m \underset{1-1 onto}{⟶} y \to \exists x (x \in ⋃_{n \in ω} (A^{n}) \land y = ran x))$
71	45 70	syl5	$⊢ (((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \land m \in ω) \to (y \approx m \to \exists x (x \in ⋃_{n \in ω} (A^{n}) \land y = ran x))$
72	71	rexlimdva	$⊢ ((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \to (\exists m \in ω y \approx m \to \exists x (x \in ⋃_{n \in ω} (A^{n}) \land y = ran x))$
73	42 72	mpd	$⊢ ((A \in dom card \land ω ≼ A) \land y \in (𝒫 A \cap Fin)) \to \exists x (x \in ⋃_{n \in ω} (A^{n}) \land y = ran x)$
74	73	ex	$⊢ (A \in dom card \land ω ≼ A) \to (y \in (𝒫 A \cap Fin) \to \exists x (x \in ⋃_{n \in ω} (A^{n}) \land y = ran x))$
75		eqid	$⊢ (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x) = (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x)$
76	75	elrnmpt	$⊢ y \in V \to (y \in ran (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x) \leftrightarrow \exists x \in ⋃_{n \in ω} (A^{n}) y = ran x)$
77	76	elv	$⊢ y \in ran (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x) \leftrightarrow \exists x \in ⋃_{n \in ω} (A^{n}) y = ran x$
78		df-rex	$⊢ \exists x \in ⋃_{n \in ω} (A^{n}) y = ran x \leftrightarrow \exists x (x \in ⋃_{n \in ω} (A^{n}) \land y = ran x)$
79	77 78	bitri	$⊢ y \in ran (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x) \leftrightarrow \exists x (x \in ⋃_{n \in ω} (A^{n}) \land y = ran x)$
80	74 79	imbitrrdi	$⊢ (A \in dom card \land ω ≼ A) \to (y \in (𝒫 A \cap Fin) \to y \in ran (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x))$
81	80	ssrdv	$⊢ (A \in dom card \land ω ≼ A) \to 𝒫 A \cap Fin \subseteq ran (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x)$
82	38 81	eqssd	$⊢ (A \in dom card \land ω ≼ A) \to ran (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x) = 𝒫 A \cap Fin$
83		df-fo	$⊢ (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x) : ⋃_{n \in ω} (A^{n}) \underset{onto}{⟶} 𝒫 A \cap Fin \leftrightarrow ((x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x) Fn ⋃_{n \in ω} (A^{n}) \land ran (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x) = 𝒫 A \cap Fin)$
84	37 82 83	sylanbrc	$⊢ (A \in dom card \land ω ≼ A) \to (x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x) : ⋃_{n \in ω} (A^{n}) \underset{onto}{⟶} 𝒫 A \cap Fin$
85		fodomnum	$⊢ ⋃_{n \in ω} (A^{n}) \in dom card \to ((x \in ⋃_{n \in ω} (A^{n}) ⟼ ran x) : ⋃_{n \in ω} (A^{n}) \underset{onto}{⟶} 𝒫 A \cap Fin \to (𝒫 A \cap Fin) ≼ ⋃_{n \in ω} (A^{n}))$
86	12 84 85	sylc	$⊢ (A \in dom card \land ω ≼ A) \to (𝒫 A \cap Fin) ≼ ⋃_{n \in ω} (A^{n})$
87		domtr	$⊢ ((𝒫 A \cap Fin) ≼ ⋃_{n \in ω} (A^{n}) \land ⋃_{n \in ω} (A^{n}) ≼ A) \to (𝒫 A \cap Fin) ≼ A$
88	86 10 87	syl2anc	$⊢ (A \in dom card \land ω ≼ A) \to (𝒫 A \cap Fin) ≼ A$
89		pwexg	$⊢ A \in dom card \to 𝒫 A \in V$
90	89	adantr	$⊢ (A \in dom card \land ω ≼ A) \to 𝒫 A \in V$
91		inex1g	$⊢ 𝒫 A \in V \to 𝒫 A \cap Fin \in V$
92	90 91	syl	$⊢ (A \in dom card \land ω ≼ A) \to 𝒫 A \cap Fin \in V$
93		infpwfidom	$⊢ 𝒫 A \cap Fin \in V \to A ≼ (𝒫 A \cap Fin)$
94	92 93	syl	$⊢ (A \in dom card \land ω ≼ A) \to A ≼ (𝒫 A \cap Fin)$
95		sbth	$⊢ ((𝒫 A \cap Fin) ≼ A \land A ≼ (𝒫 A \cap Fin)) \to (𝒫 A \cap Fin) \approx A$
96	88 94 95	syl2anc	$⊢ (A \in dom card \land ω ≼ A) \to (𝒫 A \cap Fin) \approx A$

Metamath Proof Explorer

Theorem infpwfien

Proof