Metamath Proof Explorer

Theorem opeliun2xp

Description: Membership of an ordered pair in a union of Cartesian products over its second component, analogous to opeliunxp . (Contributed by AV, 30-Mar-2019)

Ref Expression
Assertion opeliun2xp 
|- ( <. C , y >. e. U_ y e. B ( A X. { y } ) <-> ( y e. B /\ C e. A ) )

Proof

Step Hyp Ref Expression
1 df-iun 
 |-  U_ y e. B ( A X. { y } ) = { x | E. y e. B x e. ( A X. { y } ) }
2 1 eleq2i 
 |-  ( <. C , y >. e. U_ y e. B ( A X. { y } ) <-> <. C , y >. e. { x | E. y e. B x e. ( A X. { y } ) } )
3 opex 
 |-  <. C , y >. e. _V
4 df-rex 
 |-  ( E. y e. B x e. ( A X. { y } ) <-> E. y ( y e. B /\ x e. ( A X. { y } ) ) )
5 nfv 
 |-  F/ z ( y e. B /\ x e. ( A X. { y } ) )
6 nfs1v 
 |-  F/ y [ z / y ] y e. B
7 nfcsb1v 
 |-  F/_ y [_ z / y ]_ A
8 nfcv 
 |-  F/_ y { z }
9 7 8 nfxp 
 |-  F/_ y ( [_ z / y ]_ A X. { z } )
10 9 nfcri 
 |-  F/ y x e. ( [_ z / y ]_ A X. { z } )
11 6 10 nfan 
 |-  F/ y ( [ z / y ] y e. B /\ x e. ( [_ z / y ]_ A X. { z } ) )
12 sbequ12 
 |-  ( y = z -> ( y e. B <-> [ z / y ] y e. B ) )
13 csbeq1a 
 |-  ( y = z -> A = [_ z / y ]_ A )
14 sneq 
 |-  ( y = z -> { y } = { z } )
15 13 14 xpeq12d 
 |-  ( y = z -> ( A X. { y } ) = ( [_ z / y ]_ A X. { z } ) )
16 15 eleq2d 
 |-  ( y = z -> ( x e. ( A X. { y } ) <-> x e. ( [_ z / y ]_ A X. { z } ) ) )
17 12 16 anbi12d 
 |-  ( y = z -> ( ( y e. B /\ x e. ( A X. { y } ) ) <-> ( [ z / y ] y e. B /\ x e. ( [_ z / y ]_ A X. { z } ) ) ) )
18 5 11 17 cbvexv1 
 |-  ( E. y ( y e. B /\ x e. ( A X. { y } ) ) <-> E. z ( [ z / y ] y e. B /\ x e. ( [_ z / y ]_ A X. { z } ) ) )
19 4 18 bitri 
 |-  ( E. y e. B x e. ( A X. { y } ) <-> E. z ( [ z / y ] y e. B /\ x e. ( [_ z / y ]_ A X. { z } ) ) )
20 eleq1 
 |-  ( x = <. C , y >. -> ( x e. ( [_ z / y ]_ A X. { z } ) <-> <. C , y >. e. ( [_ z / y ]_ A X. { z } ) ) )
21 20 anbi2d 
 |-  ( x = <. C , y >. -> ( ( [ z / y ] y e. B /\ x e. ( [_ z / y ]_ A X. { z } ) ) <-> ( [ z / y ] y e. B /\ <. C , y >. e. ( [_ z / y ]_ A X. { z } ) ) ) )
22 21 exbidv 
 |-  ( x = <. C , y >. -> ( E. z ( [ z / y ] y e. B /\ x e. ( [_ z / y ]_ A X. { z } ) ) <-> E. z ( [ z / y ] y e. B /\ <. C , y >. e. ( [_ z / y ]_ A X. { z } ) ) ) )
23 19 22 bitrid 
 |-  ( x = <. C , y >. -> ( E. y e. B x e. ( A X. { y } ) <-> E. z ( [ z / y ] y e. B /\ <. C , y >. e. ( [_ z / y ]_ A X. { z } ) ) ) )
