Metamath Proof Explorer

Theorem onovuni

Description: A variant of onfununi for operations. (Contributed by Eric Schmidt, 26-May-2009) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses onovuni.1 
|- ( Lim y -> ( A F y ) = U_ x e. y ( A F x ) )
onovuni.2 
|- ( ( x e. On /\ y e. On /\ x C_ y ) -> ( A F x ) C_ ( A F y ) )
Assertion onovuni 
|- ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( A F U. S ) = U_ x e. S ( A F x ) )

Proof

Step Hyp Ref Expression
1 onovuni.1 
 |-  ( Lim y -> ( A F y ) = U_ x e. y ( A F x ) )
2 onovuni.2 
 |-  ( ( x e. On /\ y e. On /\ x C_ y ) -> ( A F x ) C_ ( A F y ) )
3 oveq2 
 |-  ( z = y -> ( A F z ) = ( A F y ) )
4 eqid 
 |-  ( z e. _V |-> ( A F z ) ) = ( z e. _V |-> ( A F z ) )
5 ovex 
 |-  ( A F y ) e. _V
6 3 4 5 fvmpt 
 |-  ( y e. _V -> ( ( z e. _V |-> ( A F z ) ) ` y ) = ( A F y ) )
7 6 elv 
 |-  ( ( z e. _V |-> ( A F z ) ) ` y ) = ( A F y )
8 oveq2 
 |-  ( z = x -> ( A F z ) = ( A F x ) )
9 ovex 
 |-  ( A F x ) e. _V
10 8 4 9 fvmpt 
 |-  ( x e. _V -> ( ( z e. _V |-> ( A F z ) ) ` x ) = ( A F x ) )
11 10 elv 
 |-  ( ( z e. _V |-> ( A F z ) ) ` x ) = ( A F x )
12 11 a1i 
 |-  ( x e. y -> ( ( z e. _V |-> ( A F z ) ) ` x ) = ( A F x ) )
13 12 iuneq2i 
 |-  U_ x e. y ( ( z e. _V |-> ( A F z ) ) ` x ) = U_ x e. y ( A F x )
14 1 7 13 3eqtr4g 
 |-  ( Lim y -> ( ( z e. _V |-> ( A F z ) ) ` y ) = U_ x e. y ( ( z e. _V |-> ( A F z ) ) ` x ) )
15 2 11 7 3sstr4g 
 |-  ( ( x e. On /\ y e. On /\ x C_ y ) -> ( ( z e. _V |-> ( A F z ) ) ` x ) C_ ( ( z e. _V |-> ( A F z ) ) ` y ) )
16 14 15 onfununi 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( ( z e. _V |-> ( A F z ) ) ` U. S ) = U_ x e. S ( ( z e. _V |-> ( A F z ) ) ` x ) )
17 uniexg 
 |-  ( S e. T -> U. S e. _V )
18 oveq2 
 |-  ( z = U. S -> ( A F z ) = ( A F U. S ) )
19 ovex 
 |-  ( A F U. S ) e. _V
20 18 4 19 fvmpt 
 |-  ( U. S e. _V -> ( ( z e. _V |-> ( A F z ) ) ` U. S ) = ( A F U. S ) )
21 17 20 syl 
 |-  ( S e. T -> ( ( z e. _V |-> ( A F z ) ) ` U. S ) = ( A F U. S ) )
22 21 3ad2ant1 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( ( z e. _V |-> ( A F z ) ) ` U. S ) = ( A F U. S ) )
23 11 a1i 
 |-  ( x e. S -> ( ( z e. _V |-> ( A F z ) ) ` x ) = ( A F x ) )
24 23 iuneq2i 
 |-  U_ x e. S ( ( z e. _V |-> ( A F z ) ) ` x ) = U_ x e. S ( A F x )
25 24 a1i 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> U_ x e. S ( ( z e. _V |-> ( A F z ) ) ` x ) = U_ x e. S ( A F x ) )
26 16 22 25 3eqtr3d 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( A F U. S ) = U_ x e. S ( A F x ) )