mpct

Description: The exponentiation of a countable set to a finite set is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	mpct.a	$⊢ φ \to A ≼ ω$
	mpct.b	$⊢ φ \to B \in Fin$
Assertion	mpct	$⊢ φ \to (A^{B}) ≼ ω$

Proof

Step	Hyp	Ref	Expression
1		mpct.a	$⊢ φ \to A ≼ ω$
2		mpct.b	$⊢ φ \to B \in Fin$
3		oveq2	$⊢ x = \emptyset \to A^{x} = A^{\emptyset}$
4	3	breq1d	$⊢ x = \emptyset \to ((A^{x}) ≼ ω \leftrightarrow (A^{\emptyset}) ≼ ω)$
5		oveq2	$⊢ x = y \to A^{x} = A^{y}$
6	5	breq1d	$⊢ x = y \to ((A^{x}) ≼ ω \leftrightarrow (A^{y}) ≼ ω)$
7		oveq2	$⊢ x = y \cup \{z\} \to A^{x} = A^{(y \cup \{z\})}$
8	7	breq1d	$⊢ x = y \cup \{z\} \to ((A^{x}) ≼ ω \leftrightarrow (A^{(y \cup \{z\})}) ≼ ω)$
9		oveq2	$⊢ x = B \to A^{x} = A^{B}$
10	9	breq1d	$⊢ x = B \to ((A^{x}) ≼ ω \leftrightarrow (A^{B}) ≼ ω)$
11		ctex	$⊢ A ≼ ω \to A \in V$
12	1 11	syl	$⊢ φ \to A \in V$
13		mapdm0	$⊢ A \in V \to A^{\emptyset} = \{\emptyset\}$
14	12 13	syl	$⊢ φ \to A^{\emptyset} = \{\emptyset\}$
15		snfi	$⊢ \{\emptyset\} \in Fin$
16		fict	$⊢ \{\emptyset\} \in Fin \to \{\emptyset\} ≼ ω$
17	15 16	ax-mp	$⊢ \{\emptyset\} ≼ ω$
18	17	a1i	$⊢ φ \to \{\emptyset\} ≼ ω$
19	14 18	eqbrtrd	$⊢ φ \to (A^{\emptyset}) ≼ ω$
20		vex	$⊢ y \in V$
21	20	a1i	$⊢ ((φ \land (y \subseteq B \land z \in (B ∖ y))) \land (A^{y}) ≼ ω) \to y \in V$
22		snex	$⊢ \{z\} \in V$
23	22	a1i	$⊢ ((φ \land (y \subseteq B \land z \in (B ∖ y))) \land (A^{y}) ≼ ω) \to \{z\} \in V$
24	12	ad2antrr	$⊢ ((φ \land (y \subseteq B \land z \in (B ∖ y))) \land (A^{y}) ≼ ω) \to A \in V$
25		eldifn	$⊢ z \in (B ∖ y) \to \neg z \in y$
26		disjsn	$⊢ y \cap \{z\} = \emptyset \leftrightarrow \neg z \in y$
27	25 26	sylibr	$⊢ z \in (B ∖ y) \to y \cap \{z\} = \emptyset$
28	27	adantl	$⊢ (y \subseteq B \land z \in (B ∖ y)) \to y \cap \{z\} = \emptyset$
29	28	ad2antlr	$⊢ ((φ \land (y \subseteq B \land z \in (B ∖ y))) \land (A^{y}) ≼ ω) \to y \cap \{z\} = \emptyset$
30		mapunen	$⊢ ((y \in V \land \{z\} \in V \land A \in V) \land y \cap \{z\} = \emptyset) \to (A^{(y \cup \{z\})}) \approx ((A^{y}) \times (A^{\{z\}}))$
31	21 23 24 29 30	syl31anc	$⊢ ((φ \land (y \subseteq B \land z \in (B ∖ y))) \land (A^{y}) ≼ ω) \to (A^{(y \cup \{z\})}) \approx ((A^{y}) \times (A^{\{z\}}))$
32		simpr	$⊢ ((φ \land (y \subseteq B \land z \in (B ∖ y))) \land (A^{y}) ≼ ω) \to (A^{y}) ≼ ω$
33		vex	$⊢ z \in V$
34	33	a1i	$⊢ φ \to z \in V$
35	12 34	mapsnend	$⊢ φ \to (A^{\{z\}}) \approx A$
36		endomtr	$⊢ ((A^{\{z\}}) \approx A \land A ≼ ω) \to (A^{\{z\}}) ≼ ω$
37	35 1 36	syl2anc	$⊢ φ \to (A^{\{z\}}) ≼ ω$
38	37	ad2antrr	$⊢ ((φ \land (y \subseteq B \land z \in (B ∖ y))) \land (A^{y}) ≼ ω) \to (A^{\{z\}}) ≼ ω$
39		xpct	$⊢ ((A^{y}) ≼ ω \land (A^{\{z\}}) ≼ ω) \to ((A^{y}) \times (A^{\{z\}})) ≼ ω$
40	32 38 39	syl2anc	$⊢ ((φ \land (y \subseteq B \land z \in (B ∖ y))) \land (A^{y}) ≼ ω) \to ((A^{y}) \times (A^{\{z\}})) ≼ ω$
41		endomtr	$⊢ ((A^{(y \cup \{z\})}) \approx ((A^{y}) \times (A^{\{z\}})) \land ((A^{y}) \times (A^{\{z\}})) ≼ ω) \to (A^{(y \cup \{z\})}) ≼ ω$
42	31 40 41	syl2anc	$⊢ ((φ \land (y \subseteq B \land z \in (B ∖ y))) \land (A^{y}) ≼ ω) \to (A^{(y \cup \{z\})}) ≼ ω$
43	42	ex	$⊢ (φ \land (y \subseteq B \land z \in (B ∖ y))) \to ((A^{y}) ≼ ω \to (A^{(y \cup \{z\})}) ≼ ω)$
44	4 6 8 10 19 43 2	findcard2d	$⊢ φ \to (A^{B}) ≼ ω$

Metamath Proof Explorer

Theorem mpct

Proof