Metamath Proof Explorer

Theorem elxp5

Description: Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 when the double intersection does not create class existence problems (caused by int0 ). (Contributed by NM, 1-Aug-2004)

Ref Expression
Assertion elxp5 
|- ( A e. ( B X. C ) <-> ( A = <. |^| |^| A , U. ran { A } >. /\ ( |^| |^| A e. B /\ U. ran { A } e. C ) ) )

Proof

Step Hyp Ref Expression
1 elxp 
 |-  ( A e. ( B X. C ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )
2 sneq 
 |-  ( A = <. x , y >. -> { A } = { <. x , y >. } )
3 2 rneqd 
 |-  ( A = <. x , y >. -> ran { A } = ran { <. x , y >. } )
4 3 unieqd 
 |-  ( A = <. x , y >. -> U. ran { A } = U. ran { <. x , y >. } )
5 vex 
 |-  x e. _V
6 vex 
 |-  y e. _V
7 5 6 op2nda 
 |-  U. ran { <. x , y >. } = y
8 4 7 eqtr2di 
 |-  ( A = <. x , y >. -> y = U. ran { A } )
9 8 pm4.71ri 
 |-  ( A = <. x , y >. <-> ( y = U. ran { A } /\ A = <. x , y >. ) )
10 9 anbi1i 
 |-  ( ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> ( ( y = U. ran { A } /\ A = <. x , y >. ) /\ ( x e. B /\ y e. C ) ) )
11 anass 
 |-  ( ( ( y = U. ran { A } /\ A = <. x , y >. ) /\ ( x e. B /\ y e. C ) ) <-> ( y = U. ran { A } /\ ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
12 10 11 bitri 
 |-  ( ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> ( y = U. ran { A } /\ ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
13 12 exbii 
 |-  ( E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> E. y ( y = U. ran { A } /\ ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
14 snex 
 |-  { A } e. _V
15 14 rnex 
 |-  ran { A } e. _V
16 15 uniex 
 |-  U. ran { A } e. _V
17 opeq2 
 |-  ( y = U. ran { A } -> <. x , y >. = <. x , U. ran { A } >. )
18 17 eqeq2d 
 |-  ( y = U. ran { A } -> ( A = <. x , y >. <-> A = <. x , U. ran { A } >. ) )
19 eleq1 
 |-  ( y = U. ran { A } -> ( y e. C <-> U. ran { A } e. C ) )
20 19 anbi2d 
 |-  ( y = U. ran { A } -> ( ( x e. B /\ y e. C ) <-> ( x e. B /\ U. ran { A } e. C ) ) )
21 18 20 anbi12d 
 |-  ( y = U. ran { A } -> ( ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) ) )
22 16 21 ceqsexv 
 |-  ( E. y ( y = U. ran { A } /\ ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) <-> ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) )
23 13 22 bitri 
 |-  ( E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) )
24 inteq 
 |-  ( A = <. x , U. ran { A } >. -> |^| A = |^| <. x , U. ran { A } >. )
25 24 inteqd 
 |-  ( A = <. x , U. ran { A } >. -> |^| |^| A = |^| |^| <. x , U. ran { A } >. )
26 5 16 op1stb 
 |-  |^| |^| <. x , U. ran { A } >. = x
27 25 26 eqtr2di 
 |-  ( A = <. x , U. ran { A } >. -> x = |^| |^| A )
28 27 pm4.71ri 
 |-  ( A = <. x , U. ran { A } >. <-> ( x = |^| |^| A /\ A = <. x , U. ran { A } >. ) )
29 28 anbi1i 
 |-  ( ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) <-> ( ( x = |^| |^| A /\ A = <. x , U. ran { A } >. ) /\ ( x e. B /\ U. ran { A } e. C ) ) )
30 anass 
 |-  ( ( ( x = |^| |^| A /\ A = <. x , U. ran { A } >. ) /\ ( x e. B /\ U. ran { A } e. C ) ) <-> ( x = |^| |^| A /\ ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) ) )
31 23 29 30 3bitri 
 |-  ( E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> ( x = |^| |^| A /\ ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) ) )
32 31 exbii 
 |-  ( E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> E. x ( x = |^| |^| A /\ ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) ) )
33 eqvisset 
 |-  ( x = |^| |^| A -> |^| |^| A e. _V )
34 33 adantr 
 |-  ( ( x = |^| |^| A /\ ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) ) -> |^| |^| A e. _V )
35 34 exlimiv 
 |-  ( E. x ( x = |^| |^| A /\ ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) ) -> |^| |^| A e. _V )
36 elex 
 |-  ( |^| |^| A e. B -> |^| |^| A e. _V )
37 36 ad2antrl 
 |-  ( ( A = <. |^| |^| A , U. ran { A } >. /\ ( |^| |^| A e. B /\ U. ran { A } e. C ) ) -> |^| |^| A e. _V )
38 opeq1 
 |-  ( x = |^| |^| A -> <. x , U. ran { A } >. = <. |^| |^| A , U. ran { A } >. )
39 38 eqeq2d 
 |-  ( x = |^| |^| A -> ( A = <. x , U. ran { A } >. <-> A = <. |^| |^| A , U. ran { A } >. ) )
40 eleq1 
 |-  ( x = |^| |^| A -> ( x e. B <-> |^| |^| A e. B ) )
41 40 anbi1d 
 |-  ( x = |^| |^| A -> ( ( x e. B /\ U. ran { A } e. C ) <-> ( |^| |^| A e. B /\ U. ran { A } e. C ) ) )
42 39 41 anbi12d 
 |-  ( x = |^| |^| A -> ( ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) <-> ( A = <. |^| |^| A , U. ran { A } >. /\ ( |^| |^| A e. B /\ U. ran { A } e. C ) ) ) )
43 42 ceqsexgv 
 |-  ( |^| |^| A e. _V -> ( E. x ( x = |^| |^| A /\ ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) ) <-> ( A = <. |^| |^| A , U. ran { A } >. /\ ( |^| |^| A e. B /\ U. ran { A } e. C ) ) ) )
44 35 37 43 pm5.21nii 
 |-  ( E. x ( x = |^| |^| A /\ ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) ) <-> ( A = <. |^| |^| A , U. ran { A } >. /\ ( |^| |^| A e. B /\ U. ran { A } e. C ) ) )
45 1 32 44 3bitri 
 |-  ( A e. ( B X. C ) <-> ( A = <. |^| |^| A , U. ran { A } >. /\ ( |^| |^| A e. B /\ U. ran { A } e. C ) ) )