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 𝐼 = ( ℩ 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
opiota.2 𝑋 = ( 1st𝐼 )
opiota.3 𝑌 = ( 2nd𝐼 )
opiota.4 ( 𝑥 = 𝐶 → ( 𝜑𝜓 ) )
opiota.5 ( 𝑦 = 𝐷 → ( 𝜓𝜒 ) )
Assertion opiota ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( ( 𝐶𝐴𝐷𝐵𝜒 ) ↔ ( 𝐶 = 𝑋𝐷 = 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 opiota.1 𝐼 = ( ℩ 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
2 opiota.2 𝑋 = ( 1st𝐼 )
3 opiota.3 𝑌 = ( 2nd𝐼 )
4 opiota.4 ( 𝑥 = 𝐶 → ( 𝜑𝜓 ) )
5 opiota.5 ( 𝑦 = 𝐷 → ( 𝜓𝜒 ) )
6 4 5 ceqsrex2v ( ( 𝐶𝐴𝐷𝐵 ) → ( ∃ 𝑥𝐴𝑦𝐵 ( ( 𝑥 = 𝐶𝑦 = 𝐷 ) ∧ 𝜑 ) ↔ 𝜒 ) )
7 6 bicomd ( ( 𝐶𝐴𝐷𝐵 ) → ( 𝜒 ↔ ∃ 𝑥𝐴𝑦𝐵 ( ( 𝑥 = 𝐶𝑦 = 𝐷 ) ∧ 𝜑 ) ) )
8 opex 𝐶 , 𝐷 ⟩ ∈ V
9 8 a1i ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ V )
10 id ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
11 eqeq1 ( 𝑧 = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
12 eqcom ( ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
13 vex 𝑥 ∈ V
14 vex 𝑦 ∈ V
15 13 14 opth ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝑥 = 𝐶𝑦 = 𝐷 ) )
16 12 15 bitri ( ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑥 = 𝐶𝑦 = 𝐷 ) )
17 11 16 bitrdi ( 𝑧 = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑥 = 𝐶𝑦 = 𝐷 ) ) )
18 17 anbi1d ( 𝑧 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ( 𝑥 = 𝐶𝑦 = 𝐷 ) ∧ 𝜑 ) ) )
19 18 2rexbidv ( 𝑧 = ⟨ 𝐶 , 𝐷 ⟩ → ( ∃ 𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥𝐴𝑦𝐵 ( ( 𝑥 = 𝐶𝑦 = 𝐷 ) ∧ 𝜑 ) ) )
20 19 adantl ( ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∧ 𝑧 = ⟨ 𝐶 , 𝐷 ⟩ ) → ( ∃ 𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥𝐴𝑦𝐵 ( ( 𝑥 = 𝐶𝑦 = 𝐷 ) ∧ 𝜑 ) ) )
21 nfeu1 𝑧 ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
22 nfvd ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → Ⅎ 𝑧𝑥𝐴𝑦𝐵 ( ( 𝑥 = 𝐶𝑦 = 𝐷 ) ∧ 𝜑 ) )
23 nfcvd ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝑧𝐶 , 𝐷 ⟩ )
24 9 10 20 21 22 23 iota2df ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( ∃ 𝑥𝐴𝑦𝐵 ( ( 𝑥 = 𝐶𝑦 = 𝐷 ) ∧ 𝜑 ) ↔ ( ℩ 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) = ⟨ 𝐶 , 𝐷 ⟩ ) )
25 eqcom ( ⟨ 𝐶 , 𝐷 ⟩ = 𝐼𝐼 = ⟨ 𝐶 , 𝐷 ⟩ )
26 1 eqeq1i ( 𝐼 = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( ℩ 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) = ⟨ 𝐶 , 𝐷 ⟩ )
27 25 26 bitri ( ⟨ 𝐶 , 𝐷 ⟩ = 𝐼 ↔ ( ℩ 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) = ⟨ 𝐶 , 𝐷 ⟩ )
28 24 27 bitr4di ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( ∃ 𝑥𝐴𝑦𝐵 ( ( 𝑥 = 𝐶𝑦 = 𝐷 ) ∧ 𝜑 ) ↔ ⟨ 𝐶 , 𝐷 ⟩ = 𝐼 ) )
29 7 28 sylan9bbr ( ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∧ ( 𝐶𝐴𝐷𝐵 ) ) → ( 𝜒 ↔ ⟨ 𝐶 , 𝐷 ⟩ = 𝐼 ) )
30 29 pm5.32da ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( ( ( 𝐶𝐴𝐷𝐵 ) ∧ 𝜒 ) ↔ ( ( 𝐶𝐴𝐷𝐵 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ = 𝐼 ) ) )
31 opelxpi ( ( 𝑥𝐴𝑦𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
32 simpl ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
33 32 eleq1d ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
34 31 33 syl5ibrcom ( ( 𝑥𝐴𝑦𝐵 ) → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝑧 ∈ ( 𝐴 × 𝐵 ) ) )
35 34 rexlimivv ( ∃ 𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝑧 ∈ ( 𝐴 × 𝐵 ) )
36 35 abssi { 𝑧 ∣ ∃ 𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ⊆ ( 𝐴 × 𝐵 )
37 iotacl ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( ℩ 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ∈ { 𝑧 ∣ ∃ 𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } )
38 36 37 sselid ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( ℩ 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ∈ ( 𝐴 × 𝐵 ) )
39 1 38 eqeltrid ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝐼 ∈ ( 𝐴 × 𝐵 ) )
40 opelxp ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝐶𝐴𝐷𝐵 ) )
41 eleq1 ( ⟨ 𝐶 , 𝐷 ⟩ = 𝐼 → ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ 𝐼 ∈ ( 𝐴 × 𝐵 ) ) )
42 40 41 bitr3id ( ⟨ 𝐶 , 𝐷 ⟩ = 𝐼 → ( ( 𝐶𝐴𝐷𝐵 ) ↔ 𝐼 ∈ ( 𝐴 × 𝐵 ) ) )
43 39 42 syl5ibrcom ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( ⟨ 𝐶 , 𝐷 ⟩ = 𝐼 → ( 𝐶𝐴𝐷𝐵 ) ) )
44 43 pm4.71rd ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( ⟨ 𝐶 , 𝐷 ⟩ = 𝐼 ↔ ( ( 𝐶𝐴𝐷𝐵 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ = 𝐼 ) ) )
45 1st2nd2 ( 𝐼 ∈ ( 𝐴 × 𝐵 ) → 𝐼 = ⟨ ( 1st𝐼 ) , ( 2nd𝐼 ) ⟩ )
46 39 45 syl ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝐼 = ⟨ ( 1st𝐼 ) , ( 2nd𝐼 ) ⟩ )
47 46 eqeq2d ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( ⟨ 𝐶 , 𝐷 ⟩ = 𝐼 ↔ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ ( 1st𝐼 ) , ( 2nd𝐼 ) ⟩ ) )
48 30 44 47 3bitr2d ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( ( ( 𝐶𝐴𝐷𝐵 ) ∧ 𝜒 ) ↔ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ ( 1st𝐼 ) , ( 2nd𝐼 ) ⟩ ) )
49 df-3an ( ( 𝐶𝐴𝐷𝐵𝜒 ) ↔ ( ( 𝐶𝐴𝐷𝐵 ) ∧ 𝜒 ) )
50 2 eqeq2i ( 𝐶 = 𝑋𝐶 = ( 1st𝐼 ) )
51 3 eqeq2i ( 𝐷 = 𝑌𝐷 = ( 2nd𝐼 ) )
52 50 51 anbi12i ( ( 𝐶 = 𝑋𝐷 = 𝑌 ) ↔ ( 𝐶 = ( 1st𝐼 ) ∧ 𝐷 = ( 2nd𝐼 ) ) )
53 fvex ( 1st𝐼 ) ∈ V
54 fvex ( 2nd𝐼 ) ∈ V
55 53 54 opth2 ( ⟨ 𝐶 , 𝐷 ⟩ = ⟨ ( 1st𝐼 ) , ( 2nd𝐼 ) ⟩ ↔ ( 𝐶 = ( 1st𝐼 ) ∧ 𝐷 = ( 2nd𝐼 ) ) )
56 52 55 bitr4i ( ( 𝐶 = 𝑋𝐷 = 𝑌 ) ↔ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ ( 1st𝐼 ) , ( 2nd𝐼 ) ⟩ )
57 48 49 56 3bitr4g ( ∃! 𝑧𝑥𝐴𝑦𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( ( 𝐶𝐴𝐷𝐵𝜒 ) ↔ ( 𝐶 = 𝑋𝐷 = 𝑌 ) ) )