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

Metamath Proof Explorer

Theorem invrcl2

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

Ref Expression
Hypotheses invrcl.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
invrcl.f ⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 )
invrcl2.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion invrcl2 ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 invrcl.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
2 invrcl.f ⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 )
3 invrcl2.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 df-br ⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑁 𝑌 ) )
5 2 4 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 𝑁 𝑌 ) )
6 1 2 invrcl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
7 eqid ⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
8 3 1 6 7 invffval ⊢ ( 𝜑 → 𝑁 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) )
9 8 oveqd ⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) 𝑌 ) )
10 5 9 eleqtrd ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) 𝑌 ) )
11 eqid ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) )
12 11 elmpocl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
13 10 12 syl ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )