Metamath Proof Explorer

Theorem fuconuniqlem

Description: Lemma for fuconuniq . (Contributed by Zhi Wang, 14-Sep-2026) (New usage is discouraged.)

Ref Expression
Hypotheses fuconuniq2.c ⊢ C = SetCat ⁡ 1 𝑜
fuconuniq2.e ⊢ E = Base ndx 2 𝑜 Hom ⁡ ndx m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ comp ⁡ ndx p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s
fuconuniq2.q ⊢ Q = C FuncCat E
fuconuniq2.l No typesetting found for |- L = ( <. C , C >. o.F E ) with typecode |-
fuconuniq.a ⊢ A = b ∈ 3 𝑜 ⟼ if b = 2 𝑜 2 𝑜 if b = ∅ 1 𝑜 ∅
fuconuniq.m ⊢ M = u ∈ 2 𝑜 , v ∈ 2 𝑜 ⟼ a ∈ u m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ v ⟼ A ⁡ a
fuconuniq.s ⊢ S = I ↾ 2 𝑜 M
fuconuniq.r ⊢ R = E FuncCat E
fuconuniq.o No typesetting found for |- .o. = ( <. R , Q >. curryF ( <. C , E >. o.F E ) ) with typecode |-
fuconuniq.k No typesetting found for |- K = ( ( 1st ` .o. ) ` S ) with typecode |-
fuconuniqlem.t ⊢ T = C FuncCat E × c C FuncCat C
fuconuniqlem.d ⊢ D = E Δ func C
fuconuniqlem.f ⊢ F = 1 st ⁡ D ⁡ ∅
fuconuniqlem.g ⊢ G = 1 st ⁡ D ⁡ 1 𝑜
fuconuniqlem.n ⊢ N = 1 𝑜 × ∅
Assertion fuconuniqlem ⊢ 1 st ⁡ L T Func Q 2 nd ⁡ K ∘ func L ∧ 2 nd ⁡ K ∘ func L ≠ 2 nd ⁡ L

Proof

Step Hyp Ref Expression
1 fuconuniq2.c ⊢ C = SetCat ⁡ 1 𝑜
2 fuconuniq2.e ⊢ E = Base ndx 2 𝑜 Hom ⁡ ndx m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ comp ⁡ ndx p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s
3 fuconuniq2.q ⊢ Q = C FuncCat E
4 fuconuniq2.l Could not format L = ( <. C , C >. o.F E ) : No typesetting found for |- L = ( <. C , C >. o.F E ) with typecode |-
5 fuconuniq.a ⊢ A = b ∈ 3 𝑜 ⟼ if b = 2 𝑜 2 𝑜 if b = ∅ 1 𝑜 ∅
6 fuconuniq.m ⊢ M = u ∈ 2 𝑜 , v ∈ 2 𝑜 ⟼ a ∈ u m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ v ⟼ A ⁡ a
7 fuconuniq.s ⊢ S = I ↾ 2 𝑜 M
8 fuconuniq.r ⊢ R = E FuncCat E
9 fuconuniq.o Could not format .o. = ( <. R , Q >. curryF ( <. C , E >. o.F E ) ) : No typesetting found for |- .o. = ( <. R , Q >. curryF ( <. C , E >. o.F E ) ) with typecode |-
10 fuconuniq.k Could not format K = ( ( 1st ` .o. ) ` S ) : No typesetting found for |- K = ( ( 1st ` .o. ) ` S ) with typecode |-
11 fuconuniqlem.t ⊢ T = C FuncCat E × c C FuncCat C
12 fuconuniqlem.d ⊢ D = E Δ func C
13 fuconuniqlem.f ⊢ F = 1 st ⁡ D ⁡ ∅
14 fuconuniqlem.g ⊢ G = 1 st ⁡ D ⁡ 1 𝑜
15 fuconuniqlem.n ⊢ N = 1 𝑜 × ∅
16 setc1oterm Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for |- ( SetCat ` 1o ) e. TermCat with typecode |-
17 1 16 eqeltri Could not format C e. TermCat : No typesetting found for |- C e. TermCat with typecode |-
18 17 a1i Could not format ( T. -> C e. TermCat ) : No typesetting found for |- ( T. -> C e. TermCat ) with typecode |-
19 18 termccatd ⊢ ⊤ → C ∈ Cat
20 2 par2catid ⊢ E ∈ Cat ∧ Id ⁡ E = y ∈ 2 𝑜 ⟼ 2 𝑜
21 20 simpli ⊢ E ∈ Cat
22 21 a1i ⊢ ⊤ → E ∈ Cat
23 2 5 6 parswapfunc ⊢ I ↾ 2 𝑜 M ∈ E Func E
24 7 23 eqeltri ⊢ S ∈ E Func E
25 24 a1i ⊢ ⊤ → S ∈ E Func E
26 mptresid ⊢ I ↾ 2 𝑜 = x ∈ 2 𝑜 ⟼ x
27 2oex ⊢ 2 𝑜 ∈ V
28 27 mptex ⊢ x ∈ 2 𝑜 ⟼ x ∈ V
29 26 28 eqeltri ⊢ I ↾ 2 𝑜 ∈ V
30 27 27 mpoex ⊢ u ∈ 2 𝑜 , v ∈ 2 𝑜 ⟼ a ∈ u m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ v ⟼ A ⁡ a ∈ V
31 6 30 eqeltri ⊢ M ∈ V
32 29 31 op1std ⊢ S = I ↾ 2 𝑜 M → 1 st ⁡ S = I ↾ 2 𝑜
33 7 32 mp1i ⊢ ⊤ → 1 st ⁡ S = I ↾ 2 𝑜
34 18 3 8 9 10 25 33 termcpostfix ⊢ ⊤ → K ∈ Q Func Q ∧ 1 st ⁡ K = I ↾ C Func E
35 34 simpld ⊢ ⊤ → K ∈ Q Func Q
36 34 simprd ⊢ ⊤ → 1 st ⁡ K = I ↾ C Func E
37 3 11 4 19 19 22 35 36 fucoaltfunc ⊢ ⊤ → 1 st ⁡ L T Func Q 2 nd ⁡ K ∘ func L
38 1 2 12 13 14 15 par2diag ⊢ F ∈ C Func E ∧ G ∈ C Func E ∧ N ∈ F C Nat E G ∧ N ⁡ ∅ = ∅ ∧ 1 st ⁡ F ⁡ ∅ = ∅ ∧ 1 st ⁡ G ⁡ ∅ = 1 𝑜
39 38 simp1i ⊢ F ∈ C Func E ∧ G ∈ C Func E
40 39 simpli ⊢ F ∈ C Func E
41 40 a1i ⊢ ⊤ → F ∈ C Func E
42 39 simpri ⊢ G ∈ C Func E
43 42 a1i ⊢ ⊤ → G ∈ C Func E
44 38 simp2i ⊢ N ∈ F C Nat E G ∧ N ⁡ ∅ = ∅
45 44 simpli ⊢ N ∈ F C Nat E G
46 45 a1i ⊢ ⊤ → N ∈ F C Nat E G
47 0lt1o ⊢ ∅ ∈ 1 𝑜
48 1 setc1obas ⊢ 1 𝑜 = Base C
49 47 48 eleqtri ⊢ ∅ ∈ Base C
50 49 a1i ⊢ ⊤ → ∅ ∈ Base C
51 3 8 9 25 19 10 41 43 46 50 postcof2 ⊢ ⊤ → F 2 nd ⁡ K G ⁡ N ⁡ ∅ = 1 st ⁡ F ⁡ ∅ 2 nd ⁡ S 1 st ⁡ G ⁡ ∅ ⁡ N ⁡ ∅
52 51 mptru ⊢ F 2 nd ⁡ K G ⁡ N ⁡ ∅ = 1 st ⁡ F ⁡ ∅ 2 nd ⁡ S 1 st ⁡ G ⁡ ∅ ⁡ N ⁡ ∅
53 38 simp3i ⊢ 1 st ⁡ F ⁡ ∅ = ∅ ∧ 1 st ⁡ G ⁡ ∅ = 1 𝑜
54 53 simpli ⊢ 1 st ⁡ F ⁡ ∅ = ∅
55 53 simpri ⊢ 1 st ⁡ G ⁡ ∅ = 1 𝑜
56 29 31 op2ndd ⊢ S = I ↾ 2 𝑜 M → 2 nd ⁡ S = M
57 7 56 ax-mp ⊢ 2 nd ⁡ S = M
58 54 55 57 oveq123i ⊢ 1 st ⁡ F ⁡ ∅ 2 nd ⁡ S 1 st ⁡ G ⁡ ∅ = ∅ M 1 𝑜
59 44 simpri ⊢ N ⁡ ∅ = ∅
60 58 59 fveq12i ⊢ 1 st ⁡ F ⁡ ∅ 2 nd ⁡ S 1 st ⁡ G ⁡ ∅ ⁡ N ⁡ ∅ = ∅ M 1 𝑜 ⁡ ∅
61 52 60 eqtri ⊢ F 2 nd ⁡ K G ⁡ N ⁡ ∅ = ∅ M 1 𝑜 ⁡ ∅
62 0ex ⊢ ∅ ∈ V
63 62 prid1 ⊢ ∅ ∈ ∅ 1 𝑜
64 df2o3 ⊢ 2 𝑜 = ∅ 1 𝑜
65 63 64 eleqtrri ⊢ ∅ ∈ 2 𝑜
66 65 a1i ⊢ ⊤ → ∅ ∈ 2 𝑜
67 1oelpr ⊢ 1 𝑜 ∈ ∅ 1 𝑜
68 67 64 eleqtrri ⊢ 1 𝑜 ∈ 2 𝑜
69 68 a1i ⊢ ⊤ → 1 𝑜 ∈ 2 𝑜
70 eqid ⊢ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ = m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅
71 70 par2hom ⊢ ∅ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ ∅ = 2 𝑜 ∧ 1 𝑜 m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ 1 𝑜 = 2 𝑜 ∧ ∅ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ 1 𝑜 = 2 𝑜 ∧ 1 𝑜 m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ ∅ = ∅
72 71 simp3i ⊢ ∅ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ 1 𝑜 = 2 𝑜 ∧ 1 𝑜 m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ ∅ = ∅
73 72 simpli ⊢ ∅ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ 1 𝑜 = 2 𝑜
74 65 73 eleqtrri ⊢ ∅ ∈ ∅ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ 1 𝑜
75 74 a1i ⊢ ⊤ → ∅ ∈ ∅ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ 1 𝑜
76 6 66 69 75 fvmpomptd ⊢ ⊤ → ∅ M 1 𝑜 ⁡ ∅ = A ⁡ ∅
77 76 mptru ⊢ ∅ M 1 𝑜 ⁡ ∅ = A ⁡ ∅
78 5 parswapprop ⊢ A ⁡ 2 𝑜 = 2 𝑜 ∧ ∀ t ∈ 2 𝑜 A ⁡ t ∈ 2 𝑜 ∧ A ⁡ ∅ = 1 𝑜
79 78 simp3i ⊢ A ⁡ ∅ = 1 𝑜
80 61 77 79 3eqtri ⊢ F 2 nd ⁡ K G ⁡ N ⁡ ∅ = 1 𝑜
81 1n0 ⊢ 1 𝑜 ≠ ∅
82 80 81 eqnetri ⊢ F 2 nd ⁡ K G ⁡ N ⁡ ∅ ≠ ∅
83 82 59 neeqtrri ⊢ F 2 nd ⁡ K G ⁡ N ⁡ ∅ ≠ N ⁡ ∅
84 fveq1 ⊢ F 2 nd ⁡ K G ⁡ N = N → F 2 nd ⁡ K G ⁡ N ⁡ ∅ = N ⁡ ∅
85 84 necon3i ⊢ F 2 nd ⁡ K G ⁡ N ⁡ ∅ ≠ N ⁡ ∅ → F 2 nd ⁡ K G ⁡ N ≠ N
86 83 85 mp1i ⊢ ⊤ → F 2 nd ⁡ K G ⁡ N ≠ N
87 3 4 19 22 35 41 43 46 86 fucoaltne ⊢ ⊤ → 2 nd ⁡ K ∘ func L ≠ 2 nd ⁡ L
88 37 87 jca ⊢ ⊤ → 1 st ⁡ L T Func Q 2 nd ⁡ K ∘ func L ∧ 2 nd ⁡ K ∘ func L ≠ 2 nd ⁡ L
89 88 mptru ⊢ 1 st ⁡ L T Func Q 2 nd ⁡ K ∘ func L ∧ 2 nd ⁡ K ∘ func L ≠ 2 nd ⁡ L