Metamath Proof Explorer

Theorem setc1onsubc

Description: Construct a category with one object and two morphisms and prove that category ( SetCat1o ) satisfies all conditions for a subcategory but the compatibility of identity morphisms, showing the necessity of the latter condition in defining a subcategory. Exercise 4A of Adamek p. 58. (Contributed by Zhi Wang, 6-Nov-2025)

Ref Expression
Hypotheses setc1onsubc.c ⊢ 𝐶 = { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } ⟩ }
setc1onsubc.x ⊢ · = ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) )
setc1onsubc.e ⊢ 𝐸 = ( SetCat ‘ 1o )
setc1onsubc.j ⊢ 𝐽 = ( Homf ‘ 𝐸 )
setc1onsubc.s ⊢ 𝑆 = 1o
setc1onsubc.h ⊢ 𝐻 = ( Homf ‘ 𝐶 )
setc1onsubc.i ⊢ 1 = ( Id ‘ 𝐶 )
setc1onsubc.d ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
Assertion setc1onsubc ( 𝐶 ∈ Cat ∧ 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat 𝐻 ∧ ¬ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) )

Proof

Step Hyp Ref Expression
1 setc1onsubc.c ⊢ 𝐶 = { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } ⟩ }
2 setc1onsubc.x ⊢ · = ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) )
3 setc1onsubc.e ⊢ 𝐸 = ( SetCat ‘ 1o )
4 setc1onsubc.j ⊢ 𝐽 = ( Homf ‘ 𝐸 )
5 setc1onsubc.s ⊢ 𝑆 = 1o
6 setc1onsubc.h ⊢ 𝐻 = ( Homf ‘ 𝐶 )
7 setc1onsubc.i ⊢ 1 = ( Id ‘ 𝐶 )
8 setc1onsubc.d ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
9 0ss ⊢ ∅ ⊆ 1o
10 1oex ⊢ 1o ∈ V
11 df2o3 ⊢ 2o = { ∅ , 1o }
12 1 11 2 incat ⊢ ( ( ∅ ⊆ 1o ∧ 1o ∈ V ) → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ { ∅ } ↦ 1o ) ) )
13 9 10 12 mp2an ⊢ ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ { ∅ } ↦ 1o ) )
14 13 simpli ⊢ 𝐶 ∈ Cat
15 3 setc1obas ⊢ 1o = ( Base ‘ 𝐸 )
16 5 15 eqtri ⊢ 𝑆 = ( Base ‘ 𝐸 )
17 4 16 homffn ⊢ 𝐽 Fn ( 𝑆 × 𝑆 )
18 ssid ⊢ { ∅ } ⊆ { ∅ }
19 snsspr1 ⊢ { ∅ } ⊆ { ∅ , 1o }
20 3 setc1ohomfval ⊢ { ⟨ ∅ , ∅ , 1o ⟩ } = ( Hom ‘ 𝐸 )
21 0lt1o ⊢ ∅ ∈ 1o
22 21 a1i ⊢ ( ⊤ → ∅ ∈ 1o )
23 4 15 20 22 22 homfval ⊢ ( ⊤ → ( ∅ 𝐽 ∅ ) = ( ∅ { ⟨ ∅ , ∅ , 1o ⟩ } ∅ ) )
24 23 mptru ⊢ ( ∅ 𝐽 ∅ ) = ( ∅ { ⟨ ∅ , ∅ , 1o ⟩ } ∅ )
25 10 ovsn2 ⊢ ( ∅ { ⟨ ∅ , ∅ , 1o ⟩ } ∅ ) = 1o
26 df1o2 ⊢ 1o = { ∅ }
27 24 25 26 3eqtri ⊢ ( ∅ 𝐽 ∅ ) = { ∅ }
28 snex ⊢ { ∅ } ∈ V
29 1 28 catbas ⊢ { ∅ } = ( Base ‘ 𝐶 )
30 snex ⊢ { ⟨ ∅ , ∅ , 2o ⟩ } ∈ V
31 1 30 cathomfval ⊢ { ⟨ ∅ , ∅ , 2o ⟩ } = ( Hom ‘ 𝐶 )
32 0ex ⊢ ∅ ∈ V
33 32 snid ⊢ ∅ ∈ { ∅ }
34 33 a1i ⊢ ( ⊤ → ∅ ∈ { ∅ } )
35 6 29 31 34 34 homfval ⊢ ( ⊤ → ( ∅ 𝐻 ∅ ) = ( ∅ { ⟨ ∅ , ∅ , 2o ⟩ } ∅ ) )
36 35 mptru ⊢ ( ∅ 𝐻 ∅ ) = ( ∅ { ⟨ ∅ , ∅ , 2o ⟩ } ∅ )
37 2oex ⊢ 2o ∈ V
38 37 ovsn2 ⊢ ( ∅ { ⟨ ∅ , ∅ , 2o ⟩ } ∅ ) = 2o
39 36 38 11 3eqtri ⊢ ( ∅ 𝐻 ∅ ) = { ∅ , 1o }
40 19 27 39 3sstr4i ⊢ ( ∅ 𝐽 ∅ ) ⊆ ( ∅ 𝐻 ∅ )
41 oveq1 ⊢ ( 𝑝 = ∅ → ( 𝑝 𝐽 𝑞 ) = ( ∅ 𝐽 𝑞 ) )
42 oveq1 ⊢ ( 𝑝 = ∅ → ( 𝑝 𝐻 𝑞 ) = ( ∅ 𝐻 𝑞 ) )
43 41 42 sseq12d ⊢ ( 𝑝 = ∅ → ( ( 𝑝 𝐽 𝑞 ) ⊆ ( 𝑝 𝐻 𝑞 ) ↔ ( ∅ 𝐽 𝑞 ) ⊆ ( ∅ 𝐻 𝑞 ) ) )
44 43 ralbidv ⊢ ( 𝑝 = ∅ → ( ∀ 𝑞 ∈ { ∅ } ( 𝑝 𝐽 𝑞 ) ⊆ ( 𝑝 𝐻 𝑞 ) ↔ ∀ 𝑞 ∈ { ∅ } ( ∅ 𝐽 𝑞 ) ⊆ ( ∅ 𝐻 𝑞 ) ) )
45 32 44 ralsn ⊢ ( ∀ 𝑝 ∈ { ∅ } ∀ 𝑞 ∈ { ∅ } ( 𝑝 𝐽 𝑞 ) ⊆ ( 𝑝 𝐻 𝑞 ) ↔ ∀ 𝑞 ∈ { ∅ } ( ∅ 𝐽 𝑞 ) ⊆ ( ∅ 𝐻 𝑞 ) )
46 oveq2 ⊢ ( 𝑞 = ∅ → ( ∅ 𝐽 𝑞 ) = ( ∅ 𝐽 ∅ ) )
47 oveq2 ⊢ ( 𝑞 = ∅ → ( ∅ 𝐻 𝑞 ) = ( ∅ 𝐻 ∅ ) )
48 46 47 sseq12d ⊢ ( 𝑞 = ∅ → ( ( ∅ 𝐽 𝑞 ) ⊆ ( ∅ 𝐻 𝑞 ) ↔ ( ∅ 𝐽 ∅ ) ⊆ ( ∅ 𝐻 ∅ ) ) )
49 32 48 ralsn ⊢ ( ∀ 𝑞 ∈ { ∅ } ( ∅ 𝐽 𝑞 ) ⊆ ( ∅ 𝐻 𝑞 ) ↔ ( ∅ 𝐽 ∅ ) ⊆ ( ∅ 𝐻 ∅ ) )
50 45 49 bitri ⊢ ( ∀ 𝑝 ∈ { ∅ } ∀ 𝑞 ∈ { ∅ } ( 𝑝 𝐽 𝑞 ) ⊆ ( 𝑝 𝐻 𝑞 ) ↔ ( ∅ 𝐽 ∅ ) ⊆ ( ∅ 𝐻 ∅ ) )
51 40 50 mpbir ⊢ ∀ 𝑝 ∈ { ∅ } ∀ 𝑞 ∈ { ∅ } ( 𝑝 𝐽 𝑞 ) ⊆ ( 𝑝 𝐻 𝑞 )
52 26 15 eqtr3i ⊢ { ∅ } = ( Base ‘ 𝐸 )
53 4 52 homffn ⊢ 𝐽 Fn ( { ∅ } × { ∅ } )
54 53 a1i ⊢ ( ⊤ → 𝐽 Fn ( { ∅ } × { ∅ } ) )
55 6 29 homffn ⊢ 𝐻 Fn ( { ∅ } × { ∅ } )
56 55 a1i ⊢ ( ⊤ → 𝐻 Fn ( { ∅ } × { ∅ } ) )
57 28 a1i ⊢ ( ⊤ → { ∅ } ∈ V )
58 54 56 57 isssc ⊢ ( ⊤ → ( 𝐽 ⊆cat 𝐻 ↔ ( { ∅ } ⊆ { ∅ } ∧ ∀ 𝑝 ∈ { ∅ } ∀ 𝑞 ∈ { ∅ } ( 𝑝 𝐽 𝑞 ) ⊆ ( 𝑝 𝐻 𝑞 ) ) ) )
59 58 mptru ⊢ ( 𝐽 ⊆cat 𝐻 ↔ ( { ∅ } ⊆ { ∅ } ∧ ∀ 𝑝 ∈ { ∅ } ∀ 𝑞 ∈ { ∅ } ( 𝑝 𝐽 𝑞 ) ⊆ ( 𝑝 𝐻 𝑞 ) ) )
60 18 51 59 mpbir2an ⊢ 𝐽 ⊆cat 𝐻
61 elirr ⊢ ¬ { ∅ } ∈ { ∅ }
62 5 26 eqtri ⊢ 𝑆 = { ∅ }
63 biid ⊢ ( ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
64 62 63 rexeqbii ⊢ ( ∃ 𝑥 ∈ 𝑆 ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ∃ 𝑥 ∈ { ∅ } ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
65 rexnal ⊢ ( ∃ 𝑥 ∈ 𝑆 ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
66 fveq2 ⊢ ( 𝑥 = ∅ → ( 1 ‘ 𝑥 ) = ( 1 ‘ ∅ ) )
67 26 a1i ⊢ ( 𝑦 = ∅ → 1o = { ∅ } )
68 13 simpri ⊢ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ { ∅ } ↦ 1o )
69 7 68 eqtri ⊢ 1 = ( 𝑦 ∈ { ∅ } ↦ 1o )
70 67 69 28 fvmpt ⊢ ( ∅ ∈ { ∅ } → ( 1 ‘ ∅ ) = { ∅ } )
71 33 70 ax-mp ⊢ ( 1 ‘ ∅ ) = { ∅ }
72 66 71 eqtrdi ⊢ ( 𝑥 = ∅ → ( 1 ‘ 𝑥 ) = { ∅ } )
73 oveq12 ⊢ ( ( 𝑥 = ∅ ∧ 𝑥 = ∅ ) → ( 𝑥 𝐽 𝑥 ) = ( ∅ 𝐽 ∅ ) )
74 73 anidms ⊢ ( 𝑥 = ∅ → ( 𝑥 𝐽 𝑥 ) = ( ∅ 𝐽 ∅ ) )
75 74 27 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝑥 𝐽 𝑥 ) = { ∅ } )
76 72 75 eleq12d ⊢ ( 𝑥 = ∅ → ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ { ∅ } ∈ { ∅ } ) )
77 76 notbid ⊢ ( 𝑥 = ∅ → ( ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ¬ { ∅ } ∈ { ∅ } ) )
78 32 77 rexsn ⊢ ( ∃ 𝑥 ∈ { ∅ } ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ¬ { ∅ } ∈ { ∅ } )
79 64 65 78 3bitr3ri ⊢ ( ¬ { ∅ } ∈ { ∅ } ↔ ¬ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
80 61 79 mpbi ⊢ ¬ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 )
81 setc1oterm ⊢ ( SetCat ‘ 1o ) ∈ TermCat
82 81 a1i ⊢ ( ⊤ → ( SetCat ‘ 1o ) ∈ TermCat )
83 82 termccd ⊢ ( ⊤ → ( SetCat ‘ 1o ) ∈ Cat )
84 83 mptru ⊢ ( SetCat ‘ 1o ) ∈ Cat
85 3 84 eqeltri ⊢ 𝐸 ∈ Cat
86 snex ⊢ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } ∈ V
87 1 86 catcofval ⊢ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } = ( comp ‘ 𝐶 )
88 3 setc1ocofval ⊢ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } = ( comp ‘ 𝐸 )
89 velsn ⊢ ( 𝑎 ∈ { ∅ } ↔ 𝑎 = ∅ )
90 velsn ⊢ ( 𝑏 ∈ { ∅ } ↔ 𝑏 = ∅ )
91 velsn ⊢ ( 𝑐 ∈ { ∅ } ↔ 𝑐 = ∅ )
92 89 90 91 3anbi123i ⊢ ( ( 𝑎 ∈ { ∅ } ∧ 𝑏 ∈ { ∅ } ∧ 𝑐 ∈ { ∅ } ) ↔ ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) )
93 92 anbi1i ⊢ ( ( ( 𝑎 ∈ { ∅ } ∧ 𝑏 ∈ { ∅ } ∧ 𝑐 ∈ { ∅ } ) ∧ ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ) ↔ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ) )
94 simp1 ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → 𝑎 = ∅ )
95 simp2 ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → 𝑏 = ∅ )
96 94 95 oveq12d ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑎 𝐽 𝑏 ) = ( ∅ 𝐽 ∅ ) )
97 96 27 eqtrdi ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑎 𝐽 𝑏 ) = { ∅ } )
98 97 eleq2d ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ↔ 𝑚 ∈ { ∅ } ) )
99 velsn ⊢ ( 𝑚 ∈ { ∅ } ↔ 𝑚 = ∅ )
100 98 99 bitrdi ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ↔ 𝑚 = ∅ ) )
101 simp3 ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → 𝑐 = ∅ )
102 95 101 oveq12d ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑏 𝐽 𝑐 ) = ( ∅ 𝐽 ∅ ) )
103 102 27 eqtrdi ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑏 𝐽 𝑐 ) = { ∅ } )
104 103 eleq2d ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ↔ 𝑛 ∈ { ∅ } ) )
105 velsn ⊢ ( 𝑛 ∈ { ∅ } ↔ 𝑛 = ∅ )
106 104 105 bitrdi ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ↔ 𝑛 = ∅ ) )
107 100 106 anbi12d ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ↔ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) )
108 107 pm5.32i ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ) ↔ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) )
109 93 108 bitri ⊢ ( ( ( 𝑎 ∈ { ∅ } ∧ 𝑏 ∈ { ∅ } ∧ 𝑐 ∈ { ∅ } ) ∧ ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ) ↔ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) )
110 32 prid1 ⊢ ∅ ∈ { ∅ , 1o }
111 110 11 eleqtrri ⊢ ∅ ∈ 2o
112 ineq12 ⊢ ( ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) → ( 𝑓 ∩ 𝑔 ) = ( ∅ ∩ ∅ ) )
113 0in ⊢ ( ∅ ∩ ∅ ) = ∅
114 112 113 eqtrdi ⊢ ( ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) → ( 𝑓 ∩ 𝑔 ) = ∅ )
115 114 2 32 ovmpoa ⊢ ( ( ∅ ∈ 2o ∧ ∅ ∈ 2o ) → ( ∅ · ∅ ) = ∅ )
116 111 111 115 mp2an ⊢ ( ∅ · ∅ ) = ∅
117 32 ovsn2 ⊢ ( ∅ { ⟨ ∅ , ∅ , ∅ ⟩ } ∅ ) = ∅
118 116 117 eqtr4i ⊢ ( ∅ · ∅ ) = ( ∅ { ⟨ ∅ , ∅ , ∅ ⟩ } ∅ )
119 simpl1 ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → 𝑎 = ∅ )
120 simpl2 ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → 𝑏 = ∅ )
121 119 120 opeq12d ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ∅ , ∅ ⟩ )
122 simpl3 ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → 𝑐 = ∅ )
123 121 122 oveq12d ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } 𝑐 ) = ( ⟨ ∅ , ∅ ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } ∅ ) )
124 37 37 mpoex ⊢ ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ∈ V
125 2 124 eqeltri ⊢ · ∈ V
126 125 ovsn2 ⊢ ( ⟨ ∅ , ∅ ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } ∅ ) = ·
127 123 126 eqtrdi ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } 𝑐 ) = · )
128 simprr ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → 𝑛 = ∅ )
129 simprl ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → 𝑚 = ∅ )
130 127 128 129 oveq123d ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } 𝑐 ) 𝑚 ) = ( ∅ · ∅ ) )
131 121 122 oveq12d ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } 𝑐 ) = ( ⟨ ∅ , ∅ ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ∅ ) )
132 snex ⊢ { ⟨ ∅ , ∅ , ∅ ⟩ } ∈ V
133 132 ovsn2 ⊢ ( ⟨ ∅ , ∅ ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ∅ ) = { ⟨ ∅ , ∅ , ∅ ⟩ }
134 131 133 eqtrdi ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } 𝑐 ) = { ⟨ ∅ , ∅ , ∅ ⟩ } )
135 134 128 129 oveq123d ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } 𝑐 ) 𝑚 ) = ( ∅ { ⟨ ∅ , ∅ , ∅ ⟩ } ∅ ) )
136 118 130 135 3eqtr4a ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } 𝑐 ) 𝑚 ) = ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } 𝑐 ) 𝑚 ) )
137 109 136 sylbi ⊢ ( ( ( 𝑎 ∈ { ∅ } ∧ 𝑏 ∈ { ∅ } ∧ 𝑐 ∈ { ∅ } ) ∧ ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } 𝑐 ) 𝑚 ) = ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } 𝑐 ) 𝑚 ) )
138 137 adantll ⊢ ( ( ( ⊤ ∧ ( 𝑎 ∈ { ∅ } ∧ 𝑏 ∈ { ∅ } ∧ 𝑐 ∈ { ∅ } ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } 𝑐 ) 𝑚 ) = ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } 𝑐 ) 𝑚 ) )
139 85 a1i ⊢ ( ⊤ → 𝐸 ∈ Cat )
140 18 a1i ⊢ ( ⊤ → { ∅ } ⊆ { ∅ } )
141 8 29 52 4 87 88 138 139 140 resccat ⊢ ( ⊤ → ( 𝐷 ∈ Cat ↔ 𝐸 ∈ Cat ) )
142 141 mptru ⊢ ( 𝐷 ∈ Cat ↔ 𝐸 ∈ Cat )
143 85 142 mpbir ⊢ 𝐷 ∈ Cat
144 60 80 143 3pm3.2i ⊢ ( 𝐽 ⊆cat 𝐻 ∧ ¬ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat )
145 14 17 144 3pm3.2i ⊢ ( 𝐶 ∈ Cat ∧ 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat 𝐻 ∧ ¬ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) )