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 syl5bb
 |-  ( 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 ) )