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 1on ⊢ 1o ∈ On
62 26 61 eqeltrri ⊢ { ∅ } ∈ On
63 62 onirri ⊢ ¬ { ∅ } ∈ { ∅ }
64 5 26 eqtri ⊢ 𝑆 = { ∅ }
65 biid ⊢ ( ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
66 64 65 rexeqbii ⊢ ( ∃ 𝑥 ∈ 𝑆 ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ∃ 𝑥 ∈ { ∅ } ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
67 rexnal ⊢ ( ∃ 𝑥 ∈ 𝑆 ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
68 fveq2 ⊢ ( 𝑥 = ∅ → ( 1 ‘ 𝑥 ) = ( 1 ‘ ∅ ) )
69 26 a1i ⊢ ( 𝑦 = ∅ → 1o = { ∅ } )
70 13 simpri ⊢ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ { ∅ } ↦ 1o )
71 7 70 eqtri ⊢ 1 = ( 𝑦 ∈ { ∅ } ↦ 1o )
72 69 71 28 fvmpt ⊢ ( ∅ ∈ { ∅ } → ( 1 ‘ ∅ ) = { ∅ } )
73 33 72 ax-mp ⊢ ( 1 ‘ ∅ ) = { ∅ }
74 68 73 eqtrdi ⊢ ( 𝑥 = ∅ → ( 1 ‘ 𝑥 ) = { ∅ } )
75 oveq12 ⊢ ( ( 𝑥 = ∅ ∧ 𝑥 = ∅ ) → ( 𝑥 𝐽 𝑥 ) = ( ∅ 𝐽 ∅ ) )
76 75 anidms ⊢ ( 𝑥 = ∅ → ( 𝑥 𝐽 𝑥 ) = ( ∅ 𝐽 ∅ ) )
77 76 27 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝑥 𝐽 𝑥 ) = { ∅ } )
78 74 77 eleq12d ⊢ ( 𝑥 = ∅ → ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ { ∅ } ∈ { ∅ } ) )
79 78 notbid ⊢ ( 𝑥 = ∅ → ( ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ¬ { ∅ } ∈ { ∅ } ) )
80 32 79 rexsn ⊢ ( ∃ 𝑥 ∈ { ∅ } ¬ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ¬ { ∅ } ∈ { ∅ } )
81 66 67 80 3bitr3ri ⊢ ( ¬ { ∅ } ∈ { ∅ } ↔ ¬ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
82 63 81 mpbi ⊢ ¬ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 )
83 setc1oterm ⊢ ( SetCat ‘ 1o ) ∈ TermCat
84 83 a1i ⊢ ( ⊤ → ( SetCat ‘ 1o ) ∈ TermCat )
85 84 termccd ⊢ ( ⊤ → ( SetCat ‘ 1o ) ∈ Cat )
86 85 mptru ⊢ ( SetCat ‘ 1o ) ∈ Cat
87 3 86 eqeltri ⊢ 𝐸 ∈ Cat
88 snex ⊢ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } ∈ V
89 1 88 catcofval ⊢ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } = ( comp ‘ 𝐶 )
90 3 setc1ocofval ⊢ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } = ( comp ‘ 𝐸 )
91 velsn ⊢ ( 𝑎 ∈ { ∅ } ↔ 𝑎 = ∅ )
92 velsn ⊢ ( 𝑏 ∈ { ∅ } ↔ 𝑏 = ∅ )
93 velsn ⊢ ( 𝑐 ∈ { ∅ } ↔ 𝑐 = ∅ )
94 91 92 93 3anbi123i ⊢ ( ( 𝑎 ∈ { ∅ } ∧ 𝑏 ∈ { ∅ } ∧ 𝑐 ∈ { ∅ } ) ↔ ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) )
95 94 anbi1i ⊢ ( ( ( 𝑎 ∈ { ∅ } ∧ 𝑏 ∈ { ∅ } ∧ 𝑐 ∈ { ∅ } ) ∧ ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ) ↔ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ) )
96 simp1 ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → 𝑎 = ∅ )
97 simp2 ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → 𝑏 = ∅ )
98 96 97 oveq12d ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑎 𝐽 𝑏 ) = ( ∅ 𝐽 ∅ ) )
99 98 27 eqtrdi ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑎 𝐽 𝑏 ) = { ∅ } )
100 99 eleq2d ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ↔ 𝑚 ∈ { ∅ } ) )
101 velsn ⊢ ( 𝑚 ∈ { ∅ } ↔ 𝑚 = ∅ )
102 100 101 bitrdi ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ↔ 𝑚 = ∅ ) )
103 simp3 ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → 𝑐 = ∅ )
104 97 103 oveq12d ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑏 𝐽 𝑐 ) = ( ∅ 𝐽 ∅ ) )
105 104 27 eqtrdi ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑏 𝐽 𝑐 ) = { ∅ } )
106 105 eleq2d ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ↔ 𝑛 ∈ { ∅ } ) )
107 velsn ⊢ ( 𝑛 ∈ { ∅ } ↔ 𝑛 = ∅ )
108 106 107 bitrdi ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ↔ 𝑛 = ∅ ) )
109 102 108 anbi12d ⊢ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) → ( ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ↔ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) )
110 109 pm5.32i ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ) ↔ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) )
111 95 110 bitri ⊢ ( ( ( 𝑎 ∈ { ∅ } ∧ 𝑏 ∈ { ∅ } ∧ 𝑐 ∈ { ∅ } ) ∧ ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ) ↔ ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) )
112 32 prid1 ⊢ ∅ ∈ { ∅ , 1o }
113 112 11 eleqtrri ⊢ ∅ ∈ 2o
114 ineq12 ⊢ ( ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) → ( 𝑓 ∩ 𝑔 ) = ( ∅ ∩ ∅ ) )
115 0in ⊢ ( ∅ ∩ ∅ ) = ∅
116 114 115 eqtrdi ⊢ ( ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) → ( 𝑓 ∩ 𝑔 ) = ∅ )
117 116 2 32 ovmpoa ⊢ ( ( ∅ ∈ 2o ∧ ∅ ∈ 2o ) → ( ∅ · ∅ ) = ∅ )
118 113 113 117 mp2an ⊢ ( ∅ · ∅ ) = ∅
119 32 ovsn2 ⊢ ( ∅ { ⟨ ∅ , ∅ , ∅ ⟩ } ∅ ) = ∅
120 118 119 eqtr4i ⊢ ( ∅ · ∅ ) = ( ∅ { ⟨ ∅ , ∅ , ∅ ⟩ } ∅ )
121 simpl1 ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → 𝑎 = ∅ )
122 simpl2 ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → 𝑏 = ∅ )
123 121 122 opeq12d ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ∅ , ∅ ⟩ )
124 simpl3 ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → 𝑐 = ∅ )
125 123 124 oveq12d ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } 𝑐 ) = ( ⟨ ∅ , ∅ ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } ∅ ) )
126 37 37 mpoex ⊢ ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ∈ V
127 2 126 eqeltri ⊢ · ∈ V
128 127 ovsn2 ⊢ ( ⟨ ∅ , ∅ ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } ∅ ) = ·
129 125 128 eqtrdi ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } 𝑐 ) = · )
130 simprr ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → 𝑛 = ∅ )
131 simprl ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → 𝑚 = ∅ )
132 129 130 131 oveq123d ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } 𝑐 ) 𝑚 ) = ( ∅ · ∅ ) )
133 123 124 oveq12d ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } 𝑐 ) = ( ⟨ ∅ , ∅ ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ∅ ) )
134 snex ⊢ { ⟨ ∅ , ∅ , ∅ ⟩ } ∈ V
135 134 ovsn2 ⊢ ( ⟨ ∅ , ∅ ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ∅ ) = { ⟨ ∅ , ∅ , ∅ ⟩ }
136 133 135 eqtrdi ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } 𝑐 ) = { ⟨ ∅ , ∅ , ∅ ⟩ } )
137 136 130 131 oveq123d ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } 𝑐 ) 𝑚 ) = ( ∅ { ⟨ ∅ , ∅ , ∅ ⟩ } ∅ ) )
138 120 132 137 3eqtr4a ⊢ ( ( ( 𝑎 = ∅ ∧ 𝑏 = ∅ ∧ 𝑐 = ∅ ) ∧ ( 𝑚 = ∅ ∧ 𝑛 = ∅ ) ) → ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } 𝑐 ) 𝑚 ) = ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } 𝑐 ) 𝑚 ) )
139 111 138 sylbi ⊢ ( ( ( 𝑎 ∈ { ∅ } ∧ 𝑏 ∈ { ∅ } ∧ 𝑐 ∈ { ∅ } ) ∧ ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } 𝑐 ) 𝑚 ) = ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } 𝑐 ) 𝑚 ) )
140 139 adantll ⊢ ( ( ( ⊤ ∧ ( 𝑎 ∈ { ∅ } ∧ 𝑏 ∈ { ∅ } ∧ 𝑐 ∈ { ∅ } ) ) ∧ ( 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑛 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , · ⟩ } 𝑐 ) 𝑚 ) = ( 𝑛 ( ⟨ 𝑎 , 𝑏 ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } 𝑐 ) 𝑚 ) )
141 87 a1i ⊢ ( ⊤ → 𝐸 ∈ Cat )
142 18 a1i ⊢ ( ⊤ → { ∅ } ⊆ { ∅ } )
143 8 29 52 4 89 90 140 141 142 resccat ⊢ ( ⊤ → ( 𝐷 ∈ Cat ↔ 𝐸 ∈ Cat ) )
144 143 mptru ⊢ ( 𝐷 ∈ Cat ↔ 𝐸 ∈ Cat )
145 87 144 mpbir ⊢ 𝐷 ∈ Cat
146 60 82 145 3pm3.2i ⊢ ( 𝐽 ⊆cat 𝐻 ∧ ¬ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat )
147 14 17 146 3pm3.2i ⊢ ( 𝐶 ∈ Cat ∧ 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat 𝐻 ∧ ¬ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) )