24 3 23 elab 
 |-  ( <. C , y >. e. { x | E. y e. B x e. ( A X. { y } ) } <-> E. z ( [ z / y ] y e. B /\ <. C , y >. e. ( [_ z / y ]_ A X. { z } ) ) )
25 opelxp 
 |-  ( <. C , y >. e. ( [_ z / y ]_ A X. { z } ) <-> ( C e. [_ z / y ]_ A /\ y e. { z } ) )
26 25 anbi2i 
 |-  ( ( [ z / y ] y e. B /\ <. C , y >. e. ( [_ z / y ]_ A X. { z } ) ) <-> ( [ z / y ] y e. B /\ ( C e. [_ z / y ]_ A /\ y e. { z } ) ) )
27 an13 
 |-  ( ( [ z / y ] y e. B /\ ( C e. [_ z / y ]_ A /\ y e. { z } ) ) <-> ( y e. { z } /\ ( C e. [_ z / y ]_ A /\ [ z / y ] y e. B ) ) )
28 ancom 
 |-  ( ( C e. [_ z / y ]_ A /\ [ z / y ] y e. B ) <-> ( [ z / y ] y e. B /\ C e. [_ z / y ]_ A ) )
29 28 anbi2i 
 |-  ( ( y e. { z } /\ ( C e. [_ z / y ]_ A /\ [ z / y ] y e. B ) ) <-> ( y e. { z } /\ ( [ z / y ] y e. B /\ C e. [_ z / y ]_ A ) ) )
30 27 29 bitri 
 |-  ( ( [ z / y ] y e. B /\ ( C e. [_ z / y ]_ A /\ y e. { z } ) ) <-> ( y e. { z } /\ ( [ z / y ] y e. B /\ C e. [_ z / y ]_ A ) ) )
31 velsn 
 |-  ( y e. { z } <-> y = z )
32 equcom 
 |-  ( y = z <-> z = y )
33 31 32 bitri 
 |-  ( y e. { z } <-> z = y )
34 33 anbi1i 
 |-  ( ( y e. { z } /\ ( [ z / y ] y e. B /\ C e. [_ z / y ]_ A ) ) <-> ( z = y /\ ( [ z / y ] y e. B /\ C e. [_ z / y ]_ A ) ) )
35 26 30 34 3bitri 
 |-  ( ( [ z / y ] y e. B /\ <. C , y >. e. ( [_ z / y ]_ A X. { z } ) ) <-> ( z = y /\ ( [ z / y ] y e. B /\ C e. [_ z / y ]_ A ) ) )
36 35 exbii 
 |-  ( E. z ( [ z / y ] y e. B /\ <. C , y >. e. ( [_ z / y ]_ A X. { z } ) ) <-> E. z ( z = y /\ ( [ z / y ] y e. B /\ C e. [_ z / y ]_ A ) ) )
37 sbequ12r 
 |-  ( z = y -> ( [ z / y ] y e. B <-> y e. B ) )
38 13 equcoms 
 |-  ( z = y -> A = [_ z / y ]_ A )
39 38 eqcomd 
 |-  ( z = y -> [_ z / y ]_ A = A )
40 39 eleq2d 
 |-  ( z = y -> ( C e. [_ z / y ]_ A <-> C e. A ) )
41 37 40 anbi12d 
 |-  ( z = y -> ( ( [ z / y ] y e. B /\ C e. [_ z / y ]_ A ) <-> ( y e. B /\ C e. A ) ) )
42 41 equsexvw 
 |-  ( E. z ( z = y /\ ( [ z / y ] y e. B /\ C e. [_ z / y ]_ A ) ) <-> ( y e. B /\ C e. A ) )
43 36 42 bitri 
 |-  ( E. z ( [ z / y ] y e. B /\ <. C , y >. e. ( [_ z / y ]_ A X. { z } ) ) <-> ( y e. B /\ C e. A ) )
44 2 24 43 3bitri 
 |-  ( <. C , y >. e. U_ y e. B ( A X. { y } ) <-> ( y e. B /\ C e. A ) )