Metamath Proof Explorer

Theorem dfco2a

Description: Generalization of dfco2 , where C can have any value between dom A i^i ran B and _V . (Contributed by NM, 21-Dec-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion dfco2a 
|- ( ( dom A i^i ran B ) C_ C -> ( A o. B ) = U_ x e. C ( ( `' B " { x } ) X. ( A " { x } ) ) )

Proof

Step Hyp Ref Expression
1 dfco2 
 |-  ( A o. B ) = U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) )
2 vex 
 |-  z e. _V
3 2 eliniseg 
 |-  ( x e. _V -> ( z e. ( `' B " { x } ) <-> z B x ) )
4 3 elv 
 |-  ( z e. ( `' B " { x } ) <-> z B x )
5 vex 
 |-  x e. _V
6 2 5 brelrn 
 |-  ( z B x -> x e. ran B )
7 4 6 sylbi 
 |-  ( z e. ( `' B " { x } ) -> x e. ran B )
8 vex 
 |-  w e. _V
9 5 8 elimasn 
 |-  ( w e. ( A " { x } ) <-> <. x , w >. e. A )
10 5 8 opeldm 
 |-  ( <. x , w >. e. A -> x e. dom A )
11 9 10 sylbi 
 |-  ( w e. ( A " { x } ) -> x e. dom A )
12 7 11 anim12ci 
 |-  ( ( z e. ( `' B " { x } ) /\ w e. ( A " { x } ) ) -> ( x e. dom A /\ x e. ran B ) )
13 12 adantl 
 |-  ( ( y = <. z , w >. /\ ( z e. ( `' B " { x } ) /\ w e. ( A " { x } ) ) ) -> ( x e. dom A /\ x e. ran B ) )
14 13 exlimivv 
 |-  ( E. z E. w ( y = <. z , w >. /\ ( z e. ( `' B " { x } ) /\ w e. ( A " { x } ) ) ) -> ( x e. dom A /\ x e. ran B ) )
15 elxp 
 |-  ( y e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. z E. w ( y = <. z , w >. /\ ( z e. ( `' B " { x } ) /\ w e. ( A " { x } ) ) ) )
16 elin 
 |-  ( x e. ( dom A i^i ran B ) <-> ( x e. dom A /\ x e. ran B ) )
17 14 15 16 3imtr4i 
 |-  ( y e. ( ( `' B " { x } ) X. ( A " { x } ) ) -> x e. ( dom A i^i ran B ) )
18 ssel 
 |-  ( ( dom A i^i ran B ) C_ C -> ( x e. ( dom A i^i ran B ) -> x e. C ) )
19 17 18 syl5 
 |-  ( ( dom A i^i ran B ) C_ C -> ( y e. ( ( `' B " { x } ) X. ( A " { x } ) ) -> x e. C ) )
20 19 pm4.71rd 
 |-  ( ( dom A i^i ran B ) C_ C -> ( y e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> ( x e. C /\ y e. ( ( `' B " { x } ) X. ( A " { x } ) ) ) ) )
21 20 exbidv 
 |-  ( ( dom A i^i ran B ) C_ C -> ( E. x y e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x ( x e. C /\ y e. ( ( `' B " { x } ) X. ( A " { x } ) ) ) ) )
22 rexv 
 |-  ( E. x e. _V y e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x y e. ( ( `' B " { x } ) X. ( A " { x } ) ) )
23 df-rex 
 |-  ( E. x e. C y e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x ( x e. C /\ y e. ( ( `' B " { x } ) X. ( A " { x } ) ) ) )
24 21 22 23 3bitr4g 
 |-  ( ( dom A i^i ran B ) C_ C -> ( E. x e. _V y e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x e. C y e. ( ( `' B " { x } ) X. ( A " { x } ) ) ) )
25 eliun 
 |-  ( y e. U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x e. _V y e. ( ( `' B " { x } ) X. ( A " { x } ) ) )
26 eliun 
 |-  ( y e. U_ x e. C ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x e. C y e. ( ( `' B " { x } ) X. ( A " { x } ) ) )
27 24 25 26 3bitr4g 
 |-  ( ( dom A i^i ran B ) C_ C -> ( y e. U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) <-> y e. U_ x e. C ( ( `' B " { x } ) X. ( A " { x } ) ) ) )
28 27 eqrdv 
 |-  ( ( dom A i^i ran B ) C_ C -> U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) = U_ x e. C ( ( `' B " { x } ) X. ( A " { x } ) ) )
29 1 28 eqtrid 
 |-  ( ( dom A i^i ran B ) C_ C -> ( A o. B ) = U_ x e. C ( ( `' B " { x } ) X. ( A " { x } ) ) )