Metamath Proof Explorer

Theorem setcsect

Description: A section in the category of sets, written out. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcmon.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
setcmon.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
setcmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
setcmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
setcsect.n ⊢ 𝑆 = ( Sect ‘ 𝐶 )
Assertion setcsect ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 setcmon.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
2 setcmon.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 setcmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
4 setcmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
5 setcsect.n ⊢ 𝑆 = ( Sect ‘ 𝐶 )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
8 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
9 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
10 1 setccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
11 2 10 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
12 1 2 setcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐶 ) )
13 3 12 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
14 4 12 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
15 6 7 8 9 5 11 13 14 issect ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
16 1 2 7 3 4 elsetchom ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 : 𝑋 ⟶ 𝑌 ) )
17 1 2 7 4 3 elsetchom ⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ↔ 𝐺 : 𝑌 ⟶ 𝑋 ) )
18 16 17 anbi12d ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ) )
19 18 anbi1d ⊢ ( 𝜑 → ( ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
20 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ) → 𝑈 ∈ 𝑉 )
21 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ) → 𝑋 ∈ 𝑈 )
22 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ) → 𝑌 ∈ 𝑈 )
23 simprl ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
24 simprr ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ) → 𝐺 : 𝑌 ⟶ 𝑋 )
25 1 20 8 21 22 21 23 24 setcco ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )
26 1 9 2 3 setcid ⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) = ( I ↾ 𝑋 ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) = ( I ↾ 𝑋 ) )
28 25 27 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ) → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ↔ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) )
29 28 pm5.32da ⊢ ( 𝜑 → ( ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) ) )
30 19 29 bitrd ⊢ ( 𝜑 → ( ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) ) )
31 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
32 df-3an ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) ↔ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) )
33 30 31 32 3bitr4g ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) ) )
34 15 33 bitrd ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) ) )