Metamath Proof Explorer

Theorem opiota

Description: The property of a uniquely specified ordered pair. The proof uses properties of the iota description binder. (Contributed by Mario Carneiro, 21-May-2015)

Ref Expression
Hypotheses opiota.1 
|- I = ( iota z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) )
opiota.2 
|- X = ( 1st ` I )
opiota.3 
|- Y = ( 2nd ` I )
opiota.4 
|- ( x = C -> ( ph <-> ps ) )
opiota.5 
|- ( y = D -> ( ps <-> ch ) )
Assertion opiota 
|- ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> ( ( C e. A /\ D e. B /\ ch ) <-> ( C = X /\ D = Y ) ) )

Proof

Step Hyp Ref Expression
1 opiota.1 
 |-  I = ( iota z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) )
2 opiota.2 
 |-  X = ( 1st ` I )
3 opiota.3 
 |-  Y = ( 2nd ` I )
4 opiota.4 
 |-  ( x = C -> ( ph <-> ps ) )
5 opiota.5 
 |-  ( y = D -> ( ps <-> ch ) )
6 4 5 ceqsrex2v 
 |-  ( ( C e. A /\ D e. B ) -> ( E. x e. A E. y e. B ( ( x = C /\ y = D ) /\ ph ) <-> ch ) )
7 6 bicomd 
 |-  ( ( C e. A /\ D e. B ) -> ( ch <-> E. x e. A E. y e. B ( ( x = C /\ y = D ) /\ ph ) ) )
8 opex 
 |-  <. C , D >. e. _V
9 8 a1i 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> <. C , D >. e. _V )
10 id 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) )
11 eqeq1 
 |-  ( z = <. C , D >. -> ( z = <. x , y >. <-> <. C , D >. = <. x , y >. ) )
12 eqcom 
 |-  ( <. C , D >. = <. x , y >. <-> <. x , y >. = <. C , D >. )
13 vex 
 |-  x e. _V
14 vex 
 |-  y e. _V
15 13 14 opth 
 |-  ( <. x , y >. = <. C , D >. <-> ( x = C /\ y = D ) )
16 12 15 bitri 
 |-  ( <. C , D >. = <. x , y >. <-> ( x = C /\ y = D ) )
17 11 16 bitrdi 
 |-  ( z = <. C , D >. -> ( z = <. x , y >. <-> ( x = C /\ y = D ) ) )
18 17 anbi1d 
 |-  ( z = <. C , D >. -> ( ( z = <. x , y >. /\ ph ) <-> ( ( x = C /\ y = D ) /\ ph ) ) )
19 18 2rexbidv 
 |-  ( z = <. C , D >. -> ( E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) <-> E. x e. A E. y e. B ( ( x = C /\ y = D ) /\ ph ) ) )
20 19 adantl 
 |-  ( ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) /\ z = <. C , D >. ) -> ( E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) <-> E. x e. A E. y e. B ( ( x = C /\ y = D ) /\ ph ) ) )
21 nfeu1 
 |-  F/ z E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph )
22 nfvd 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> F/ z E. x e. A E. y e. B ( ( x = C /\ y = D ) /\ ph ) )
23 nfcvd 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> F/_ z <. C , D >. )
24 9 10 20 21 22 23 iota2df 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> ( E. x e. A E. y e. B ( ( x = C /\ y = D ) /\ ph ) <-> ( iota z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) ) = <. C , D >. ) )
25 eqcom 
 |-  ( <. C , D >. = I <-> I = <. C , D >. )
26 1 eqeq1i 
 |-  ( I = <. C , D >. <-> ( iota z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) ) = <. C , D >. )
27 25 26 bitri 
 |-  ( <. C , D >. = I <-> ( iota z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) ) = <. C , D >. )
28 24 27 bitr4di 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> ( E. x e. A E. y e. B ( ( x = C /\ y = D ) /\ ph ) <-> <. C , D >. = I ) )
29 7 28 sylan9bbr 
 |-  ( ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) /\ ( C e. A /\ D e. B ) ) -> ( ch <-> <. C , D >. = I ) )
30 29 pm5.32da 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> ( ( ( C e. A /\ D e. B ) /\ ch ) <-> ( ( C e. A /\ D e. B ) /\ <. C , D >. = I ) ) )
31 opelxpi 
 |-  ( ( x e. A /\ y e. B ) -> <. x , y >. e. ( A X. B ) )
32 simpl 
 |-  ( ( z = <. x , y >. /\ ph ) -> z = <. x , y >. )
33 32 eleq1d 
 |-  ( ( z = <. x , y >. /\ ph ) -> ( z e. ( A X. B ) <-> <. x , y >. e. ( A X. B ) ) )
34 31 33 syl5ibrcom 
 |-  ( ( x e. A /\ y e. B ) -> ( ( z = <. x , y >. /\ ph ) -> z e. ( A X. B ) ) )
35 34 rexlimivv 
 |-  ( E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> z e. ( A X. B ) )
36 35 abssi 
 |-  { z | E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) } C_ ( A X. B )
37 iotacl 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> ( iota z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) ) e. { z | E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) } )
38 36 37 sseldi 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> ( iota z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) ) e. ( A X. B ) )
39 1 38 eqeltrid 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> I e. ( A X. B ) )
40 opelxp 
 |-  ( <. C , D >. e. ( A X. B ) <-> ( C e. A /\ D e. B ) )
41 eleq1 
 |-  ( <. C , D >. = I -> ( <. C , D >. e. ( A X. B ) <-> I e. ( A X. B ) ) )
42 40 41 bitr3id 
 |-  ( <. C , D >. = I -> ( ( C e. A /\ D e. B ) <-> I e. ( A X. B ) ) )
43 39 42 syl5ibrcom 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> ( <. C , D >. = I -> ( C e. A /\ D e. B ) ) )
44 43 pm4.71rd 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> ( <. C , D >. = I <-> ( ( C e. A /\ D e. B ) /\ <. C , D >. = I ) ) )
45 1st2nd2 
 |-  ( I e. ( A X. B ) -> I = <. ( 1st ` I ) , ( 2nd ` I ) >. )
46 39 45 syl 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> I = <. ( 1st ` I ) , ( 2nd ` I ) >. )
47 46 eqeq2d 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> ( <. C , D >. = I <-> <. C , D >. = <. ( 1st ` I ) , ( 2nd ` I ) >. ) )
48 30 44 47 3bitr2d 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> ( ( ( C e. A /\ D e. B ) /\ ch ) <-> <. C , D >. = <. ( 1st ` I ) , ( 2nd ` I ) >. ) )
49 df-3an 
 |-  ( ( C e. A /\ D e. B /\ ch ) <-> ( ( C e. A /\ D e. B ) /\ ch ) )
50 2 eqeq2i 
 |-  ( C = X <-> C = ( 1st ` I ) )
51 3 eqeq2i 
 |-  ( D = Y <-> D = ( 2nd ` I ) )
52 50 51 anbi12i 
 |-  ( ( C = X /\ D = Y ) <-> ( C = ( 1st ` I ) /\ D = ( 2nd ` I ) ) )
53 fvex 
 |-  ( 1st ` I ) e. _V
54 fvex 
 |-  ( 2nd ` I ) e. _V
55 53 54 opth2 
 |-  ( <. C , D >. = <. ( 1st ` I ) , ( 2nd ` I ) >. <-> ( C = ( 1st ` I ) /\ D = ( 2nd ` I ) ) )
56 52 55 bitr4i 
 |-  ( ( C = X /\ D = Y ) <-> <. C , D >. = <. ( 1st ` I ) , ( 2nd ` I ) >. )
57 48 49 56 3bitr4g 
 |-  ( E! z E. x e. A E. y e. B ( z = <. x , y >. /\ ph ) -> ( ( C e. A /\ D e. B /\ ch ) <-> ( C = X /\ D = Y ) ) )