Theorem invrcl2

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

	Ref	Expression
Hypotheses	invrcl.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
	invrcl.f	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 )
	invrcl2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	invrcl2	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		invrcl.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
2		invrcl.f	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 )
3		invrcl2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		df-br	⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑁 𝑌 ) )
5	2 4	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑁 𝑌 ) )
6	1 2	invrcl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
7		eqid	⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
8	3 1 6 7	invffval	⊢ ( 𝜑 → 𝑁 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) )
9	8	oveqd	⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) 𝑌 ) )
10	5 9	eleqtrd	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) 𝑌 ) )
11		eqid	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) )
12	11	elmpocl	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
13	10 12	syl	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )