Metamath Proof Explorer

Theorem arweuthinc

Description: If a structure has a unique disjointified arrow, then the structure is a thin category. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Assertion arweuthinc ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → 𝐶 ∈ ThinCat )

Proof

Step Hyp Ref Expression
1 eqidd ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 ) )
2 eqidd ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
3 eqeq1 ⊢ ( 𝑎 = ⟨ 𝑥 , 𝑦 , 𝑓 ⟩ → ( 𝑎 = 𝑏 ↔ ⟨ 𝑥 , 𝑦 , 𝑓 ⟩ = 𝑏 ) )
4 eqeq2 ⊢ ( 𝑏 = ⟨ 𝑥 , 𝑦 , 𝑔 ⟩ → ( ⟨ 𝑥 , 𝑦 , 𝑓 ⟩ = 𝑏 ↔ ⟨ 𝑥 , 𝑦 , 𝑓 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑔 ⟩ ) )
5 eumo ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ∃* 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) )
6 5 ad2antrr ⊢ ( ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ∃* 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) )
7 moel ⊢ ( ∃* 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ↔ ∀ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∀ 𝑏 ∈ ( Arrow ‘ 𝐶 ) 𝑎 = 𝑏 )
8 6 7 sylib ⊢ ( ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ∀ 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∀ 𝑏 ∈ ( Arrow ‘ 𝐶 ) 𝑎 = 𝑏 )
9 eqid ⊢ ( Arrow ‘ 𝐶 ) = ( Arrow ‘ 𝐶 )
10 eqid ⊢ ( Homa ‘ 𝐶 ) = ( Homa ‘ 𝐶 )
11 9 10 homarw ⊢ ( 𝑥 ( Homa ‘ 𝐶 ) 𝑦 ) ⊆ ( Arrow ‘ 𝐶 )
12 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
13 euex ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → ∃ 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) )
14 9 arwrcl ⊢ ( 𝑎 ∈ ( Arrow ‘ 𝐶 ) → 𝐶 ∈ Cat )
15 14 exlimiv ⊢ ( ∃ 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → 𝐶 ∈ Cat )
16 13 15 syl ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → 𝐶 ∈ Cat )
17 16 ad2antrr ⊢ ( ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝐶 ∈ Cat )
18 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
19 simplrl ⊢ ( ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
20 simplrr ⊢ ( ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
21 simprl ⊢ ( ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
22 10 12 17 18 19 20 21 elhomai2 ⊢ ( ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ⟨ 𝑥 , 𝑦 , 𝑓 ⟩ ∈ ( 𝑥 ( Homa ‘ 𝐶 ) 𝑦 ) )
23 11 22 sselid ⊢ ( ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ⟨ 𝑥 , 𝑦 , 𝑓 ⟩ ∈ ( Arrow ‘ 𝐶 ) )
24 simprr ⊢ ( ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
25 10 12 17 18 19 20 24 elhomai2 ⊢ ( ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ⟨ 𝑥 , 𝑦 , 𝑔 ⟩ ∈ ( 𝑥 ( Homa ‘ 𝐶 ) 𝑦 ) )
26 11 25 sselid ⊢ ( ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ⟨ 𝑥 , 𝑦 , 𝑔 ⟩ ∈ ( Arrow ‘ 𝐶 ) )
27 3 4 8 23 26 rspc2dv ⊢ ( ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ⟨ 𝑥 , 𝑦 , 𝑓 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑔 ⟩ )
28 vex ⊢ 𝑥 ∈ V
29 vex ⊢ 𝑦 ∈ V
30 vex ⊢ 𝑓 ∈ V
31 28 29 30 otth ⊢ ( ⟨ 𝑥 , 𝑦 , 𝑓 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑔 ⟩ ↔ ( 𝑥 = 𝑥 ∧ 𝑦 = 𝑦 ∧ 𝑓 = 𝑔 ) )
32 31 simp3bi ⊢ ( ⟨ 𝑥 , 𝑦 , 𝑓 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑔 ⟩ → 𝑓 = 𝑔 )
33 27 32 syl ⊢ ( ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑓 = 𝑔 )
34 33 ralrimivva ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) 𝑓 = 𝑔 )
35 moel ⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↔ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) 𝑓 = 𝑔 )
36 34 35 sylibr ⊢ ( ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
37 1 2 36 16 isthincd ⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝐶 ) → 𝐶 ∈ ThinCat )