Metamath Proof Explorer

Theorem arwhoma

Description: An arrow is contained in the hom-set corresponding to its domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses arwrcl.a ⊢ 𝐴 = ( Arrow ‘ 𝐶 )
arwhoma.h ⊢ 𝐻 = ( Homa ‘ 𝐶 )
Assertion arwhoma ( 𝐹 ∈ 𝐴 → 𝐹 ∈ ( ( doma ‘ 𝐹 ) 𝐻 ( coda ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 arwrcl.a ⊢ 𝐴 = ( Arrow ‘ 𝐶 )
2 arwhoma.h ⊢ 𝐻 = ( Homa ‘ 𝐶 )
3 1 2 arwval ⊢ 𝐴 = ∪ ran 𝐻
4 3 eleq2i ⊢ ( 𝐹 ∈ 𝐴 ↔ 𝐹 ∈ ∪ ran 𝐻 )
5 4 biimpi ⊢ ( 𝐹 ∈ 𝐴 → 𝐹 ∈ ∪ ran 𝐻 )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 1 arwrcl ⊢ ( 𝐹 ∈ 𝐴 → 𝐶 ∈ Cat )
8 2 6 7 homaf ⊢ ( 𝐹 ∈ 𝐴 → 𝐻 : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ⟶ 𝒫 ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) × V ) )
9 ffn ⊢ ( 𝐻 : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ⟶ 𝒫 ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) × V ) → 𝐻 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
10 fnunirn ⊢ ( 𝐻 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → ( 𝐹 ∈ ∪ ran 𝐻 ↔ ∃ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) 𝐹 ∈ ( 𝐻 ‘ 𝑧 ) ) )
11 8 9 10 3syl ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ∈ ∪ ran 𝐻 ↔ ∃ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) 𝐹 ∈ ( 𝐻 ‘ 𝑧 ) ) )
12 5 11 mpbid ⊢ ( 𝐹 ∈ 𝐴 → ∃ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) 𝐹 ∈ ( 𝐻 ‘ 𝑧 ) )
13 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
14 df-ov ⊢ ( 𝑥 𝐻 𝑦 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
15 13 14 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻 ‘ 𝑧 ) = ( 𝑥 𝐻 𝑦 ) )
16 15 eleq2d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ∈ ( 𝐻 ‘ 𝑧 ) ↔ 𝐹 ∈ ( 𝑥 𝐻 𝑦 ) ) )
17 16 rexxp ⊢ ( ∃ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) 𝐹 ∈ ( 𝐻 ‘ 𝑧 ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐶 ) ∃ 𝑦 ∈ ( Base ‘ 𝐶 ) 𝐹 ∈ ( 𝑥 𝐻 𝑦 ) )
18 12 17 sylib ⊢ ( 𝐹 ∈ 𝐴 → ∃ 𝑥 ∈ ( Base ‘ 𝐶 ) ∃ 𝑦 ∈ ( Base ‘ 𝐶 ) 𝐹 ∈ ( 𝑥 𝐻 𝑦 ) )
19 id ⊢ ( 𝐹 ∈ ( 𝑥 𝐻 𝑦 ) → 𝐹 ∈ ( 𝑥 𝐻 𝑦 ) )
20 2 homadm ⊢ ( 𝐹 ∈ ( 𝑥 𝐻 𝑦 ) → ( doma ‘ 𝐹 ) = 𝑥 )
21 2 homacd ⊢ ( 𝐹 ∈ ( 𝑥 𝐻 𝑦 ) → ( coda ‘ 𝐹 ) = 𝑦 )
22 20 21 oveq12d ⊢ ( 𝐹 ∈ ( 𝑥 𝐻 𝑦 ) → ( ( doma ‘ 𝐹 ) 𝐻 ( coda ‘ 𝐹 ) ) = ( 𝑥 𝐻 𝑦 ) )
23 19 22 eleqtrrd ⊢ ( 𝐹 ∈ ( 𝑥 𝐻 𝑦 ) → 𝐹 ∈ ( ( doma ‘ 𝐹 ) 𝐻 ( coda ‘ 𝐹 ) ) )
24 23 rexlimivw ⊢ ( ∃ 𝑦 ∈ ( Base ‘ 𝐶 ) 𝐹 ∈ ( 𝑥 𝐻 𝑦 ) → 𝐹 ∈ ( ( doma ‘ 𝐹 ) 𝐻 ( coda ‘ 𝐹 ) ) )
25 24 rexlimivw ⊢ ( ∃ 𝑥 ∈ ( Base ‘ 𝐶 ) ∃ 𝑦 ∈ ( Base ‘ 𝐶 ) 𝐹 ∈ ( 𝑥 𝐻 𝑦 ) → 𝐹 ∈ ( ( doma ‘ 𝐹 ) 𝐻 ( coda ‘ 𝐹 ) ) )
26 18 25 syl ⊢ ( 𝐹 ∈ 𝐴 → 𝐹 ∈ ( ( doma ‘ 𝐹 ) 𝐻 ( coda ‘ 𝐹 ) ) )