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

Metamath Proof Explorer

Theorem isisod

Description: The predicate "is an isomorphism" (deduction form). (Contributed by Zhi Wang, 16-Sep-2025)

Ref Expression
Hypotheses isisod.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
isisod.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
isisod.o ⊢ · = ( comp ‘ 𝐶 )
isisod.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
isisod.1 ⊢ 1 = ( Id ‘ 𝐶 )
isisod.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
isisod.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
isisod.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
isisod.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
isisod.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) )
isisod.gf ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) )
isisod.fg ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 1 ‘ 𝑌 ) )
Assertion isisod ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )

Proof

Step Hyp Ref Expression
1 isisod.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 isisod.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 isisod.o ⊢ · = ( comp ‘ 𝐶 )
4 isisod.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
5 isisod.1 ⊢ 1 = ( Id ‘ 𝐶 )
6 isisod.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
7 isisod.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 isisod.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 isisod.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
10 isisod.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) )
11 isisod.gf ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) )
12 isisod.fg ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 1 ‘ 𝑌 ) )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
14 13 oveq1d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) )
15 14 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ↔ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ) )
16 13 oveq2d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) )
17 16 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 1 ‘ 𝑌 ) ↔ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 1 ‘ 𝑌 ) ) )
18 15 17 anbi12d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 1 ‘ 𝑌 ) ) ↔ ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 1 ‘ 𝑌 ) ) ) )
19 10 18 rspcedv ⊢ ( 𝜑 → ( ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) 𝐺 ) = ( 1 ‘ 𝑌 ) ) → ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 1 ‘ 𝑌 ) ) ) )
20 11 12 19 mp2and ⊢ ( 𝜑 → ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 1 ‘ 𝑌 ) ) )
21 3 oveqi ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) = ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 )
22 3 oveqi ⊢ ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) = ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 )
23 1 2 6 4 7 8 9 5 21 22 dfiso2 ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 1 ‘ 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ · 𝑌 ) 𝑔 ) = ( 1 ‘ 𝑌 ) ) ) )
24 20 23 mpbird ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )