Metamath Proof Explorer

Theorem invrcl

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

Ref Expression
Hypotheses invrcl.n ⊢ N = Inv ⁡ C
invrcl.f ⊢ φ → F X N Y G
Assertion invrcl ⊢ φ → C ∈ Cat

Proof

Step Hyp Ref Expression
1 invrcl.n ⊢ N = Inv ⁡ C
2 invrcl.f ⊢ φ → F X N Y G
3 df-br ⊢ F X N Y G ↔ F G ∈ X N Y
4 df-ov ⊢ X N Y = N ⁡ X Y
5 4 eleq2i ⊢ F G ∈ X N Y ↔ F G ∈ N ⁡ X Y
6 3 5 bitri ⊢ F X N Y G ↔ F G ∈ N ⁡ X Y
7 elfvne0 ⊢ F G ∈ N ⁡ X Y → N ≠ ∅
8 6 7 sylbi ⊢ F X N Y G → N ≠ ∅
9 1 neeq1i ⊢ N ≠ ∅ ↔ Inv ⁡ C ≠ ∅
10 n0 ⊢ Inv ⁡ C ≠ ∅ ↔ ∃ x x ∈ Inv ⁡ C
11 9 10 bitri ⊢ N ≠ ∅ ↔ ∃ x x ∈ Inv ⁡ C
12 8 11 sylib ⊢ F X N Y G → ∃ x x ∈ Inv ⁡ C
13 df-inv ⊢ Inv = c ∈ Cat ⟼ x ∈ Base c , y ∈ Base c ⟼ x Sect ⁡ c y ∩ y Sect ⁡ c x -1
14 13 mptrcl ⊢ x ∈ Inv ⁡ C → C ∈ Cat
15 14 exlimiv ⊢ ∃ x x ∈ Inv ⁡ C → C ∈ Cat
16 2 12 15 3syl ⊢ φ → C ∈ Cat