Metamath Proof Explorer

Theorem dfiso3

Description: Alternate definition of an isomorphism of a category as a section in both directions. (Contributed by AV, 11-Apr-2020)

Ref Expression
Hypotheses dfiso3.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
dfiso3.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
dfiso3.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
dfiso3.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
dfiso3.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
dfiso3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
dfiso3.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
dfiso3.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion dfiso3 ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( 𝑔 ( 𝑌 𝑆 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 𝑆 𝑌 ) 𝑔 ) ) )

Proof

Step Hyp Ref Expression
1 dfiso3.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 dfiso3.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 dfiso3.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
4 dfiso3.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
5 dfiso3.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
6 dfiso3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 dfiso3.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 dfiso3.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
9 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
10 eqid ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) = ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 )
11 eqid ⊢ ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) = ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 )
12 1 2 5 3 6 7 8 9 10 11 dfiso2 ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) ) )
13 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
14 5 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) → 𝐶 ∈ Cat )
15 7 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) → 𝑌 ∈ 𝐵 )
16 6 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) → 𝑋 ∈ 𝐵 )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) → 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) )
18 8 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
19 1 2 13 9 4 14 15 16 17 18 issect2 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) → ( 𝑔 ( 𝑌 𝑆 𝑋 ) 𝐹 ↔ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
20 1 2 13 9 4 14 16 15 18 17 issect2 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝑔 ↔ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
21 19 20 anbi12d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) → ( ( 𝑔 ( 𝑌 𝑆 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 𝑆 𝑌 ) 𝑔 ) ↔ ( ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
22 ancom ⊢ ( ( ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ∧ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
23 21 22 bitr2di ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ) → ( ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) ↔ ( 𝑔 ( 𝑌 𝑆 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 𝑆 𝑌 ) 𝑔 ) ) )
24 23 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) ↔ ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( 𝑔 ( 𝑌 𝑆 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 𝑆 𝑌 ) 𝑔 ) ) )
25 12 24 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ∃ 𝑔 ∈ ( 𝑌 𝐻 𝑋 ) ( 𝑔 ( 𝑌 𝑆 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 𝑆 𝑌 ) 𝑔 ) ) )