This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opreuopreu

Description: There is a unique ordered pair fulfilling a wff iff its components fulfil a corresponding wff. (Contributed by AV, 2-Jul-2023)

Ref Expression
Hypothesis opreuopreu.a ⊢ ( ( 𝑎 = ( 1st ‘ 𝑝 ) ∧ 𝑏 = ( 2nd ‘ 𝑝 ) ) → ( 𝜓 ↔ 𝜑 ) )
Assertion opreuopreu ( ∃! 𝑝 ∈ ( 𝐴 × 𝐵 ) 𝜑 ↔ ∃! 𝑝 ∈ ( 𝐴 × 𝐵 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 opreuopreu.a ⊢ ( ( 𝑎 = ( 1st ‘ 𝑝 ) ∧ 𝑏 = ( 2nd ‘ 𝑝 ) ) → ( 𝜓 ↔ 𝜑 ) )
2 elxpi ⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) )
3 simprl ⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ) → 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ )
4 vex ⊢ 𝑎 ∈ V
5 vex ⊢ 𝑏 ∈ V
6 4 5 op1st ⊢ ( 1st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑎
7 6 eqcomi ⊢ 𝑎 = ( 1st ‘ ⟨ 𝑎 , 𝑏 ⟩ )
8 4 5 op2nd ⊢ ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑏
9 8 eqcomi ⊢ 𝑏 = ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ )
10 7 9 pm3.2i ⊢ ( 𝑎 = ( 1st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑏 = ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
11 fveq2 ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 1st ‘ 𝑝 ) = ( 1st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
12 11 eqeq2d ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑎 = ( 1st ‘ 𝑝 ) ↔ 𝑎 = ( 1st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
13 fveq2 ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 2nd ‘ 𝑝 ) = ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
14 13 eqeq2d ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑏 = ( 2nd ‘ 𝑝 ) ↔ 𝑏 = ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
15 12 14 anbi12d ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑎 = ( 1st ‘ 𝑝 ) ∧ 𝑏 = ( 2nd ‘ 𝑝 ) ) ↔ ( 𝑎 = ( 1st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑏 = ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) ) )
16 10 15 mpbiri ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑎 = ( 1st ‘ 𝑝 ) ∧ 𝑏 = ( 2nd ‘ 𝑝 ) ) )
17 16 1 syl ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜓 ↔ 𝜑 ) )
18 17 biimprd ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜑 → 𝜓 ) )
19 18 adantr ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝜑 → 𝜓 ) )
20 19 impcom ⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ) → 𝜓 )
21 3 20 jca ⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ) → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) )
22 21 ex ⊢ ( 𝜑 → ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) ) )
23 22 2eximdv ⊢ ( 𝜑 → ( ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) ) )
24 2 23 syl5com ⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ( 𝜑 → ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) ) )
25 17 biimpa ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) → 𝜑 )
26 25 a1i ⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) → 𝜑 ) )
27 26 exlimdvv ⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ( ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) → 𝜑 ) )
28 24 27 impbid ⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ( 𝜑 ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) ) )
29 28 reubiia ⊢ ( ∃! 𝑝 ∈ ( 𝐴 × 𝐵 ) 𝜑 ↔ ∃! 𝑝 ∈ ( 𝐴 × 𝐵 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜓 ) )