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

Metamath Proof Explorer

Theorem termfucterm

Description: All functors between two terminal categories are isomorphisms. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses termfucterm.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
termfucterm.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
termfucterm.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
termfucterm.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
termfucterm.xt ⊢ ( 𝜑 → 𝑋 ∈ TermCat )
termfucterm.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
termfucterm.yt ⊢ ( 𝜑 → 𝑌 ∈ TermCat )
Assertion termfucterm ( 𝜑 → ( 𝑋 Func 𝑌 ) = ( 𝑋 𝐼 𝑌 ) )

Proof

Step Hyp Ref Expression
1 termfucterm.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2 termfucterm.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 termfucterm.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
4 termfucterm.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 termfucterm.xt ⊢ ( 𝜑 → 𝑋 ∈ TermCat )
6 termfucterm.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 termfucterm.yt ⊢ ( 𝜑 → 𝑌 ∈ TermCat )
8 1 2 4 6 5 termcciso ⊢ ( 𝜑 → ( 𝑌 ∈ TermCat ↔ 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ) )
9 7 8 mpbid ⊢ ( 𝜑 → 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 )
10 cicrcl2 ⊢ ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 → 𝐶 ∈ Cat )
11 9 10 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
12 3 2 11 4 6 cic ⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ∃ 𝑔 𝑔 ∈ ( 𝑋 𝐼 𝑌 ) ) )
13 9 12 mpbid ⊢ ( 𝜑 → ∃ 𝑔 𝑔 ∈ ( 𝑋 𝐼 𝑌 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 Func 𝑌 ) ) → ∃ 𝑔 𝑔 ∈ ( 𝑋 𝐼 𝑌 ) )
15 eqid ⊢ ( 𝑋 FuncCat 𝑌 ) = ( 𝑋 FuncCat 𝑌 )
16 5 termccd ⊢ ( 𝜑 → 𝑋 ∈ Cat )
17 15 16 7 fucterm ⊢ ( 𝜑 → ( 𝑋 FuncCat 𝑌 ) ∈ TermCat )
18 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 Func 𝑌 ) ) ∧ 𝑔 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝑋 FuncCat 𝑌 ) ∈ TermCat )
19 15 fucbas ⊢ ( 𝑋 Func 𝑌 ) = ( Base ‘ ( 𝑋 FuncCat 𝑌 ) )
20 simplr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 Func 𝑌 ) ) ∧ 𝑔 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑓 ∈ ( 𝑋 Func 𝑌 ) )
21 fullfunc ⊢ ( 𝑋 Full 𝑌 ) ⊆ ( 𝑋 Func 𝑌 )
22 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
23 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
24 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 Func 𝑌 ) ) ∧ 𝑔 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑔 ∈ ( 𝑋 𝐼 𝑌 ) )
25 1 22 23 3 24 catcisoi ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 Func 𝑌 ) ) ∧ 𝑔 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝑔 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1st ‘ 𝑔 ) : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) )
26 25 simpld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 Func 𝑌 ) ) ∧ 𝑔 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑔 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) )
27 26 elin1d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 Func 𝑌 ) ) ∧ 𝑔 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑔 ∈ ( 𝑋 Full 𝑌 ) )
28 21 27 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 Func 𝑌 ) ) ∧ 𝑔 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑔 ∈ ( 𝑋 Func 𝑌 ) )
29 18 19 20 28 termcbasmo ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 Func 𝑌 ) ) ∧ 𝑔 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑓 = 𝑔 )
30 29 24 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 Func 𝑌 ) ) ∧ 𝑔 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) )
31 14 30 exlimddv ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 Func 𝑌 ) ) → 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) )
32 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) )
33 1 22 23 3 32 catcisoi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝑓 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1st ‘ 𝑓 ) : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) )
34 33 simpld ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑓 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) )
35 34 elin1d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑓 ∈ ( 𝑋 Full 𝑌 ) )
36 21 35 sselid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑓 ∈ ( 𝑋 Func 𝑌 ) )
37 31 36 impbida ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 Func 𝑌 ) ↔ 𝑓 ∈ ( 𝑋 𝐼 𝑌 ) ) )
38 37 eqrdv ⊢ ( 𝜑 → ( 𝑋 Func 𝑌 ) = ( 𝑋 𝐼 𝑌 ) )