Theorem mptctf

Description: A countable mapping set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017)

	Ref	Expression
Hypothesis	mptctf.1	⊢ Ⅎ 𝑥 𝐴
Assertion	mptctf	⊢ ( 𝐴 ≼ ω → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω )

Proof

Step	Hyp	Ref	Expression
1		mptctf.1	⊢ Ⅎ 𝑥 𝐴
2		funmpt	⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3		ctex	⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V )
4		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	4	dmmpt	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V }
6		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ V ) }
7		simpl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ V ) → 𝑥 ∈ 𝐴 )
8	7	ss2abi	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ V ) } ⊆ { 𝑥 ∣ 𝑥 ∈ 𝐴 }
9	1	abid2f	⊢ { 𝑥 ∣ 𝑥 ∈ 𝐴 } = 𝐴
10	8 9	sseqtri	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ V ) } ⊆ 𝐴
11	6 10	eqsstri	⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ⊆ 𝐴
12	5 11	eqsstri	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴
13		ssdomg	⊢ ( 𝐴 ∈ V → ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ 𝐴 ) )
14	3 12 13	mpisyl	⊢ ( 𝐴 ≼ ω → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ 𝐴 )
15		domtr	⊢ ( ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ 𝐴 ∧ 𝐴 ≼ ω ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω )
16	14 15	mpancom	⊢ ( 𝐴 ≼ ω → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω )
17		funfn	⊢ ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
18		fnct	⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω )
19	17 18	sylanb	⊢ ( ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω )
20	2 16 19	sylancr	⊢ ( 𝐴 ≼ ω → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω )