Metamath Proof Explorer

Theorem opeliunxp

Description: Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Mario Carneiro, 1-Jan-2017)

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

Proof

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