Metamath Proof Explorer


Theorem dfco2

Description: Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008)

Ref Expression
Assertion dfco2
|- ( A o. B ) = U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) )

Proof

Step Hyp Ref Expression
1 relco
 |-  Rel ( A o. B )
2 reliun
 |-  ( Rel U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) <-> A. x e. _V Rel ( ( `' B " { x } ) X. ( A " { x } ) ) )
3 relxp
 |-  Rel ( ( `' B " { x } ) X. ( A " { x } ) )
4 3 a1i
 |-  ( x e. _V -> Rel ( ( `' B " { x } ) X. ( A " { x } ) ) )
5 2 4 mprgbir
 |-  Rel U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) )
6 opelco2g
 |-  ( ( y e. _V /\ z e. _V ) -> ( <. y , z >. e. ( A o. B ) <-> E. x ( <. y , x >. e. B /\ <. x , z >. e. A ) ) )
7 6 el2v
 |-  ( <. y , z >. e. ( A o. B ) <-> E. x ( <. y , x >. e. B /\ <. x , z >. e. A ) )
8 eliun
 |-  ( <. y , z >. e. U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x e. _V <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) )
9 rexv
 |-  ( E. x e. _V <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) )
10 opelxp
 |-  ( <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> ( y e. ( `' B " { x } ) /\ z e. ( A " { x } ) ) )
11 vex
 |-  x e. _V
12 vex
 |-  y e. _V
13 11 12 elimasn
 |-  ( y e. ( `' B " { x } ) <-> <. x , y >. e. `' B )
14 11 12 opelcnv
 |-  ( <. x , y >. e. `' B <-> <. y , x >. e. B )
15 13 14 bitri
 |-  ( y e. ( `' B " { x } ) <-> <. y , x >. e. B )
16 vex
 |-  z e. _V
17 11 16 elimasn
 |-  ( z e. ( A " { x } ) <-> <. x , z >. e. A )
18 15 17 anbi12i
 |-  ( ( y e. ( `' B " { x } ) /\ z e. ( A " { x } ) ) <-> ( <. y , x >. e. B /\ <. x , z >. e. A ) )
19 10 18 bitri
 |-  ( <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> ( <. y , x >. e. B /\ <. x , z >. e. A ) )
20 19 exbii
 |-  ( E. x <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x ( <. y , x >. e. B /\ <. x , z >. e. A ) )
21 8 9 20 3bitrri
 |-  ( E. x ( <. y , x >. e. B /\ <. x , z >. e. A ) <-> <. y , z >. e. U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) )
22 7 21 bitri
 |-  ( <. y , z >. e. ( A o. B ) <-> <. y , z >. e. U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) )
23 1 5 22 eqrelriiv
 |-  ( A o. B ) = U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) )