Metamath Proof Explorer

Theorem ofoaf

Description: Addition operator for functions from sets into power of omega results in a function from the intersection of sets to that power of omega. (Contributed by RP, 5-Jan-2025)

Ref Expression
Assertion ofoaf 
|- ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E = ( _om ^o D ) ) ) -> ( oF +o |` ( ( E ^m A ) X. ( E ^m B ) ) ) : ( ( E ^m A ) X. ( E ^m B ) ) --> ( E ^m C ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> E = ( _om ^o D ) )
2 omelon 
 |-  _om e. On
3 simpl 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> D e. On )
4 oecl 
 |-  ( ( _om e. On /\ D e. On ) -> ( _om ^o D ) e. On )
5 2 3 4 sylancr 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> ( _om ^o D ) e. On )
6 1 5 eqeltrd 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> E e. On )
7 3 2 jctil 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> ( _om e. On /\ D e. On ) )
8 peano1 
 |-  (/) e. _om
9 oen0 
 |-  ( ( ( _om e. On /\ D e. On ) /\ (/) e. _om ) -> (/) e. ( _om ^o D ) )
10 7 8 9 sylancl 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> (/) e. ( _om ^o D ) )
11 10 1 eleqtrrd 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> (/) e. E )
12 oveq1 
 |-  ( x = (/) -> ( x +o E ) = ( (/) +o E ) )
13 12 sseq2d 
 |-  ( x = (/) -> ( E C_ ( x +o E ) <-> E C_ ( (/) +o E ) ) )
14 13 adantl 
 |-  ( ( ( D e. On /\ E = ( _om ^o D ) ) /\ x = (/) ) -> ( E C_ ( x +o E ) <-> E C_ ( (/) +o E ) ) )
15 oa0r 
 |-  ( E e. On -> ( (/) +o E ) = E )
16 6 15 syl 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> ( (/) +o E ) = E )
17 ssid 
 |-  ( (/) +o E ) C_ ( (/) +o E )
18 16 17 eqsstrrdi 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> E C_ ( (/) +o E ) )
19 11 14 18 rspcedvd 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> E. x e. E E C_ ( x +o E ) )
20 ssiun 
 |-  ( E. x e. E E C_ ( x +o E ) -> E C_ U_ x e. E ( x +o E ) )
21 19 20 syl 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> E C_ U_ x e. E ( x +o E ) )
22 1 eleq2d 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> ( x e. E <-> x e. ( _om ^o D ) ) )
23 22 biimpa 
 |-  ( ( ( D e. On /\ E = ( _om ^o D ) ) /\ x e. E ) -> x e. ( _om ^o D ) )
24 6 adantr 
 |-  ( ( ( D e. On /\ E = ( _om ^o D ) ) /\ x e. E ) -> E e. On )
25 1 adantr 
 |-  ( ( ( D e. On /\ E = ( _om ^o D ) ) /\ x e. E ) -> E = ( _om ^o D ) )
26 ssid 
 |-  E C_ E
27 25 26 eqsstrrdi 
 |-  ( ( ( D e. On /\ E = ( _om ^o D ) ) /\ x e. E ) -> ( _om ^o D ) C_ E )
28 oaabs2 
 |-  ( ( ( x e. ( _om ^o D ) /\ E e. On ) /\ ( _om ^o D ) C_ E ) -> ( x +o E ) = E )
29 23 24 27 28 syl21anc 
 |-  ( ( ( D e. On /\ E = ( _om ^o D ) ) /\ x e. E ) -> ( x +o E ) = E )
30 29 26 eqsstrdi 
 |-  ( ( ( D e. On /\ E = ( _om ^o D ) ) /\ x e. E ) -> ( x +o E ) C_ E )
31 30 iunssd 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> U_ x e. E ( x +o E ) C_ E )
32 21 31 eqssd 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> E = U_ x e. E ( x +o E ) )
33 6 6 32 3jca 
 |-  ( ( D e. On /\ E = ( _om ^o D ) ) -> ( E e. On /\ E e. On /\ E = U_ x e. E ( x +o E ) ) )
34 ofoafg 
 |-  ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( E e. On /\ E e. On /\ E = U_ x e. E ( x +o E ) ) ) -> ( oF +o |` ( ( E ^m A ) X. ( E ^m B ) ) ) : ( ( E ^m A ) X. ( E ^m B ) ) --> ( E ^m C ) )
35 33 34 sylan2 
 |-  ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E = ( _om ^o D ) ) ) -> ( oF +o |` ( ( E ^m A ) X. ( E ^m B ) ) ) : ( ( E ^m A ) X. ( E ^m B ) ) --> ( E ^m C ) )