Metamath Proof Explorer

Theorem eliunxp2

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

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

Proof

Step Hyp Ref Expression
1 relxp 
 |-  Rel ( A X. { y } )
2 1 rgenw 
 |-  A. y e. B Rel ( A X. { y } )
3 reliun 
 |-  ( Rel U_ y e. B ( A X. { y } ) <-> A. y e. B Rel ( A X. { y } ) )
4 2 3 mpbir 
 |-  Rel U_ y e. B ( A X. { y } )
5 elrel 
 |-  ( ( Rel U_ y e. B ( A X. { y } ) /\ C e. U_ y e. B ( A X. { y } ) ) -> E. x E. y C = <. x , y >. )
6 4 5 mpan 
 |-  ( C e. U_ y e. B ( A X. { y } ) -> E. x E. y C = <. x , y >. )
7 excom 
 |-  ( E. y E. x C = <. x , y >. <-> E. x E. y C = <. x , y >. )
8 6 7 sylibr 
 |-  ( C e. U_ y e. B ( A X. { y } ) -> E. y E. x C = <. x , y >. )
9 8 pm4.71ri 
 |-  ( C e. U_ y e. B ( A X. { y } ) <-> ( E. y E. x C = <. x , y >. /\ C e. U_ y e. B ( A X. { y } ) ) )
10 nfiu1 
 |-  F/_ y U_ y e. B ( A X. { y } )
11 10 nfel2 
 |-  F/ y C e. U_ y e. B ( A X. { y } )
12 11 19.41 
 |-  ( E. y ( E. x C = <. x , y >. /\ C e. U_ y e. B ( A X. { y } ) ) <-> ( E. y E. x C = <. x , y >. /\ C e. U_ y e. B ( A X. { y } ) ) )
13 19.41v 
 |-  ( E. x ( C = <. x , y >. /\ C e. U_ y e. B ( A X. { y } ) ) <-> ( E. x C = <. x , y >. /\ C e. U_ y e. B ( A X. { y } ) ) )
14 eleq1 
 |-  ( C = <. x , y >. -> ( C e. U_ y e. B ( A X. { y } ) <-> <. x , y >. e. U_ y e. B ( A X. { y } ) ) )
15 opeliun2xp 
 |-  ( <. x , y >. e. U_ y e. B ( A X. { y } ) <-> ( y e. B /\ x e. A ) )
16 15 biancomi 
 |-  ( <. x , y >. e. U_ y e. B ( A X. { y } ) <-> ( x e. A /\ y e. B ) )
17 14 16 bitrdi 
 |-  ( C = <. x , y >. -> ( C e. U_ y e. B ( A X. { y } ) <-> ( x e. A /\ y e. B ) ) )
18 17 pm5.32i 
 |-  ( ( C = <. x , y >. /\ C e. U_ y e. B ( A X. { y } ) ) <-> ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
19 18 exbii 
 |-  ( E. x ( C = <. x , y >. /\ C e. U_ y e. B ( A X. { y } ) ) <-> E. x ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
20 13 19 bitr3i 
 |-  ( ( E. x C = <. x , y >. /\ C e. U_ y e. B ( A X. { y } ) ) <-> E. x ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
21 20 exbii 
 |-  ( E. y ( E. x C = <. x , y >. /\ C e. U_ y e. B ( A X. { y } ) ) <-> E. y E. x ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
22 9 12 21 3bitr2i 
 |-  ( C e. U_ y e. B ( A X. { y } ) <-> E. y E. x ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
23 excom 
 |-  ( E. y E. x ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) <-> E. x E. y ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
24 22 23 bitri 
 |-  ( C e. U_ y e. B ( A X. { y } ) <-> E. x E. y ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )