Theorem brcici

Description: Prove that two objects are isomorphic by an explicit isomorphism. (Contributed by AV, 4-Apr-2020)

	Ref	Expression
Hypotheses	cic.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
	cic.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	cic.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	cic.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	cic.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	cic.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
Assertion	brcici	⊢ ( 𝜑 → 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		cic.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
2		cic.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		cic.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		cic.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		cic.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		cic.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
7		eleq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) )
8	7	spcegv	⊢ ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) → ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ) )
9	6 6 8	sylc	⊢ ( 𝜑 → ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) )
10	1 2 3 4 5	cic	⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ) )
11	9 10	mpbird	⊢ ( 𝜑 → 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 )