Metamath Proof Explorer

Theorem unielxp

Description: The membership relation for a Cartesian product is inherited by union. (Contributed by NM, 16-Sep-2006)

Ref Expression
Assertion unielxp 
|- ( A e. ( B X. C ) -> U. A e. U. ( B X. C ) )

Proof

Step Hyp Ref Expression
1 elxp7 
 |-  ( A e. ( B X. C ) <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )
2 elvvuni 
 |-  ( A e. ( _V X. _V ) -> U. A e. A )
3 2 adantr 
 |-  ( ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) -> U. A e. A )
4 simprl 
 |-  ( ( U. A e. A /\ ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) ) -> A e. ( _V X. _V ) )
5 eleq2 
 |-  ( x = A -> ( U. A e. x <-> U. A e. A ) )
6 eleq1 
 |-  ( x = A -> ( x e. ( _V X. _V ) <-> A e. ( _V X. _V ) ) )
7 fveq2 
 |-  ( x = A -> ( 1st ` x ) = ( 1st ` A ) )
8 7 eleq1d 
 |-  ( x = A -> ( ( 1st ` x ) e. B <-> ( 1st ` A ) e. B ) )
9 fveq2 
 |-  ( x = A -> ( 2nd ` x ) = ( 2nd ` A ) )
10 9 eleq1d 
 |-  ( x = A -> ( ( 2nd ` x ) e. C <-> ( 2nd ` A ) e. C ) )
11 8 10 anbi12d 
 |-  ( x = A -> ( ( ( 1st ` x ) e. B /\ ( 2nd ` x ) e. C ) <-> ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )
12 6 11 anbi12d 
 |-  ( x = A -> ( ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. B /\ ( 2nd ` x ) e. C ) ) <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) ) )
13 5 12 anbi12d 
 |-  ( x = A -> ( ( U. A e. x /\ ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. B /\ ( 2nd ` x ) e. C ) ) ) <-> ( U. A e. A /\ ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) ) ) )
14 13 spcegv 
 |-  ( A e. ( _V X. _V ) -> ( ( U. A e. A /\ ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) ) -> E. x ( U. A e. x /\ ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. B /\ ( 2nd ` x ) e. C ) ) ) ) )
15 4 14 mpcom 
 |-  ( ( U. A e. A /\ ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) ) -> E. x ( U. A e. x /\ ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. B /\ ( 2nd ` x ) e. C ) ) ) )
16 eluniab 
 |-  ( U. A e. U. { x | ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. B /\ ( 2nd ` x ) e. C ) ) } <-> E. x ( U. A e. x /\ ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. B /\ ( 2nd ` x ) e. C ) ) ) )
17 15 16 sylibr 
 |-  ( ( U. A e. A /\ ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) ) -> U. A e. U. { x | ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. B /\ ( 2nd ` x ) e. C ) ) } )
18 xp2 
 |-  ( B X. C ) = { x e. ( _V X. _V ) | ( ( 1st ` x ) e. B /\ ( 2nd ` x ) e. C ) }
19 df-rab 
 |-  { x e. ( _V X. _V ) | ( ( 1st ` x ) e. B /\ ( 2nd ` x ) e. C ) } = { x | ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. B /\ ( 2nd ` x ) e. C ) ) }
20 18 19 eqtri 
 |-  ( B X. C ) = { x | ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. B /\ ( 2nd ` x ) e. C ) ) }
21 20 unieqi 
 |-  U. ( B X. C ) = U. { x | ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. B /\ ( 2nd ` x ) e. C ) ) }
22 17 21 eleqtrrdi 
 |-  ( ( U. A e. A /\ ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) ) -> U. A e. U. ( B X. C ) )
23 3 22 mpancom 
 |-  ( ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) -> U. A e. U. ( B X. C ) )
24 1 23 sylbi 
 |-  ( A e. ( B X. C ) -> U. A e. U. ( B X. C ) )