This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )