Metamath Proof Explorer

Theorem onoviun

Description: A variant of onovuni with indexed unions. (Contributed by Eric Schmidt, 26-May-2009) (Proof shortened by Mario Carneiro, 5-Dec-2016)

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 onoviun 
|- ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> ( A F U_ z e. K L ) = U_ z e. K ( A F L ) )

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 dfiun3g 
 |-  ( A. z e. K L e. On -> U_ z e. K L = U. ran ( z e. K |-> L ) )
4 3 3ad2ant2 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> U_ z e. K L = U. ran ( z e. K |-> L ) )
5 4 oveq2d 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> ( A F U_ z e. K L ) = ( A F U. ran ( z e. K |-> L ) ) )
6 simp1 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> K e. T )
7 mptexg 
 |-  ( K e. T -> ( z e. K |-> L ) e. _V )
8 rnexg 
 |-  ( ( z e. K |-> L ) e. _V -> ran ( z e. K |-> L ) e. _V )
9 6 7 8 3syl 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> ran ( z e. K |-> L ) e. _V )
10 simp2 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> A. z e. K L e. On )
11 eqid 
 |-  ( z e. K |-> L ) = ( z e. K |-> L )
12 11 fmpt 
 |-  ( A. z e. K L e. On <-> ( z e. K |-> L ) : K --> On )
13 10 12 sylib 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> ( z e. K |-> L ) : K --> On )
14 13 frnd 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> ran ( z e. K |-> L ) C_ On )
15 dmmptg 
 |-  ( A. z e. K L e. On -> dom ( z e. K |-> L ) = K )
16 15 3ad2ant2 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> dom ( z e. K |-> L ) = K )
17 simp3 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> K =/= (/) )
18 16 17 eqnetrd 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> dom ( z e. K |-> L ) =/= (/) )
19 dm0rn0 
 |-  ( dom ( z e. K |-> L ) = (/) <-> ran ( z e. K |-> L ) = (/) )
20 19 necon3bii 
 |-  ( dom ( z e. K |-> L ) =/= (/) <-> ran ( z e. K |-> L ) =/= (/) )
21 18 20 sylib 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> ran ( z e. K |-> L ) =/= (/) )
22 1 2 onovuni 
 |-  ( ( ran ( z e. K |-> L ) e. _V /\ ran ( z e. K |-> L ) C_ On /\ ran ( z e. K |-> L ) =/= (/) ) -> ( A F U. ran ( z e. K |-> L ) ) = U_ x e. ran ( z e. K |-> L ) ( A F x ) )
23 9 14 21 22 syl3anc 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> ( A F U. ran ( z e. K |-> L ) ) = U_ x e. ran ( z e. K |-> L ) ( A F x ) )
24 oveq2 
 |-  ( x = L -> ( A F x ) = ( A F L ) )
25 24 eleq2d 
 |-  ( x = L -> ( w e. ( A F x ) <-> w e. ( A F L ) ) )
26 11 25 rexrnmptw 
 |-  ( A. z e. K L e. On -> ( E. x e. ran ( z e. K |-> L ) w e. ( A F x ) <-> E. z e. K w e. ( A F L ) ) )
27 26 3ad2ant2 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> ( E. x e. ran ( z e. K |-> L ) w e. ( A F x ) <-> E. z e. K w e. ( A F L ) ) )
28 eliun 
 |-  ( w e. U_ x e. ran ( z e. K |-> L ) ( A F x ) <-> E. x e. ran ( z e. K |-> L ) w e. ( A F x ) )
29 eliun 
 |-  ( w e. U_ z e. K ( A F L ) <-> E. z e. K w e. ( A F L ) )
30 27 28 29 3bitr4g 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> ( w e. U_ x e. ran ( z e. K |-> L ) ( A F x ) <-> w e. U_ z e. K ( A F L ) ) )
31 30 eqrdv 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> U_ x e. ran ( z e. K |-> L ) ( A F x ) = U_ z e. K ( A F L ) )
32 5 23 31 3eqtrd 
 |-  ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> ( A F U_ z e. K L ) = U_ z e. K ( A F L ) )