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

Metamath Proof Explorer

Theorem sectrcl

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

Ref Expression
Hypotheses sectrcl.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
sectrcl.f ⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
Assertion sectrcl ( 𝜑 → 𝐶 ∈ Cat )

Proof

Step Hyp Ref Expression
1 sectrcl.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
2 sectrcl.f ⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
3 df-br ⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑆 𝑌 ) )
4 df-ov ⊢ ( 𝑋 𝑆 𝑌 ) = ( 𝑆 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
5 4 eleq2i ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑆 𝑌 ) ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑆 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
6 3 5 bitri ⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑆 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
7 elfvne0 ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑆 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) → 𝑆 ≠ ∅ )
8 6 7 sylbi ⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 → 𝑆 ≠ ∅ )
9 1 neeq1i ⊢ ( 𝑆 ≠ ∅ ↔ ( Sect ‘ 𝐶 ) ≠ ∅ )
10 n0 ⊢ ( ( Sect ‘ 𝐶 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( Sect ‘ 𝐶 ) )
11 9 10 bitri ⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( Sect ‘ 𝐶 ) )
12 8 11 sylib ⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 → ∃ 𝑥 𝑥 ∈ ( Sect ‘ 𝐶 ) )
13 df-sect ⊢ Sect = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Hom ‘ 𝑐 ) / ℎ ] ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ) } ) )
14 13 mptrcl ⊢ ( 𝑥 ∈ ( Sect ‘ 𝐶 ) → 𝐶 ∈ Cat )
15 14 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ ( Sect ‘ 𝐶 ) → 𝐶 ∈ Cat )
16 2 12 15 3syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )