Metamath Proof Explorer

Theorem elxp4

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp5 , elxp6 , and elxp7 . (Contributed by NM, 17-Feb-2004)

Ref Expression
Assertion elxp4 
|- ( A e. ( B X. C ) <-> ( A = <. U. dom { A } , U. ran { A } >. /\ ( U. dom { 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 sneq 
 |-  ( A = <. x , U. ran { A } >. -> { A } = { <. x , U. ran { A } >. } )
25 24 dmeqd 
 |-  ( A = <. x , U. ran { A } >. -> dom { A } = dom { <. x , U. ran { A } >. } )
26 25 unieqd 
 |-  ( A = <. x , U. ran { A } >. -> U. dom { A } = U. dom { <. x , U. ran { A } >. } )
27 5 16 op1sta 
 |-  U. dom { <. x , U. ran { A } >. } = x
28 26 27 eqtr2di 
 |-  ( A = <. x , U. ran { A } >. -> x = U. dom { A } )
29 28 pm4.71ri 
 |-  ( A = <. x , U. ran { A } >. <-> ( x = U. dom { A } /\ A = <. x , U. ran { A } >. ) )
30 29 anbi1i 
 |-  ( ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) <-> ( ( x = U. dom { A } /\ A = <. x , U. ran { A } >. ) /\ ( x e. B /\ U. ran { A } e. C ) ) )
31 anass 
 |-  ( ( ( x = U. dom { A } /\ A = <. x , U. ran { A } >. ) /\ ( x e. B /\ U. ran { A } e. C ) ) <-> ( x = U. dom { A } /\ ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) ) )
32 23 30 31 3bitri 
 |-  ( E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> ( x = U. dom { A } /\ ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) ) )
33 32 exbii 
 |-  ( E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> E. x ( x = U. dom { A } /\ ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) ) )
34 14 dmex 
 |-  dom { A } e. _V
35 34 uniex 
 |-  U. dom { A } e. _V
36 opeq1 
 |-  ( x = U. dom { A } -> <. x , U. ran { A } >. = <. U. dom { A } , U. ran { A } >. )
37 36 eqeq2d 
 |-  ( x = U. dom { A } -> ( A = <. x , U. ran { A } >. <-> A = <. U. dom { A } , U. ran { A } >. ) )
38 eleq1 
 |-  ( x = U. dom { A } -> ( x e. B <-> U. dom { A } e. B ) )
39 38 anbi1d 
 |-  ( x = U. dom { A } -> ( ( x e. B /\ U. ran { A } e. C ) <-> ( U. dom { A } e. B /\ U. ran { A } e. C ) ) )
40 37 39 anbi12d 
 |-  ( x = U. dom { A } -> ( ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) <-> ( A = <. U. dom { A } , U. ran { A } >. /\ ( U. dom { A } e. B /\ U. ran { A } e. C ) ) ) )
41 35 40 ceqsexv 
 |-  ( E. x ( x = U. dom { A } /\ ( A = <. x , U. ran { A } >. /\ ( x e. B /\ U. ran { A } e. C ) ) ) <-> ( A = <. U. dom { A } , U. ran { A } >. /\ ( U. dom { A } e. B /\ U. ran { A } e. C ) ) )
42 1 33 41 3bitri 
 |-  ( A e. ( B X. C ) <-> ( A = <. U. dom { A } , U. ran { A } >. /\ ( U. dom { A } e. B /\ U. ran { A } e. C ) ) )