Metamath Proof Explorer

Theorem ofoaid2

Description: Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025)

Ref Expression
Assertion ofoaid2 
|- ( ( ( A e. V /\ B e. On ) /\ F e. ( B ^m A ) ) -> ( ( A X. { (/) } ) oF +o F ) = F )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. V /\ B e. On ) /\ F e. ( B ^m A ) ) -> A e. V )
2 onss 
 |-  ( B e. On -> B C_ On )
3 sstr 
 |-  ( ( ran F C_ B /\ B C_ On ) -> ran F C_ On )
4 3 expcom 
 |-  ( B C_ On -> ( ran F C_ B -> ran F C_ On ) )
5 2 4 syl 
 |-  ( B e. On -> ( ran F C_ B -> ran F C_ On ) )
6 5 anim2d 
 |-  ( B e. On -> ( ( F Fn A /\ ran F C_ B ) -> ( F Fn A /\ ran F C_ On ) ) )
7 df-f 
 |-  ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
8 df-f 
 |-  ( F : A --> On <-> ( F Fn A /\ ran F C_ On ) )
9 6 7 8 3imtr4g 
 |-  ( B e. On -> ( F : A --> B -> F : A --> On ) )
10 elmapi 
 |-  ( F e. ( B ^m A ) -> F : A --> B )
11 9 10 impel 
 |-  ( ( B e. On /\ F e. ( B ^m A ) ) -> F : A --> On )
12 11 adantll 
 |-  ( ( ( A e. V /\ B e. On ) /\ F e. ( B ^m A ) ) -> F : A --> On )
13 peano1 
 |-  (/) e. _om
14 fnconstg 
 |-  ( (/) e. _om -> ( A X. { (/) } ) Fn A )
15 13 14 mp1i 
 |-  ( ( ( A e. V /\ B e. On ) /\ F e. ( B ^m A ) ) -> ( A X. { (/) } ) Fn A )
16 simp3 
 |-  ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) -> ( A X. { (/) } ) Fn A )
17 simp2 
 |-  ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) -> F : A --> On )
18 17 ffnd 
 |-  ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) -> F Fn A )
19 simp1 
 |-  ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) -> A e. V )
20 inidm 
 |-  ( A i^i A ) = A
21 16 18 19 19 20 offn 
 |-  ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) -> ( ( A X. { (/) } ) oF +o F ) Fn A )
22 16 18 jca 
 |-  ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) -> ( ( A X. { (/) } ) Fn A /\ F Fn A ) )
23 22 adantr 
 |-  ( ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) /\ a e. A ) -> ( ( A X. { (/) } ) Fn A /\ F Fn A ) )
24 19 adantr 
 |-  ( ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) /\ a e. A ) -> A e. V )
25 simpr 
 |-  ( ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) /\ a e. A ) -> a e. A )
26 fnfvof 
 |-  ( ( ( ( A X. { (/) } ) Fn A /\ F Fn A ) /\ ( A e. V /\ a e. A ) ) -> ( ( ( A X. { (/) } ) oF +o F ) ` a ) = ( ( ( A X. { (/) } ) ` a ) +o ( F ` a ) ) )
27 23 24 25 26 syl12anc 
 |-  ( ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) /\ a e. A ) -> ( ( ( A X. { (/) } ) oF +o F ) ` a ) = ( ( ( A X. { (/) } ) ` a ) +o ( F ` a ) ) )
28 fvconst2g 
 |-  ( ( (/) e. _om /\ a e. A ) -> ( ( A X. { (/) } ) ` a ) = (/) )
29 13 25 28 sylancr 
 |-  ( ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) /\ a e. A ) -> ( ( A X. { (/) } ) ` a ) = (/) )
30 29 oveq1d 
 |-  ( ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) /\ a e. A ) -> ( ( ( A X. { (/) } ) ` a ) +o ( F ` a ) ) = ( (/) +o ( F ` a ) ) )
31 17 ffvelcdmda 
 |-  ( ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) /\ a e. A ) -> ( F ` a ) e. On )
32 oa0r 
 |-  ( ( F ` a ) e. On -> ( (/) +o ( F ` a ) ) = ( F ` a ) )
33 31 32 syl 
 |-  ( ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) /\ a e. A ) -> ( (/) +o ( F ` a ) ) = ( F ` a ) )
34 27 30 33 3eqtrd 
 |-  ( ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) /\ a e. A ) -> ( ( ( A X. { (/) } ) oF +o F ) ` a ) = ( F ` a ) )
35 21 18 34 eqfnfvd 
 |-  ( ( A e. V /\ F : A --> On /\ ( A X. { (/) } ) Fn A ) -> ( ( A X. { (/) } ) oF +o F ) = F )
36 1 12 15 35 syl3anc 
 |-  ( ( ( A e. V /\ B e. On ) /\ F e. ( B ^m A ) ) -> ( ( A X. { (/) } ) oF +o F ) = F )