Theorem invrcl

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

	Ref	Expression
Hypotheses	invrcl.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
	invrcl.f	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 )
Assertion	invrcl	⊢ ( 𝜑 → 𝐶 ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		invrcl.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
2		invrcl.f	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 )
3		df-br	⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑁 𝑌 ) )
4		df-ov	⊢ ( 𝑋 𝑁 𝑌 ) = ( 𝑁 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
5	4	eleq2i	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑁 𝑌 ) ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑁 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
6	3 5	bitri	⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑁 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
7		elfvne0	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑁 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) → 𝑁 ≠ ∅ )
8	6 7	sylbi	⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 → 𝑁 ≠ ∅ )
9	1	neeq1i	⊢ ( 𝑁 ≠ ∅ ↔ ( Inv ‘ 𝐶 ) ≠ ∅ )
10		n0	⊢ ( ( Inv ‘ 𝐶 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( Inv ‘ 𝐶 ) )
11	9 10	bitri	⊢ ( 𝑁 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( Inv ‘ 𝐶 ) )
12	8 11	sylib	⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 → ∃ 𝑥 𝑥 ∈ ( Inv ‘ 𝐶 ) )
13		df-inv	⊢ Inv = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) ) )
14	13	mptrcl	⊢ ( 𝑥 ∈ ( Inv ‘ 𝐶 ) → 𝐶 ∈ Cat )
15	14	exlimiv	⊢ ( ∃ 𝑥 𝑥 ∈ ( Inv ‘ 𝐶 ) → 𝐶 ∈ Cat )
16	2 12 15	3syl	⊢ ( 𝜑 → 𝐶 ∈ Cat )