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 = ι z | x A y B z = x y φ
opiota.2 X = 1 st I
opiota.3 Y = 2 nd I
opiota.4 x = C φ ψ
opiota.5 y = D ψ χ
Assertion opiota ∃! z x A y B z = x y φ C A D B χ C = X D = Y

Proof

Step Hyp Ref Expression
1 opiota.1 I = ι z | x A y B z = x y φ
2 opiota.2 X = 1 st I
3 opiota.3 Y = 2 nd I
4 opiota.4 x = C φ ψ
5 opiota.5 y = D ψ χ
6 4 5 ceqsrex2v C A D B x A y B x = C y = D φ χ
7 6 bicomd C A D B χ x A y B x = C y = D φ
8 opex C D V
9 8 a1i ∃! z x A y B z = x y φ C D V
10 id ∃! z x A y B z = x y φ ∃! z x A y B z = x y φ
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 V
14 vex y 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 φ x = C y = D φ
19 18 2rexbidv z = C D x A y B z = x y φ x A y B x = C y = D φ
20 19 adantl ∃! z x A y B z = x y φ z = C D x A y B z = x y φ x A y B x = C y = D φ
21 nfeu1 z ∃! z x A y B z = x y φ
22 nfvd ∃! z x A y B z = x y φ z x A y B x = C y = D φ
23 nfcvd ∃! z x A y B z = x y φ _ z C D
24 9 10 20 21 22 23 iota2df ∃! z x A y B z = x y φ x A y B x = C y = D φ ι z | x A y B z = x y φ = C D
25 eqcom C D = I I = C D
26 1 eqeq1i I = C D ι z | x A y B z = x y φ = C D
27 25 26 bitri C D = I ι z | x A y B z = x y φ = C D
28 24 27 bitr4di ∃! z x A y B z = x y φ x A y B x = C y = D φ C D = I
29 7 28 sylan9bbr ∃! z x A y B z = x y φ C A D B χ C D = I
30 29 pm5.32da ∃! z x A y B z = x y φ C A D B χ C A D B C D = I
31 opelxpi x A y B x y A × B
32 simpl z = x y φ z = x y
33 32 eleq1d z = x y φ z A × B x y A × B
34 31 33 syl5ibrcom x A y B z = x y φ z A × B
35 34 rexlimivv x A y B z = x y φ z A × B
36 35 abssi z | x A y B z = x y φ A × B
37 iotacl ∃! z x A y B z = x y φ ι z | x A y B z = x y φ z | x A y B z = x y φ
38 36 37 sseldi ∃! z x A y B z = x y φ ι z | x A y B z = x y φ A × B
39 1 38 eqeltrid ∃! z x A y B z = x y φ I A × B
40 opelxp C D A × B C A D B
41 eleq1 C D = I C D A × B I A × B
42 40 41 bitr3id C D = I C A D B I A × B
43 39 42 syl5ibrcom ∃! z x A y B z = x y φ C D = I C A D B
44 43 pm4.71rd ∃! z x A y B z = x y φ C D = I C A D B C D = I
45 1st2nd2 I A × B I = 1 st I 2 nd I
46 39 45 syl ∃! z x A y B z = x y φ I = 1 st I 2 nd I
47 46 eqeq2d ∃! z x A y B z = x y φ C D = I C D = 1 st I 2 nd I
48 30 44 47 3bitr2d ∃! z x A y B z = x y φ C A D B χ C D = 1 st I 2 nd I
49 df-3an C A D B χ C A D B χ
50 2 eqeq2i C = X C = 1 st I
51 3 eqeq2i D = Y D = 2 nd I
52 50 51 anbi12i C = X D = Y C = 1 st I D = 2 nd I
53 fvex 1 st I V
54 fvex 2 nd I V
55 53 54 opth2 C D = 1 st I 2 nd I C = 1 st I D = 2 nd I
56 52 55 bitr4i C = X D = Y C D = 1 st I 2 nd I
57 48 49 56 3bitr4g ∃! z x A y B z = x y φ C A D B χ C = X D = Y