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	|- F/_ x A
Assertion	mptctf	|- ( A ~<_ _om -> ( x e. A |-> B ) ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		mptctf.1	|- F/_ x A
2		funmpt	|- Fun ( x e. A |-> B )
3		ctex	|- ( A ~<_ _om -> A e. _V )
4		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
5	4	dmmpt	|- dom ( x e. A |-> B ) = { x e. A | B e. _V }
6		df-rab	|- { x e. A | B e. _V } = { x | ( x e. A /\ B e. _V ) }
7		simpl	|- ( ( x e. A /\ B e. _V ) -> x e. A )
8	7	ss2abi	|- { x | ( x e. A /\ B e. _V ) } C_ { x | x e. A }
9	1	abid2f	|- { x | x e. A } = A
10	8 9	sseqtri	|- { x | ( x e. A /\ B e. _V ) } C_ A
11	6 10	eqsstri	|- { x e. A | B e. _V } C_ A
12	5 11	eqsstri	|- dom ( x e. A |-> B ) C_ A
13		ssdomg	|- ( A e. _V -> ( dom ( x e. A |-> B ) C_ A -> dom ( x e. A |-> B ) ~<_ A ) )
14	3 12 13	mpisyl	|- ( A ~<_ _om -> dom ( x e. A |-> B ) ~<_ A )
15		domtr	|- ( ( dom ( x e. A |-> B ) ~<_ A /\ A ~<_ _om ) -> dom ( x e. A |-> B ) ~<_ _om )
16	14 15	mpancom	|- ( A ~<_ _om -> dom ( x e. A |-> B ) ~<_ _om )
17		funfn	|- ( Fun ( x e. A |-> B ) <-> ( x e. A |-> B ) Fn dom ( x e. A |-> B ) )
18		fnct	|- ( ( ( x e. A |-> B ) Fn dom ( x e. A |-> B ) /\ dom ( x e. A |-> B ) ~<_ _om ) -> ( x e. A |-> B ) ~<_ _om )
19	17 18	sylanb	|- ( ( Fun ( x e. A |-> B ) /\ dom ( x e. A |-> B ) ~<_ _om ) -> ( x e. A |-> B ) ~<_ _om )
20	2 16 19	sylancr	|- ( A ~<_ _om -> ( x e. A |-> B ) ~<_ _om )