Theorem mptct

Description: A countable mapping set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016)

	Ref	Expression
Assertion	mptct	|- ( A ~<_ _om -> ( x e. A |-> B ) ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		funmpt	|- Fun ( x e. A |-> B )
2		ctex	|- ( A ~<_ _om -> A e. _V )
3		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
4	3	dmmptss	|- dom ( x e. A |-> B ) C_ A
5		ssdomg	|- ( A e. _V -> ( dom ( x e. A |-> B ) C_ A -> dom ( x e. A |-> B ) ~<_ A ) )
6	2 4 5	mpisyl	|- ( A ~<_ _om -> dom ( x e. A |-> B ) ~<_ A )
7		domtr	|- ( ( dom ( x e. A |-> B ) ~<_ A /\ A ~<_ _om ) -> dom ( x e. A |-> B ) ~<_ _om )
8	6 7	mpancom	|- ( A ~<_ _om -> dom ( x e. A |-> B ) ~<_ _om )
9		funfn	|- ( Fun ( x e. A |-> B ) <-> ( x e. A |-> B ) Fn dom ( x e. A |-> B ) )
10		fnct	|- ( ( ( x e. A |-> B ) Fn dom ( x e. A |-> B ) /\ dom ( x e. A |-> B ) ~<_ _om ) -> ( x e. A |-> B ) ~<_ _om )
11	9 10	sylanb	|- ( ( Fun ( x e. A |-> B ) /\ dom ( x e. A |-> B ) ~<_ _om ) -> ( x e. A |-> B ) ~<_ _om )
12	1 8 11	sylancr	|- ( A ~<_ _om -> ( x e. A |-> B ) ~<_ _om )