Metamath Proof Explorer

Theorem padct

Description: Index a countable set with integers and pad with Z . (Contributed by Thierry Arnoux, 1-Jun-2020) Avoid ax-rep . (Revised by GG, 2-Apr-2026)

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 isfinite2 
 |-  ( A ~< _om -> A e. Fin )
3 isfinite4 
 |-  ( A e. Fin <-> ( 1 ... ( # ` A ) ) ~~ A )
4 2 3 sylib 
 |-  ( A ~< _om -> ( 1 ... ( # ` A ) ) ~~ A )
5 4 adantr 
 |-  ( ( A ~< _om /\ Z e. V ) -> ( 1 ... ( # ` A ) ) ~~ A )
6 bren 
 |-  ( ( 1 ... ( # ` A ) ) ~~ A <-> E. g g : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
7 5 6 sylib 
 |-  ( ( A ~< _om /\ Z e. V ) -> E. g g : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
8 7 3adant3 
 |-  ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) -> E. g g : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
9 f1of 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> g : ( 1 ... ( # ` A ) ) --> A )
10 9 adantl 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> g : ( 1 ... ( # ` A ) ) --> A )
11 fconstmpt 
 |-  ( ( NN \ ( 1 ... ( # ` A ) ) ) X. { Z } ) = ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z )
12 11 eqcomi 
 |-  ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) = ( ( NN \ ( 1 ... ( # ` A ) ) ) X. { Z } )
13 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 } ) ) )
14 13 ad2antlr 
 |-  ( ( ( 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 } ) ) )
15 12 14 mpbiri 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) : ( NN \ ( 1 ... ( # ` A ) ) ) --> { Z } )
16 disjdif 
 |-  ( ( 1 ... ( # ` A ) ) i^i ( NN \ ( 1 ... ( # ` A ) ) ) ) = (/)
17 16 a1i 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( ( 1 ... ( # ` A ) ) i^i ( NN \ ( 1 ... ( # ` A ) ) ) ) = (/) )
18 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 } ) )
19 10 15 17 18 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 } ) )
20 fz1ssnn 
 |-  ( 1 ... ( # ` A ) ) C_ NN
21 undif 
 |-  ( ( 1 ... ( # ` A ) ) C_ NN <-> ( ( 1 ... ( # ` A ) ) u. ( NN \ ( 1 ... ( # ` A ) ) ) ) = NN )
22 20 21 mpbi 
 |-  ( ( 1 ... ( # ` A ) ) u. ( NN \ ( 1 ... ( # ` A ) ) ) ) = NN
23 22 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 } ) )
24 19 23 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 } ) )
25 24 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 } ) )
26 simpr 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> g : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
27 f1ofo 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> g : ( 1 ... ( # ` A ) ) -onto-> A )
28 forn 
 |-  ( g : ( 1 ... ( # ` A ) ) -onto-> A -> ran g = A )
29 26 27 28 3syl 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ran g = A )
30 ssun1 
 |-  ran g C_ ( ran g u. ran ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) )
31 29 30 eqsstrrdi 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> A C_ ( ran g u. ran ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) )
32 rnun 
 |-  ran ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) = ( ran g u. ran ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) )
33 31 32 sseqtrrdi 
 |-  ( ( ( A ~< _om /\ Z e. V ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> A C_ ran ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) )
34 33 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 ) ) )
35 dff1o3 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A <-> ( g : ( 1 ... ( # ` A ) ) -onto-> A /\ Fun `' g ) )
36 35 simprbi 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> Fun `' g )
37 36 adantl 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> Fun `' g )
38 cnvun 
 |-  `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) = ( `' g u. `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) )
39 38 reseq1i 
 |-  ( `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) = ( ( `' g u. `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A )
40 resundir 
 |-  ( ( `' g u. `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) = ( ( `' g |` A ) u. ( `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) |` A ) )
41 39 40 eqtri 
 |-  ( `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) = ( ( `' g |` A ) u. ( `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) |` A ) )
42 dff1o4 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A <-> ( g Fn ( 1 ... ( # ` A ) ) /\ `' g Fn A ) )
43 42 simprbi 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> `' g Fn A )
44 fnresdm 
 |-  ( `' g Fn A -> ( `' g |` A ) = `' g )
45 43 44 syl 
 |-  ( g : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ( `' g |` A ) = `' g )
46 45 adantl 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( `' g |` A ) = `' g )
47 simpl3 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> -. Z e. A )
48 12 cnveqi 
 |-  `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) = `' ( ( NN \ ( 1 ... ( # ` A ) ) ) X. { Z } )
49 cnvxp 
 |-  `' ( ( NN \ ( 1 ... ( # ` A ) ) ) X. { Z } ) = ( { Z } X. ( NN \ ( 1 ... ( # ` A ) ) ) )
50 48 49 eqtri 
 |-  `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) = ( { Z } X. ( NN \ ( 1 ... ( # ` A ) ) ) )
51 50 reseq1i 
 |-  ( `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) |` A ) = ( ( { Z } X. ( NN \ ( 1 ... ( # ` A ) ) ) ) |` A )
52 ineqcom 
 |-  ( ( { Z } i^i A ) = (/) <-> ( A i^i { Z } ) = (/) )
53 disjsn 
 |-  ( ( A i^i { Z } ) = (/) <-> -. Z e. A )
54 52 53 sylbbr 
 |-  ( -. Z e. A -> ( { Z } i^i A ) = (/) )
55 xpdisjres 
 |-  ( ( { Z } i^i A ) = (/) -> ( ( { Z } X. ( NN \ ( 1 ... ( # ` A ) ) ) ) |` A ) = (/) )
56 54 55 syl 
 |-  ( -. Z e. A -> ( ( { Z } X. ( NN \ ( 1 ... ( # ` A ) ) ) ) |` A ) = (/) )
57 51 56 eqtrid 
 |-  ( -. Z e. A -> ( `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) |` A ) = (/) )
58 47 57 syl 
 |-  ( ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) /\ g : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( `' ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) |` A ) = (/) )
59 46 58 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. (/) ) )
60 un0 
 |-  ( `' g u. (/) ) = `' g
61 59 60 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 )
62 41 61 eqtrid 
 |-  ( ( ( 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 )
63 62 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 ) )
64 37 63 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 ) )
65 vex 
 |-  g e. _V
66 nnex 
 |-  NN e. _V
67 66 difexi 
 |-  ( NN \ ( 1 ... ( # ` A ) ) ) e. _V
68 snex 
 |-  { Z } e. _V
69 67 68 xpex 
 |-  ( ( NN \ ( 1 ... ( # ` A ) ) ) X. { Z } ) e. _V
70 11 69 eqeltrri 
 |-  ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) e. _V
71 65 70 unex 
 |-  ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) e. _V
72 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 } ) ) )
73 rneq 
 |-  ( f = ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) -> ran f = ran ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) )
74 73 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 ) ) ) )
75 cnveq 
 |-  ( f = ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) -> `' f = `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) )
76 75 reseq1d 
 |-  ( f = ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) -> ( `' f |` A ) = ( `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) )
77 76 funeqd 
 |-  ( f = ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) -> ( Fun ( `' f |` A ) <-> Fun ( `' ( g u. ( x e. ( NN \ ( 1 ... ( # ` A ) ) ) |-> Z ) ) |` A ) ) )
78 72 74 77 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 ) ) ) )
79 71 78 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 ) ) )
80 25 34 64 79 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 ) ) )
81 8 80 exlimddv 
 |-  ( ( A ~< _om /\ Z e. V /\ -. Z e. A ) -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )
82 81 3expia 
 |-  ( ( A ~< _om /\ Z e. V ) -> ( -. Z e. A -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) )
83 nnenom 
 |-  NN ~~ _om
84 ensym 
 |-  ( A ~~ _om -> _om ~~ A )
85 84 adantr 
 |-  ( ( A ~~ _om /\ Z e. V ) -> _om ~~ A )
86 entr 
 |-  ( ( NN ~~ _om /\ _om ~~ A ) -> NN ~~ A )
87 83 85 86 sylancr 
 |-  ( ( A ~~ _om /\ Z e. V ) -> NN ~~ A )
88 bren 
 |-  ( NN ~~ A <-> E. f f : NN -1-1-onto-> A )
89 87 88 sylib 
 |-  ( ( A ~~ _om /\ Z e. V ) -> E. f f : NN -1-1-onto-> A )
90 simpr 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> f : NN -1-1-onto-> A )
91 f1of 
 |-  ( f : NN -1-1-onto-> A -> f : NN --> A )
92 ssun1 
 |-  A C_ ( A u. { Z } )
93 fss 
 |-  ( ( f : NN --> A /\ A C_ ( A u. { Z } ) ) -> f : NN --> ( A u. { Z } ) )
94 92 93 mpan2 
 |-  ( f : NN --> A -> f : NN --> ( A u. { Z } ) )
95 90 91 94 3syl 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> f : NN --> ( A u. { Z } ) )
96 f1ofo 
 |-  ( f : NN -1-1-onto-> A -> f : NN -onto-> A )
97 forn 
 |-  ( f : NN -onto-> A -> ran f = A )
98 90 96 97 3syl 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> ran f = A )
99 98 eqimsscd 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> A C_ ran f )
100 f1ocnv 
 |-  ( f : NN -1-1-onto-> A -> `' f : A -1-1-onto-> NN )
101 f1of1 
 |-  ( `' f : A -1-1-onto-> NN -> `' f : A -1-1-> NN )
102 90 100 101 3syl 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> `' f : A -1-1-> NN )
103 ssid 
 |-  A C_ A
104 f1ores 
 |-  ( ( `' f : A -1-1-> NN /\ A C_ A ) -> ( `' f |` A ) : A -1-1-onto-> ( `' f " A ) )
105 103 104 mpan2 
 |-  ( `' f : A -1-1-> NN -> ( `' f |` A ) : A -1-1-onto-> ( `' f " A ) )
106 f1ofun 
 |-  ( ( `' f |` A ) : A -1-1-onto-> ( `' f " A ) -> Fun ( `' f |` A ) )
107 102 105 106 3syl 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> Fun ( `' f |` A ) )
108 95 99 107 3jca 
 |-  ( ( ( A ~~ _om /\ Z e. V ) /\ f : NN -1-1-onto-> A ) -> ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )
109 108 ex 
 |-  ( ( A ~~ _om /\ Z e. V ) -> ( f : NN -1-1-onto-> A -> ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) )
110 109 eximdv 
 |-  ( ( 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 ) ) ) )
111 89 110 mpd 
 |-  ( ( A ~~ _om /\ Z e. V ) -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )
112 111 a1d 
 |-  ( ( A ~~ _om /\ Z e. V ) -> ( -. Z e. A -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) ) )
113 82 112 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 ) ) ) )
114 113 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 ) ) )
115 1 114 syl3an1b 
 |-  ( ( A ~<_ _om /\ Z e. V /\ -. Z e. A ) -> E. f ( f : NN --> ( A u. { Z } ) /\ A C_ ran f /\ Fun ( `' f |` A ) ) )