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 ⊢ ( ∃! 𝑧 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝜒 ) ↔ ( 𝐶 = 𝑋 ∧ 𝐷 = 𝑌 ) ) )