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}=\left(\iota {z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\right)$
opiota.2 ${⊢}{X}={1}^{st}\left({I}\right)$
opiota.3 ${⊢}{Y}={2}^{nd}\left({I}\right)$
opiota.4 ${⊢}{x}={C}\to \left({\phi }↔{\psi }\right)$
opiota.5 ${⊢}{y}={D}\to \left({\psi }↔{\chi }\right)$
Assertion opiota ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \left(\left({C}\in {A}\wedge {D}\in {B}\wedge {\chi }\right)↔\left({C}={X}\wedge {D}={Y}\right)\right)$

Proof

Step Hyp Ref Expression
1 opiota.1 ${⊢}{I}=\left(\iota {z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\right)$
2 opiota.2 ${⊢}{X}={1}^{st}\left({I}\right)$
3 opiota.3 ${⊢}{Y}={2}^{nd}\left({I}\right)$
4 opiota.4 ${⊢}{x}={C}\to \left({\phi }↔{\psi }\right)$
5 opiota.5 ${⊢}{y}={D}\to \left({\psi }↔{\chi }\right)$
6 4 5 ceqsrex2v ${⊢}\left({C}\in {A}\wedge {D}\in {B}\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}={C}\wedge {y}={D}\right)\wedge {\phi }\right)↔{\chi }\right)$
7 6 bicomd ${⊢}\left({C}\in {A}\wedge {D}\in {B}\right)\to \left({\chi }↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}={C}\wedge {y}={D}\right)\wedge {\phi }\right)\right)$
8 opex ${⊢}⟨{C},{D}⟩\in \mathrm{V}$
9 8 a1i ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to ⟨{C},{D}⟩\in \mathrm{V}$
10 id ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)$
11 eqeq1 ${⊢}{z}=⟨{C},{D}⟩\to \left({z}=⟨{x},{y}⟩↔⟨{C},{D}⟩=⟨{x},{y}⟩\right)$
12 eqcom ${⊢}⟨{C},{D}⟩=⟨{x},{y}⟩↔⟨{x},{y}⟩=⟨{C},{D}⟩$
13 vex ${⊢}{x}\in \mathrm{V}$
14 vex ${⊢}{y}\in \mathrm{V}$
15 13 14 opth ${⊢}⟨{x},{y}⟩=⟨{C},{D}⟩↔\left({x}={C}\wedge {y}={D}\right)$
16 12 15 bitri ${⊢}⟨{C},{D}⟩=⟨{x},{y}⟩↔\left({x}={C}\wedge {y}={D}\right)$
17 11 16 syl6bb ${⊢}{z}=⟨{C},{D}⟩\to \left({z}=⟨{x},{y}⟩↔\left({x}={C}\wedge {y}={D}\right)\right)$
18 17 anbi1d ${⊢}{z}=⟨{C},{D}⟩\to \left(\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)↔\left(\left({x}={C}\wedge {y}={D}\right)\wedge {\phi }\right)\right)$
19 18 2rexbidv ${⊢}{z}=⟨{C},{D}⟩\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}={C}\wedge {y}={D}\right)\wedge {\phi }\right)\right)$
20 19 adantl ${⊢}\left(\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\wedge {z}=⟨{C},{D}⟩\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}={C}\wedge {y}={D}\right)\wedge {\phi }\right)\right)$
21 nfeu1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)$
22 nfvd ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to Ⅎ{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}={C}\wedge {y}={D}\right)\wedge {\phi }\right)$
23 nfcvd ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}⟨{C},{D}⟩$
24 9 10 20 21 22 23 iota2df ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}={C}\wedge {y}={D}\right)\wedge {\phi }\right)↔\left(\iota {z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\right)=⟨{C},{D}⟩\right)$
25 eqcom ${⊢}⟨{C},{D}⟩={I}↔{I}=⟨{C},{D}⟩$
26 1 eqeq1i ${⊢}{I}=⟨{C},{D}⟩↔\left(\iota {z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\right)=⟨{C},{D}⟩$
27 25 26 bitri ${⊢}⟨{C},{D}⟩={I}↔\left(\iota {z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\right)=⟨{C},{D}⟩$
28 24 27 syl6bbr ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}={C}\wedge {y}={D}\right)\wedge {\phi }\right)↔⟨{C},{D}⟩={I}\right)$
29 7 28 sylan9bbr ${⊢}\left(\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\wedge \left({C}\in {A}\wedge {D}\in {B}\right)\right)\to \left({\chi }↔⟨{C},{D}⟩={I}\right)$
30 29 pm5.32da ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \left(\left(\left({C}\in {A}\wedge {D}\in {B}\right)\wedge {\chi }\right)↔\left(\left({C}\in {A}\wedge {D}\in {B}\right)\wedge ⟨{C},{D}⟩={I}\right)\right)$
31 opelxpi ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to ⟨{x},{y}⟩\in \left({A}×{B}\right)$
32 simpl ${⊢}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to {z}=⟨{x},{y}⟩$
33 32 eleq1d ${⊢}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \left({z}\in \left({A}×{B}\right)↔⟨{x},{y}⟩\in \left({A}×{B}\right)\right)$
34 31 33 syl5ibrcom ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to \left(\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to {z}\in \left({A}×{B}\right)\right)$
35 34 rexlimivv ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to {z}\in \left({A}×{B}\right)$
36 35 abssi ${⊢}\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\right\}\subseteq {A}×{B}$
37 iotacl ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \left(\iota {z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\right)\in \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\right\}$
38 36 37 sseldi ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \left(\iota {z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\right)\in \left({A}×{B}\right)$
39 1 38 eqeltrid ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to {I}\in \left({A}×{B}\right)$
40 opelxp ${⊢}⟨{C},{D}⟩\in \left({A}×{B}\right)↔\left({C}\in {A}\wedge {D}\in {B}\right)$
41 eleq1 ${⊢}⟨{C},{D}⟩={I}\to \left(⟨{C},{D}⟩\in \left({A}×{B}\right)↔{I}\in \left({A}×{B}\right)\right)$
42 40 41 syl5bbr ${⊢}⟨{C},{D}⟩={I}\to \left(\left({C}\in {A}\wedge {D}\in {B}\right)↔{I}\in \left({A}×{B}\right)\right)$
43 39 42 syl5ibrcom ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \left(⟨{C},{D}⟩={I}\to \left({C}\in {A}\wedge {D}\in {B}\right)\right)$
44 43 pm4.71rd ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \left(⟨{C},{D}⟩={I}↔\left(\left({C}\in {A}\wedge {D}\in {B}\right)\wedge ⟨{C},{D}⟩={I}\right)\right)$
45 1st2nd2 ${⊢}{I}\in \left({A}×{B}\right)\to {I}=⟨{1}^{st}\left({I}\right),{2}^{nd}\left({I}\right)⟩$
46 39 45 syl ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to {I}=⟨{1}^{st}\left({I}\right),{2}^{nd}\left({I}\right)⟩$
47 46 eqeq2d ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \left(⟨{C},{D}⟩={I}↔⟨{C},{D}⟩=⟨{1}^{st}\left({I}\right),{2}^{nd}\left({I}\right)⟩\right)$
48 30 44 47 3bitr2d ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \left(\left(\left({C}\in {A}\wedge {D}\in {B}\right)\wedge {\chi }\right)↔⟨{C},{D}⟩=⟨{1}^{st}\left({I}\right),{2}^{nd}\left({I}\right)⟩\right)$
49 df-3an ${⊢}\left({C}\in {A}\wedge {D}\in {B}\wedge {\chi }\right)↔\left(\left({C}\in {A}\wedge {D}\in {B}\right)\wedge {\chi }\right)$
50 2 eqeq2i ${⊢}{C}={X}↔{C}={1}^{st}\left({I}\right)$
51 3 eqeq2i ${⊢}{D}={Y}↔{D}={2}^{nd}\left({I}\right)$
52 50 51 anbi12i ${⊢}\left({C}={X}\wedge {D}={Y}\right)↔\left({C}={1}^{st}\left({I}\right)\wedge {D}={2}^{nd}\left({I}\right)\right)$
53 fvex ${⊢}{1}^{st}\left({I}\right)\in \mathrm{V}$
54 fvex ${⊢}{2}^{nd}\left({I}\right)\in \mathrm{V}$
55 53 54 opth2 ${⊢}⟨{C},{D}⟩=⟨{1}^{st}\left({I}\right),{2}^{nd}\left({I}\right)⟩↔\left({C}={1}^{st}\left({I}\right)\wedge {D}={2}^{nd}\left({I}\right)\right)$
56 52 55 bitr4i ${⊢}\left({C}={X}\wedge {D}={Y}\right)↔⟨{C},{D}⟩=⟨{1}^{st}\left({I}\right),{2}^{nd}\left({I}\right)⟩$
57 48 49 56 3bitr4g ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge {\phi }\right)\to \left(\left({C}\in {A}\wedge {D}\in {B}\wedge {\chi }\right)↔\left({C}={X}\wedge {D}={Y}\right)\right)$