Metamath Proof Explorer

Theorem 2arwcat

Description: The condition for a structure with at most one object and at most two morphisms being a category. "2arwcat.2" to "2arwcat.5" are also necessary conditions if X , .0. , and .1. are all sets, due to catlid , catrid , and catcocl . (Contributed by Zhi Wang, 5-Nov-2025)

Ref Expression
Hypotheses 2arwcat.b ⊢ ( 𝜑 → { 𝑋 } = ( Base ‘ 𝐶 ) )
2arwcat.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
2arwcat.x ⊢ ( 𝜑 → · = ( comp ‘ 𝐶 ) )
2arwcat.1 ⊢ ( 𝑋 𝐻 𝑋 ) = { 0 , 1 }
2arwcat.2 ⊢ ( 𝜑 → ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) = 1 )
2arwcat.3 ⊢ ( 𝜑 → ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) = 0 )
2arwcat.4 ⊢ ( 𝜑 → ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) = 0 )
2arwcat.5 ⊢ ( 𝜑 → ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) ∈ { 0 , 1 } )
Assertion 2arwcat ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ { 𝑋 } ↦ 1 ) ) )

Proof

Step Hyp Ref Expression
1 2arwcat.b ⊢ ( 𝜑 → { 𝑋 } = ( Base ‘ 𝐶 ) )
2 2arwcat.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
3 2arwcat.x ⊢ ( 𝜑 → · = ( comp ‘ 𝐶 ) )
4 2arwcat.1 ⊢ ( 𝑋 𝐻 𝑋 ) = { 0 , 1 }
5 2arwcat.2 ⊢ ( 𝜑 → ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) = 1 )
6 2arwcat.3 ⊢ ( 𝜑 → ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) = 0 )
7 2arwcat.4 ⊢ ( 𝜑 → ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) = 0 )
8 2arwcat.5 ⊢ ( 𝜑 → ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) ∈ { 0 , 1 } )
9 ovex ⊢ ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) ∈ V
10 5 9 eqeltrrdi ⊢ ( 𝜑 → 1 ∈ V )
11 prid2g ⊢ ( 1 ∈ V → 1 ∈ { 0 , 1 } )
12 10 11 syl ⊢ ( 𝜑 → 1 ∈ { 0 , 1 } )
13 12 4 eleqtrrdi ⊢ ( 𝜑 → 1 ∈ ( 𝑋 𝐻 𝑋 ) )
14 df-ov ⊢ ( 𝑋 𝐻 𝑋 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑋 ⟩ )
15 2 fveq1d ⊢ ( 𝜑 → ( 𝐻 ‘ ⟨ 𝑋 , 𝑋 ⟩ ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ 𝑋 , 𝑋 ⟩ ) )
16 14 15 eqtrid ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑋 ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ 𝑋 , 𝑋 ⟩ ) )
17 13 16 eleqtrd ⊢ ( 𝜑 → 1 ∈ ( ( Hom ‘ 𝐶 ) ‘ ⟨ 𝑋 , 𝑋 ⟩ ) )
18 elfv2ex ⊢ ( 1 ∈ ( ( Hom ‘ 𝐶 ) ‘ ⟨ 𝑋 , 𝑋 ⟩ ) → 𝐶 ∈ V )
19 17 18 syl ⊢ ( 𝜑 → 𝐶 ∈ V )
20 4 2arwcatlem1 ⊢ ( ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ↔ ( ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ { 𝑋 } ) ∧ ( 𝑧 ∈ { 𝑋 } ∧ 𝑤 ∈ { 𝑋 } ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
21 12 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑋 } ) → 1 ∈ { 0 , 1 } )
22 velsn ⊢ ( 𝑦 ∈ { 𝑋 } ↔ 𝑦 = 𝑋 )
23 id ⊢ ( 𝑦 = 𝑋 → 𝑦 = 𝑋 )
24 23 23 oveq12d ⊢ ( 𝑦 = 𝑋 → ( 𝑦 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑋 ) )
25 24 4 eqtrdi ⊢ ( 𝑦 = 𝑋 → ( 𝑦 𝐻 𝑦 ) = { 0 , 1 } )
26 22 25 sylbi ⊢ ( 𝑦 ∈ { 𝑋 } → ( 𝑦 𝐻 𝑦 ) = { 0 , 1 } )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑋 } ) → ( 𝑦 𝐻 𝑦 ) = { 0 , 1 } )
28 21 27 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑋 } ) → 1 ∈ ( 𝑦 𝐻 𝑦 ) )
29 simprll ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) )
30 29 simpld ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → 𝑥 = 𝑋 )
31 29 simprd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → 𝑦 = 𝑋 )
32 simprr1 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑓 = 0 ∨ 𝑓 = 1 ) )
33 5 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) = 1 )
34 6 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) = 0 )
35 30 31 31 32 33 34 2arwcatlem2 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 )
36 simprlr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) )
37 36 simpld ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → 𝑧 = 𝑋 )
38 simprr2 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑔 = 0 ∨ 𝑔 = 1 ) )
39 7 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) = 0 )
40 31 31 37 38 33 39 2arwcatlem3 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 )
41 8 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) ∈ { 0 , 1 } )
42 30 31 37 32 33 39 34 41 38 2arwcatlem4 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ { 0 , 1 } )
43 30 37 oveq12d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑋 𝐻 𝑋 ) )
44 43 4 eqtrdi ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑥 𝐻 𝑧 ) = { 0 , 1 } )
45 42 44 eleqtrrd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
46 6 7 8 2arwcatlem5 ⊢ ( 𝜑 → ( ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) = ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) ) )
47 46 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 0 ) → ( ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) = ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) ) )
48 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 0 ) → 𝑘 = 0 )
49 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 0 ) → 𝑔 = 0 )
50 48 49 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 0 ) → ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) = ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) )
51 simpr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) → 𝑓 = 0 )
52 51 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 0 ) → 𝑓 = 0 )
53 50 52 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 0 ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) )
54 49 52 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 0 ) → ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) )
55 48 54 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 0 ) → ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) = ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 0 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 0 ) ) )
56 47 53 55 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 0 ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) )
57 eqidd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → 𝑋 = 𝑋 )
58 30 31 opeq12d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑋 ⟩ )
59 58 37 oveq12d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) = ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) )
60 59 oveqd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) )
61 60 42 eqeltrrd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ∈ { 0 , 1 } )
62 ovex ⊢ ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ∈ V
63 62 elpr ⊢ ( ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ∈ { 0 , 1 } ↔ ( ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 0 ∨ ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 1 ) )
64 61 63 sylib ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 0 ∨ ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 1 ) )
65 57 57 57 64 33 34 2arwcatlem2 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) = ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) )
66 65 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 1 ) → ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) = ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) )
67 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 1 ) → 𝑘 = 1 )
68 67 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 1 ) → ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) = ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) )
69 67 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 1 ) → ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) = ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) )
70 57 57 57 38 33 34 2arwcatlem2 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) = 𝑔 )
71 70 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 1 ) → ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) = 𝑔 )
72 69 71 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 1 ) → ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) = 𝑔 )
73 72 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 1 ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) )
74 66 68 73 3eqtr4rd ⊢ ( ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) ∧ 𝑘 = 1 ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) )
75 simprr3 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑘 = 0 ∨ 𝑘 = 1 ) )
76 75 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) → ( 𝑘 = 0 ∨ 𝑘 = 1 ) )
77 56 74 76 mpjaodan ⊢ ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 0 ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) )
78 simpr ⊢ ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 1 ) → 𝑔 = 1 )
79 78 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 1 ) → ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) )
80 57 57 57 75 33 39 2arwcatlem3 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) = 𝑘 )
81 80 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 1 ) → ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) = 𝑘 )
82 79 81 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 1 ) → ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) = 𝑘 )
83 82 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 1 ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) )
84 78 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 1 ) → ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) )
85 57 57 57 32 33 34 2arwcatlem2 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑓 )
86 85 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 1 ) → ( 1 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑓 )
87 84 86 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 1 ) → ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑓 )
88 87 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 1 ) → ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) )
89 83 88 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) ∧ 𝑔 = 1 ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) )
90 38 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) → ( 𝑔 = 0 ∨ 𝑔 = 1 ) )
91 77 89 90 mpjaodan ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 0 ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) )
92 57 57 57 38 33 39 34 41 75 2arwcatlem4 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ∈ { 0 , 1 } )
93 ovex ⊢ ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ∈ V
94 93 elpr ⊢ ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ∈ { 0 , 1 } ↔ ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) = 0 ∨ ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) = 1 ) )
95 92 94 sylib ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) = 0 ∨ ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) = 1 ) )
96 57 57 57 95 33 39 2arwcatlem3 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) )
97 96 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 1 ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) )
98 simpr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 1 ) → 𝑓 = 1 )
99 98 oveq2d ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 1 ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) )
100 98 oveq2d ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 1 ) → ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) )
101 57 57 57 38 33 39 2arwcatlem3 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) = 𝑔 )
102 101 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 1 ) → ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 1 ) = 𝑔 )
103 100 102 eqtrd ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 1 ) → ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑔 )
104 103 oveq2d ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 1 ) → ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) )
105 97 99 104 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) ∧ 𝑓 = 1 ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) )
106 91 105 32 mpjaodan ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) )
107 36 simprd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → 𝑤 = 𝑋 )
108 58 107 oveq12d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) = ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) )
109 31 37 opeq12d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑋 , 𝑋 ⟩ )
110 109 107 oveq12d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) = ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) )
111 110 oveqd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) )
112 eqidd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → 𝑓 = 𝑓 )
113 108 111 112 oveq123d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑔 ) ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) )
114 30 37 opeq12d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑋 , 𝑋 ⟩ )
115 114 107 oveq12d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) = ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) )
116 eqidd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → 𝑘 = 𝑘 )
117 115 116 60 oveq123d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) = ( 𝑘 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) ( 𝑔 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) ) )
118 106 113 117 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) )
119 1 2 3 19 20 28 35 40 45 118 iscatd2 ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ { 𝑋 } ↦ 1 ) ) )