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	⊢ ( 𝜑 → 𝐴 ≼ ω )
	mpct.b	⊢ ( 𝜑 → 𝐵 ∈ Fin )
Assertion	mpct	⊢ ( 𝜑 → ( 𝐴 ↑_m 𝐵 ) ≼ ω )

Proof

Step	Hyp	Ref	Expression
1		mpct.a	⊢ ( 𝜑 → 𝐴 ≼ ω )
2		mpct.b	⊢ ( 𝜑 → 𝐵 ∈ Fin )
3		oveq2	⊢ ( 𝑥 = ∅ → ( 𝐴 ↑_m 𝑥 ) = ( 𝐴 ↑_m ∅ ) )
4	3	breq1d	⊢ ( 𝑥 = ∅ → ( ( 𝐴 ↑_m 𝑥 ) ≼ ω ↔ ( 𝐴 ↑_m ∅ ) ≼ ω ) )
5		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑_m 𝑥 ) = ( 𝐴 ↑_m 𝑦 ) )
6	5	breq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ↑_m 𝑥 ) ≼ ω ↔ ( 𝐴 ↑_m 𝑦 ) ≼ ω ) )
7		oveq2	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐴 ↑_m 𝑥 ) = ( 𝐴 ↑_m ( 𝑦 ∪ { 𝑧 } ) ) )
8	7	breq1d	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐴 ↑_m 𝑥 ) ≼ ω ↔ ( 𝐴 ↑_m ( 𝑦 ∪ { 𝑧 } ) ) ≼ ω ) )
9		oveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 ↑_m 𝑥 ) = ( 𝐴 ↑_m 𝐵 ) )
10	9	breq1d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ↑_m 𝑥 ) ≼ ω ↔ ( 𝐴 ↑_m 𝐵 ) ≼ ω ) )
11		ctex	⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V )
12	1 11	syl	⊢ ( 𝜑 → 𝐴 ∈ V )
13		mapdm0	⊢ ( 𝐴 ∈ V → ( 𝐴 ↑_m ∅ ) = { ∅ } )
14	12 13	syl	⊢ ( 𝜑 → ( 𝐴 ↑_m ∅ ) = { ∅ } )
15		snfi	⊢ { ∅ } ∈ Fin
16		fict	⊢ ( { ∅ } ∈ Fin → { ∅ } ≼ ω )
17	15 16	ax-mp	⊢ { ∅ } ≼ ω
18	17	a1i	⊢ ( 𝜑 → { ∅ } ≼ ω )
19	14 18	eqbrtrd	⊢ ( 𝜑 → ( 𝐴 ↑_m ∅ ) ≼ ω )
20		vex	⊢ 𝑦 ∈ V
21	20	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑_m 𝑦 ) ≼ ω ) → 𝑦 ∈ V )
22		vsnex	⊢ { 𝑧 } ∈ V
23	22	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑_m 𝑦 ) ≼ ω ) → { 𝑧 } ∈ V )
24	12	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑_m 𝑦 ) ≼ ω ) → 𝐴 ∈ V )
25		eldifn	⊢ ( 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) → ¬ 𝑧 ∈ 𝑦 )
26		disjsn	⊢ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑦 )
27	25 26	sylibr	⊢ ( 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
28	27	adantl	⊢ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
29	28	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑_m 𝑦 ) ≼ ω ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
30		mapunen	⊢ ( ( ( 𝑦 ∈ V ∧ { 𝑧 } ∈ V ∧ 𝐴 ∈ V ) ∧ ( 𝑦 ∩ { 𝑧 } ) = ∅ ) → ( 𝐴 ↑_m ( 𝑦 ∪ { 𝑧 } ) ) ≈ ( ( 𝐴 ↑_m 𝑦 ) × ( 𝐴 ↑_m { 𝑧 } ) ) )
31	21 23 24 29 30	syl31anc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑_m 𝑦 ) ≼ ω ) → ( 𝐴 ↑_m ( 𝑦 ∪ { 𝑧 } ) ) ≈ ( ( 𝐴 ↑_m 𝑦 ) × ( 𝐴 ↑_m { 𝑧 } ) ) )
32		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑_m 𝑦 ) ≼ ω ) → ( 𝐴 ↑_m 𝑦 ) ≼ ω )
33		vex	⊢ 𝑧 ∈ V
34	33	a1i	⊢ ( 𝜑 → 𝑧 ∈ V )
35	12 34	mapsnend	⊢ ( 𝜑 → ( 𝐴 ↑_m { 𝑧 } ) ≈ 𝐴 )
36		endomtr	⊢ ( ( ( 𝐴 ↑_m { 𝑧 } ) ≈ 𝐴 ∧ 𝐴 ≼ ω ) → ( 𝐴 ↑_m { 𝑧 } ) ≼ ω )
37	35 1 36	syl2anc	⊢ ( 𝜑 → ( 𝐴 ↑_m { 𝑧 } ) ≼ ω )
38	37	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑_m 𝑦 ) ≼ ω ) → ( 𝐴 ↑_m { 𝑧 } ) ≼ ω )
39		xpct	⊢ ( ( ( 𝐴 ↑_m 𝑦 ) ≼ ω ∧ ( 𝐴 ↑_m { 𝑧 } ) ≼ ω ) → ( ( 𝐴 ↑_m 𝑦 ) × ( 𝐴 ↑_m { 𝑧 } ) ) ≼ ω )
40	32 38 39	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑_m 𝑦 ) ≼ ω ) → ( ( 𝐴 ↑_m 𝑦 ) × ( 𝐴 ↑_m { 𝑧 } ) ) ≼ ω )
41		endomtr	⊢ ( ( ( 𝐴 ↑_m ( 𝑦 ∪ { 𝑧 } ) ) ≈ ( ( 𝐴 ↑_m 𝑦 ) × ( 𝐴 ↑_m { 𝑧 } ) ) ∧ ( ( 𝐴 ↑_m 𝑦 ) × ( 𝐴 ↑_m { 𝑧 } ) ) ≼ ω ) → ( 𝐴 ↑_m ( 𝑦 ∪ { 𝑧 } ) ) ≼ ω )
42	31 40 41	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) ∧ ( 𝐴 ↑_m 𝑦 ) ≼ ω ) → ( 𝐴 ↑_m ( 𝑦 ∪ { 𝑧 } ) ) ≼ ω )
43	42	ex	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝑦 ) ) ) → ( ( 𝐴 ↑_m 𝑦 ) ≼ ω → ( 𝐴 ↑_m ( 𝑦 ∪ { 𝑧 } ) ) ≼ ω ) )
44	4 6 8 10 19 43 2	findcard2d	⊢ ( 𝜑 → ( 𝐴 ↑_m 𝐵 ) ≼ ω )

Metamath Proof Explorer

Theorem mpct

Proof