Metamath Proof Explorer

Theorem setcinv

Description: An inverse in the category of sets is the converse operation. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcmon.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
setcmon.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
setcmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
setcmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
setcinv.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
Assertion setcinv ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 setcmon.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
2 setcmon.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 setcmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
4 setcmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
5 setcinv.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 1 setccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
8 2 7 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
9 1 2 setcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐶 ) )
10 3 9 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
11 4 9 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
12 eqid ⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
13 6 5 8 10 11 12 isinv ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ) )
14 1 2 3 4 12 setcsect ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) ) )
15 df-3an ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) ↔ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) )
16 14 15 bitrdi ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ↔ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) ) )
17 1 2 4 3 12 setcsect ⊢ ( 𝜑 → ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ↔ ( 𝐺 : 𝑌 ⟶ 𝑋 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) ) )
18 3ancoma ⊢ ( ( 𝐺 : 𝑌 ⟶ 𝑋 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) )
19 df-3an ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) ↔ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) )
20 18 19 bitri ⊢ ( ( 𝐺 : 𝑌 ⟶ 𝑋 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) ↔ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) )
21 17 20 bitrdi ⊢ ( 𝜑 → ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ↔ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) ) )
22 16 21 anbi12d ⊢ ( 𝜑 → ( ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ↔ ( ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) ∧ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) ) ) )
23 anandi ⊢ ( ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) ) ↔ ( ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) ∧ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) ) )
24 22 23 bitr4di ⊢ ( 𝜑 → ( ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ↔ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) ) ) )
25 fcof1o ⊢ ( ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ◡ 𝐹 = 𝐺 ) )
26 eqcom ⊢ ( ◡ 𝐹 = 𝐺 ↔ 𝐺 = ◡ 𝐹 )
27 26 anbi2i ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ◡ 𝐹 = 𝐺 ) ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) )
28 25 27 sylib ⊢ ( ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) )
29 28 ancom2s ⊢ ( ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) )
30 29 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) )
31 f1of ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
32 31 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
33 f1ocnv ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
34 33 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
35 f1oeq1 ⊢ ( 𝐺 = ◡ 𝐹 → ( 𝐺 : 𝑌 –1-1-onto→ 𝑋 ↔ ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) )
36 35 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐺 : 𝑌 –1-1-onto→ 𝑋 ↔ ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) )
37 34 36 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → 𝐺 : 𝑌 –1-1-onto→ 𝑋 )
38 f1of ⊢ ( 𝐺 : 𝑌 –1-1-onto→ 𝑋 → 𝐺 : 𝑌 ⟶ 𝑋 )
39 37 38 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → 𝐺 : 𝑌 ⟶ 𝑋 )
40 simprr ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → 𝐺 = ◡ 𝐹 )
41 40 coeq1d ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐺 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ 𝐹 ) )
42 f1ococnv1 ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝑋 ) )
43 42 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝑋 ) )
44 41 43 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) )
45 40 coeq2d ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∘ 𝐺 ) = ( 𝐹 ∘ ◡ 𝐹 ) )
46 f1ococnv2 ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ 𝑌 ) )
47 46 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ 𝑌 ) )
48 45 47 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) )
49 44 48 jca ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) )
50 32 39 49 jca31 ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) ) )
51 30 50 impbida ⊢ ( 𝜑 → ( ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) ∧ ( ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝑌 ) ) ) ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) )
52 13 24 51 3bitrd ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐺 = ◡ 𝐹 ) ) )