Theorem isorcl2

Description: Reverse closure for isomorphism relations. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	isorcl.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
	isorcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
	isorcl2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	isorcl2	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		isorcl.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
2		isorcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
3		isorcl2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		eqid	⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
5	1 2	isorcl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
6	3 4 5 1	isofval2	⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ dom ( 𝑥 ( Inv ‘ 𝐶 ) 𝑦 ) ) )
7	6	oveqd	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ dom ( 𝑥 ( Inv ‘ 𝐶 ) 𝑦 ) ) 𝑌 ) )
8	2 7	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ dom ( 𝑥 ( Inv ‘ 𝐶 ) 𝑦 ) ) 𝑌 ) )
9		eqid	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ dom ( 𝑥 ( Inv ‘ 𝐶 ) 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ dom ( 𝑥 ( Inv ‘ 𝐶 ) 𝑦 ) )
10	9	elmpocl	⊢ ( 𝐹 ∈ ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ dom ( 𝑥 ( Inv ‘ 𝐶 ) 𝑦 ) ) 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
11	8 10	syl	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )