This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )