Metamath Proof Explorer

Theorem ofoafo

Description: Addition operator for functions from a set into a power of omega is an onto binary operator. (Contributed by RP, 5-Jan-2025)

Ref Expression
Assertion ofoafo 
|- ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) -> ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) : ( ( C ^m A ) X. ( C ^m A ) ) -onto-> ( C ^m A ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. V -> A e. V )
2 inidm 
 |-  ( A i^i A ) = A
3 2 eqcomi 
 |-  A = ( A i^i A )
4 3 a1i 
 |-  ( A e. V -> A = ( A i^i A ) )
5 1 1 4 3jca 
 |-  ( A e. V -> ( A e. V /\ A e. V /\ A = ( A i^i A ) ) )
6 ofoaf 
 |-  ( ( ( A e. V /\ A e. V /\ A = ( A i^i A ) ) /\ ( B e. On /\ C = ( _om ^o B ) ) ) -> ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) : ( ( C ^m A ) X. ( C ^m A ) ) --> ( C ^m A ) )
7 5 6 sylan 
 |-  ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) -> ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) : ( ( C ^m A ) X. ( C ^m A ) ) --> ( C ^m A ) )
8 simpr 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ h e. ( C ^m A ) ) -> h e. ( C ^m A ) )
9 omelon 
 |-  _om e. On
10 9 a1i 
 |-  ( ( B e. On /\ C = ( _om ^o B ) ) -> _om e. On )
11 simpl 
 |-  ( ( B e. On /\ C = ( _om ^o B ) ) -> B e. On )
12 10 11 jca 
 |-  ( ( B e. On /\ C = ( _om ^o B ) ) -> ( _om e. On /\ B e. On ) )
13 peano1 
 |-  (/) e. _om
14 oen0 
 |-  ( ( ( _om e. On /\ B e. On ) /\ (/) e. _om ) -> (/) e. ( _om ^o B ) )
15 12 13 14 sylancl 
 |-  ( ( B e. On /\ C = ( _om ^o B ) ) -> (/) e. ( _om ^o B ) )
16 simpr 
 |-  ( ( B e. On /\ C = ( _om ^o B ) ) -> C = ( _om ^o B ) )
17 15 16 eleqtrrd 
 |-  ( ( B e. On /\ C = ( _om ^o B ) ) -> (/) e. C )
18 fconst6g 
 |-  ( (/) e. C -> ( A X. { (/) } ) : A --> C )
19 17 18 syl 
 |-  ( ( B e. On /\ C = ( _om ^o B ) ) -> ( A X. { (/) } ) : A --> C )
20 19 adantl 
 |-  ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) -> ( A X. { (/) } ) : A --> C )
21 oecl 
 |-  ( ( _om e. On /\ B e. On ) -> ( _om ^o B ) e. On )
22 9 11 21 sylancr 
 |-  ( ( B e. On /\ C = ( _om ^o B ) ) -> ( _om ^o B ) e. On )
23 16 22 eqeltrd 
 |-  ( ( B e. On /\ C = ( _om ^o B ) ) -> C e. On )
24 23 adantl 
 |-  ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) -> C e. On )
25 simpl 
 |-  ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) -> A e. V )
26 24 25 elmapd 
 |-  ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) -> ( ( A X. { (/) } ) e. ( C ^m A ) <-> ( A X. { (/) } ) : A --> C ) )
27 20 26 mpbird 
 |-  ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) -> ( A X. { (/) } ) e. ( C ^m A ) )
28 27 adantr 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ h e. ( C ^m A ) ) -> ( A X. { (/) } ) e. ( C ^m A ) )
29 ovres 
 |-  ( ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) -> ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) ( A X. { (/) } ) ) = ( h oF +o ( A X. { (/) } ) ) )
30 29 adantl 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) -> ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) ( A X. { (/) } ) ) = ( h oF +o ( A X. { (/) } ) ) )
31 elmapi 
 |-  ( h e. ( C ^m A ) -> h : A --> C )
32 31 adantr 
 |-  ( ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) -> h : A --> C )
33 32 ffnd 
 |-  ( ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) -> h Fn A )
34 33 adantl 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) -> h Fn A )
35 elmapi 
 |-  ( ( A X. { (/) } ) e. ( C ^m A ) -> ( A X. { (/) } ) : A --> C )
36 35 adantl 
 |-  ( ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) -> ( A X. { (/) } ) : A --> C )
37 36 ffnd 
 |-  ( ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) -> ( A X. { (/) } ) Fn A )
38 37 adantl 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) -> ( A X. { (/) } ) Fn A )
39 25 adantr 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) -> A e. V )
40 34 38 39 39 2 offn 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) -> ( h oF +o ( A X. { (/) } ) ) Fn A )
41 elmapfn 
 |-  ( h e. ( C ^m A ) -> h Fn A )
42 elmapfn 
 |-  ( ( A X. { (/) } ) e. ( C ^m A ) -> ( A X. { (/) } ) Fn A )
43 41 42 anim12i 
 |-  ( ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) -> ( h Fn A /\ ( A X. { (/) } ) Fn A ) )
44 43 adantl 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) -> ( h Fn A /\ ( A X. { (/) } ) Fn A ) )
45 39 anim1i 
 |-  ( ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) /\ a e. A ) -> ( A e. V /\ a e. A ) )
46 fnfvof 
 |-  ( ( ( h Fn A /\ ( A X. { (/) } ) Fn A ) /\ ( A e. V /\ a e. A ) ) -> ( ( h oF +o ( A X. { (/) } ) ) ` a ) = ( ( h ` a ) +o ( ( A X. { (/) } ) ` a ) ) )
47 44 45 46 syl2an2r 
 |-  ( ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) /\ a e. A ) -> ( ( h oF +o ( A X. { (/) } ) ) ` a ) = ( ( h ` a ) +o ( ( A X. { (/) } ) ` a ) ) )
48 simpr 
 |-  ( ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) /\ a e. A ) -> a e. A )
49 fvconst2g 
 |-  ( ( (/) e. _om /\ a e. A ) -> ( ( A X. { (/) } ) ` a ) = (/) )
50 13 48 49 sylancr 
 |-  ( ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) /\ a e. A ) -> ( ( A X. { (/) } ) ` a ) = (/) )
51 50 oveq2d 
 |-  ( ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) /\ a e. A ) -> ( ( h ` a ) +o ( ( A X. { (/) } ) ` a ) ) = ( ( h ` a ) +o (/) ) )
52 24 adantr 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) -> C e. On )
53 52 adantr 
 |-  ( ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) /\ a e. A ) -> C e. On )
54 onss 
 |-  ( C e. On -> C C_ On )
55 53 54 syl 
 |-  ( ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) /\ a e. A ) -> C C_ On )
56 31 ad2antrl 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) -> h : A --> C )
57 56 ffvelcdmda 
 |-  ( ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) /\ a e. A ) -> ( h ` a ) e. C )
58 55 57 sseldd 
 |-  ( ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) /\ a e. A ) -> ( h ` a ) e. On )
59 oa0 
 |-  ( ( h ` a ) e. On -> ( ( h ` a ) +o (/) ) = ( h ` a ) )
60 58 59 syl 
 |-  ( ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) /\ a e. A ) -> ( ( h ` a ) +o (/) ) = ( h ` a ) )
61 47 51 60 3eqtrd 
 |-  ( ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) /\ a e. A ) -> ( ( h oF +o ( A X. { (/) } ) ) ` a ) = ( h ` a ) )
62 40 34 61 eqfnfvd 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) -> ( h oF +o ( A X. { (/) } ) ) = h )
63 30 62 eqtr2d 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( h e. ( C ^m A ) /\ ( A X. { (/) } ) e. ( C ^m A ) ) ) -> h = ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) ( A X. { (/) } ) ) )
64 63 expr 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ h e. ( C ^m A ) ) -> ( ( A X. { (/) } ) e. ( C ^m A ) -> h = ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) ( A X. { (/) } ) ) ) )
65 28 64 jcai 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ h e. ( C ^m A ) ) -> ( ( A X. { (/) } ) e. ( C ^m A ) /\ h = ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) ( A X. { (/) } ) ) ) )
66 oveq2 
 |-  ( z = ( A X. { (/) } ) -> ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) = ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) ( A X. { (/) } ) ) )
67 66 rspceeqv 
 |-  ( ( ( A X. { (/) } ) e. ( C ^m A ) /\ h = ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) ( A X. { (/) } ) ) ) -> E. z e. ( C ^m A ) h = ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) )
68 65 67 syl 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ h e. ( C ^m A ) ) -> E. z e. ( C ^m A ) h = ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) )
69 8 68 jca 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ h e. ( C ^m A ) ) -> ( h e. ( C ^m A ) /\ E. z e. ( C ^m A ) h = ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) ) )
70 oveq1 
 |-  ( f = h -> ( f ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) = ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) )
71 70 eqeq2d 
 |-  ( f = h -> ( h = ( f ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) <-> h = ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) ) )
72 71 rexbidv 
 |-  ( f = h -> ( E. z e. ( C ^m A ) h = ( f ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) <-> E. z e. ( C ^m A ) h = ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) ) )
73 72 rspcev 
 |-  ( ( h e. ( C ^m A ) /\ E. z e. ( C ^m A ) h = ( h ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) ) -> E. f e. ( C ^m A ) E. z e. ( C ^m A ) h = ( f ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) )
74 69 73 syl 
 |-  ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ h e. ( C ^m A ) ) -> E. f e. ( C ^m A ) E. z e. ( C ^m A ) h = ( f ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) )
75 74 ralrimiva 
 |-  ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) -> A. h e. ( C ^m A ) E. f e. ( C ^m A ) E. z e. ( C ^m A ) h = ( f ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) )
76 foov 
 |-  ( ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) : ( ( C ^m A ) X. ( C ^m A ) ) -onto-> ( C ^m A ) <-> ( ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) : ( ( C ^m A ) X. ( C ^m A ) ) --> ( C ^m A ) /\ A. h e. ( C ^m A ) E. f e. ( C ^m A ) E. z e. ( C ^m A ) h = ( f ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) z ) ) )
77 7 75 76 sylanbrc 
 |-  ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) -> ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) : ( ( C ^m A ) X. ( C ^m A ) ) -onto-> ( C ^m A ) )