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	⊢ ( 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) → 𝑃 = ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) → 𝐶 ∈ dom ≃𝑐 )
2		cicfn	⊢ ≃𝑐 Fn Cat
3	2	fndmi	⊢ dom ≃𝑐 = Cat
4	1 3	eleqtrdi	⊢ ( 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) → 𝐶 ∈ Cat )
5		relcic	⊢ ( 𝐶 ∈ Cat → Rel ( ≃𝑐 ‘ 𝐶 ) )
6	4 5	syl	⊢ ( 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) → Rel ( ≃𝑐 ‘ 𝐶 ) )
7		1st2nd	⊢ ( ( Rel ( ≃𝑐 ‘ 𝐶 ) ∧ 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) ) → 𝑃 = ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ )
8	6 7	mpancom	⊢ ( 𝑃 ∈ ( ≃𝑐 ‘ 𝐶 ) → 𝑃 = ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ )