Metamath Proof Explorer

Theorem cic1st2nd

Description: Reconstruction of a pair of isomorphic objects in terms of its ordered pair components. (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Assertion cic1st2nd ⊢ P ∈ ≃ 𝑐 ⁡ C → P = 1 st ⁡ P 2 nd ⁡ P

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ P ∈ ≃ 𝑐 ⁡ C → C ∈ dom ⁡ ≃ 𝑐
2 cicfn ⊢ ≃ 𝑐 Fn Cat
3 2 fndmi ⊢ dom ⁡ ≃ 𝑐 = Cat
4 1 3 eleqtrdi ⊢ P ∈ ≃ 𝑐 ⁡ C → C ∈ Cat
5 relcic ⊢ C ∈ Cat → Rel ⁡ ≃ 𝑐 ⁡ C
6 4 5 syl ⊢ P ∈ ≃ 𝑐 ⁡ C → Rel ⁡ ≃ 𝑐 ⁡ C
7 1st2nd ⊢ Rel ⁡ ≃ 𝑐 ⁡ C ∧ P ∈ ≃ 𝑐 ⁡ C → P = 1 st ⁡ P 2 nd ⁡ P
8 6 7 mpancom ⊢ P ∈ ≃ 𝑐 ⁡ C → P = 1 st ⁡ P 2 nd ⁡ P