Metamath Proof Explorer

Theorem padct

Description: Index a countable set with integers and pad with Z . (Contributed by Thierry Arnoux, 1-Jun-2020)

Ref Expression
Assertion padct 
|- ( ( A ~<_ _om /\ Z e. V /\ -. Z e. A ) -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )

Proof

Step Hyp Ref Expression
1 brdom2 
 |-  ( A ~<_ _om <-> ( A ~< _om \/ A ~~ _om ) )
2 nfv 
 |-  F/ g ( A ~< _om /\ Z e. V /\ -. Z e. A )
3 nfv 
 |-  F/ g E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) )
4 isfinite2 
 |-  ( A ~< _om -> A e. Fin )
5 isfinite4 
 |-  ( A e. Fin <-> ( 1 ... ( # ` A ) ) ~~ A )
6 4 5 sylib 
 |-  ( A ~< _om -> ( 1 ... ( # ` A ) ) ~~ A )
7 6 adantr 
 |-  ( ( A ~< _om /\ Z e. V ) -> ( 1 ... ( # ` A ) ) ~~ A )
8 bren 
 |-  ( ( 1 ... ( # ` A ) ) ~~ A <-> E. g g : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
9 7 8 sylib 
 |-  ( ( A ~< _om /\ Z e. V ) -> E. g g : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
10 9 3adant3 
 |-  ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) -> E. g g : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
11 f1of 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> g : ( 1 ... ( # ` A ) ) --> A )
12 11 adantl 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> g : ( 1 ... ( # ` A ) ) --> A )
13 fconstmpt 
 |-  ( ( NN \ ( 1 ... ( # ` A ) ) ) X. { Z } ) = ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z )
14 13 eqcomi 
 |-  ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) = ( ( NN \ ( 1 ... ( # ` A ) ) ) X. { Z } )
15 simplr 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> Z e. V )
16 fconst2g 
 |-  ( Z e. V -> ( ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) : ( NN \ ( 1 ... ( # ` A ) ) ) --> { Z } <-> ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) = ( ( NN \ ( 1 ... ( # ` A ) ) ) X. { Z } ) ) )
17 15 16 syl 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) : ( NN \ ( 1 ... ( # ` A ) ) ) --> { Z } <-> ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) = ( ( NN \ ( 1 ... ( # ` A ) ) ) X. { Z } ) ) )
18 14 17 mpbiri 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) : ( NN \ ( 1 ... ( # ` A ) ) ) --> { Z } )
19 disjdif 
 |-  ( ( 1 ... ( # ` A ) ) i^i ( NN \ ( 1 ... ( # ` A ) ) ) ) = (/)
20 19 a1i 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( ( 1 ... ( # ` A ) ) i^i ( NN \ ( 1 ... ( # ` A ) ) ) ) = (/) )
21 fun 
 |-  ( ( ( g : ( 1 ... ( # ` A ) ) --> A /\ ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) : ( NN \ ( 1 ... ( # ` A ) ) ) --> { Z } ) /\ ( ( 1 ... ( # ` A ) ) i^i ( NN \ ( 1 ... ( # ` A ) ) ) ) = (/) ) -> ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) : ( ( 1 ... ( # ` A ) ) u. ( NN \ ( 1 ... ( # ` A ) ) ) ) --> ( A u. { Z } ) )
22 12 18 20 21 syl21anc 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) : ( ( 1 ... ( # ` A ) ) u. ( NN \ ( 1 ... ( # ` A ) ) ) ) --> ( A u. { Z } ) )
23 fz1ssnn 
 |-  ( 1 ... ( # ` A ) ) C_ NN
24 undif 
 |-  ( ( 1 ... ( # ` A ) ) C_ NN <-> ( ( 1 ... ( # ` A ) ) u. ( NN \ ( 1 ... ( # ` A ) ) ) ) = NN )
25 23 24 mpbi 
 |-  ( ( 1 ... ( # ` A ) ) u. ( NN \ ( 1 ... ( # ` A ) ) ) ) = NN
26 25 feq2i 
 |-  ( ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) : ( ( 1 ... ( # ` A ) ) u. ( NN \ ( 1 ... ( # ` A ) ) ) ) --> ( A u. { Z } ) <-> ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) : NN --> ( A u. { Z } ) )
27 22 26 sylib 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) : NN --> ( A u. { Z } ) )
28 27 3adantl3 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) : NN --> ( A u. { Z } ) )
29 ssid 
 |-  A C_ A
30 simpr 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> g : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
31 f1ofo 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> g : ( 1 ... ( # ` A ) ) -onto-> A )
32 forn 
 |-  ( g : ( 1 ... ( # ` A ) ) -onto-> A -> ran g = A )
33 30 31 32 3syl 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ran g = A )
34 29 33 sseqtrrid 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> A C_ ran g )
35 34 orcd 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( A C_ ran g \/ A C_ ran ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) )
36 ssun 
 |-  ( ( A C_ ran g \/ A C_ ran ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) -> A C_ ( ran g u. ran ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) )
37 35 36 syl 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> A C_ ( ran g u. ran ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) )
38 rnun 
 |-  ran ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) = ( ran g u. ran ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) )
39 37 38 sseqtrrdi 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> A C_ ran ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) )
40 39 3adantl3 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> A C_ ran ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) )
41 dff1o3 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A <-> ( g : ( 1 ... ( # ` A ) ) -onto-> A /\ Fun `' g ) )
42 41 simprbi 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> Fun `' g )
43 42 adantl 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> Fun `' g )
44 cnvun 
 |-  `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) = ( `' g u. `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) )
45 44 reseq1i 
 |-  ( `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) = ( ( `' g u. `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A )
46 resundir 
 |-  ( ( `' g u. `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) = ( ( `' g |` A ) u. ( `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) |` A ) )
47 45 46 eqtri 
 |-  ( `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) = ( ( `' g |` A ) u. ( `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) |` A ) )
48 dff1o4 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A <-> ( g Fn ( 1 ... ( # ` A ) ) /\ `' g Fn A ) )
49 48 simprbi 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> `' g Fn A )
50 fnresdm 
 |-  ( `' g Fn A -> ( `' g |` A ) = `' g )
51 49 50 syl 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ( `' g |` A ) = `' g )
52 51 adantl 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( `' g |` A ) = `' g )
53 simpl3 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> -. Z e. A )
54 14 cnveqi 
 |-  `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) = `' ( ( NN \ ( 1 ... ( # ` A ) ) ) X. { Z } )
55 cnvxp 
 |-  `' ( ( NN \ ( 1 ... ( # ` A ) ) ) X. { Z } ) = ( { Z } X. ( NN \ ( 1 ... ( # ` A ) ) ) )
56 54 55 eqtri 
 |-  `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) = ( { Z } X. ( NN \ ( 1 ... ( # ` A ) ) ) )
57 56 reseq1i 
 |-  ( `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) |` A ) = ( ( { Z } X. ( NN \ ( 1 ... ( # ` A ) ) ) ) |` A )
58 incom 
 |-  ( A i^i { Z } ) = ( { Z } i^i A )
59 disjsn 
 |-  ( ( A i^i { Z } ) = (/) <-> -. Z e. A )
60 59 biimpri 
 |-  ( -. Z e. A -> ( A i^i { Z } ) = (/) )
61 58 60 eqtr3id 
 |-  ( -. Z e. A -> ( { Z } i^i A ) = (/) )
62 xpdisjres 
 |-  ( ( { Z } i^i A ) = (/) -> ( ( { Z } X. ( NN \ ( 1 ... ( # ` A ) ) ) ) |` A ) = (/) )
63 61 62 syl 
 |-  ( -. Z e. A -> ( ( { Z } X. ( NN \ ( 1 ... ( # ` A ) ) ) ) |` A ) = (/) )
64 57 63 syl5eq 
 |-  ( -. Z e. A -> ( `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) |` A ) = (/) )
65 53 64 syl 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) |` A ) = (/) )
66 52 65 uneq12d 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( ( `' g |` A ) u. ( `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) |` A ) ) = ( `' g u. (/) ) )
67 un0 
 |-  ( `' g u. (/) ) = `' g
68 66 67 eqtrdi 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( ( `' g |` A ) u. ( `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) |` A ) ) = `' g )
69 47 68 syl5eq 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) = `' g )
70 69 funeqd 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( Fun ( `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) <-> Fun `' g ) )
71 43 70 mpbird 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> Fun ( `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) )
72 vex 
 |-  g e. _V
73 nnex 
 |-  NN e. _V
74 difexg 
 |-  ( NN e. _V -> ( NN \ ( 1 ... ( # ` A ) ) ) e. _V )
75 73 74 ax-mp 
 |-  ( NN \ ( 1 ... ( # ` A ) ) ) e. _V
76 75 mptex 
 |-  ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) e. _V
77 72 76 unex 
 |-  ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) e. _V
78 feq1 
 |-  ( f = ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) -> ( f : NN --> ( A u. { Z } ) <-> ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) : NN --> ( A u. { Z } ) ) )
79 rneq 
 |-  ( f = ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) -> ran f = ran ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) )
80 79 sseq2d 
 |-  ( f = ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) -> ( A C_ ran f <-> A C_ ran ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) ) )
81 cnveq 
 |-  ( f = ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) -> `' f = `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) )
82 eqidd 
 |-  ( f = ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) -> A = A )
83 81 82 reseq12d 
 |-  ( f = ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) -> ( `' f |` A ) = ( `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) )
84 83 funeqd 
 |-  ( f = ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) -> ( Fun ( `' f |` A ) <-> Fun ( `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) ) )
85 78 80 84 3anbi123d 
 |-  ( f = ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) -> ( ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) <-> ( ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) : NN --> ( A u. { Z } ) /\ A C_ ran ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) /\ Fun ( `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) ) ) )
86 77 85 spcev 
 |-  ( ( ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) : NN --> ( A u. { Z } ) /\ A C_ ran ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) /\ Fun ( `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) ) -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )
87 28 40 71 86 syl3anc 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )
88 87 ex 
 |-  ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) -> ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) )
89 2 3 10 88 exlimimdd 
 |-  ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )
90 89 3expia 
 |-  ( ( A ~< _om /\ Z e. V ) -> ( -. Z e. A -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) )
91 nnenom 
 |-  NN ~~ _om
92 simpl 
 |-  ( ( A ~~ _om /\ Z e. V ) -> A ~~ _om )
93 92 ensymd 
 |-  ( ( A ~~ _om /\ Z e. V ) -> _om ~~ A )
94 entr 
 |-  ( ( NN ~~ _om /\ _om ~~ A ) -> NN ~~ A )
95 91 93 94 sylancr 
 |-  ( ( A ~~ _om /\ Z e. V ) -> NN ~~ A )
96 bren 
 |-  ( NN ~~ A <-> E. f f : NN -1-1-onto-> A )
97 95 96 sylib 
 |-  ( ( A ~~ _om /\ Z e. V ) -> E. f f : NN -1-1-onto-> A )
98 nfv 
 |-  F/ f ( A ~~ _om /\ Z e. V )
99 simpr 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> f : NN -1-1-onto-> A )
100 f1of 
 |-  ( f : NN -1-1-onto-> A -> f : NN --> A )
101 ssun1 
 |-  A C_ ( A u. { Z } )
102 fss 
 |-  ( ( f : NN --> A /\ A C_ ( A u. { Z } ) ) -> f : NN --> ( A u. { Z } ) )
103 101 102 mpan2 
 |-  ( f : NN --> A -> f : NN --> ( A u. { Z } ) )
104 99 100 103 3syl 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> f : NN --> ( A u. { Z } ) )
105 f1ofo 
 |-  ( f : NN -1-1-onto-> A -> f : NN -onto-> A )
106 forn 
 |-  ( f : NN -onto-> A -> ran f = A )
107 99 105 106 3syl 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> ran f = A )
108 29 107 sseqtrrid 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> A C_ ran f )
109 f1ocnv 
 |-  ( f : NN -1-1-onto-> A -> `' f : A -1-1-onto-> NN )
110 f1of1 
 |-  ( `' f : A -1-1-onto-> NN -> `' f : A -1-1-> NN )
111 99 109 110 3syl 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> `' f : A -1-1-> NN )
112 f1ores 
 |-  ( ( `' f : A -1-1-> NN /\ A C_ A ) -> ( `' f |` A ) : A -1-1-onto-> ( `' f " A ) )
113 29 112 mpan2 
 |-  ( `' f : A -1-1-> NN -> ( `' f |` A ) : A -1-1-onto-> ( `' f " A ) )
114 f1ofun 
 |-  ( ( `' f |` A ) : A -1-1-onto-> ( `' f " A ) -> Fun ( `' f |` A ) )
115 111 113 114 3syl 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> Fun ( `' f |` A ) )
116 104 108 115 3jca 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )
117 116 ex 
 |-  ( ( A ~~ _om /\ Z e. V ) -> ( f : NN -1-1-onto-> A -> ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) )
118 98 117 eximd 
 |-  ( ( A ~~ _om /\ Z e. V ) -> ( E. f f : NN -1-1-onto-> A -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) )
119 97 118 mpd 
 |-  ( ( A ~~ _om /\ Z e. V ) -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )
120 119 a1d 
 |-  ( ( A ~~ _om /\ Z e. V ) -> ( -. Z e. A -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) )
121 90 120 jaoian 
 |-  ( ( ( A ~< _om \/ A ~~ _om ) /\ Z e. V ) -> ( -. Z e. A -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) )
122 121 3impia 
 |-  ( ( ( A ~< _om \/ A ~~ _om ) /\ Z e. V /\ -. Z e. A ) -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )
123 1 122 syl3an1b 
 |-  ( ( A ~<_ _om /\ Z e. V /\ -. Z e. A ) -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )