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

Metamath Proof Explorer

Theorem sectrcl2

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

Ref Expression
Hypotheses sectrcl.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
sectrcl.f ⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
sectrcl2.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion sectrcl2 ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sectrcl.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
2 sectrcl.f ⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
3 sectrcl2.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 df-br ⊢ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑆 𝑌 ) )
5 2 4 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑆 𝑌 ) )
6 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
7 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
8 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
9 1 2 sectrcl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
10 3 6 7 8 1 9 sectffval ⊢ ( 𝜑 → 𝑆 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) )
11 10 oveqd ⊢ ( 𝜑 → ( 𝑋 𝑆 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) 𝑌 ) )
12 5 11 eleqtrd ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) 𝑌 ) )
13 eqid ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } )
14 13 elmpocl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
15 12 14 syl ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )