homadm

Description: The domain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017)

		Ref	Expression
	Hypothesis	homahom.h	$⊢ H = {Hom}_{a} (C)$
	Assertion	homadm	$⊢ F \in (X H Y) \to {dom}_{a} (F) = X$

Step	Hyp	Ref	Expression
1		homahom.h	$⊢ H = {Hom}_{a} (C)$
2		df-doma	$⊢ {dom}_{a} = 1^{st} \circ 1^{st}$
3	2	fveq1i	$⊢ {dom}_{a} (F) = (1^{st} \circ 1^{st}) (F)$
4		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
5		fof	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} : V ⟶ V$
6	4 5	ax-mp	$⊢ 1^{st} : V ⟶ V$
7		elex	$⊢ F \in (X H Y) \to F \in V$
8		fvco3	$⊢ (1^{st} : V ⟶ V \land F \in V) \to (1^{st} \circ 1^{st}) (F) = 1^{st} (1^{st} (F))$
9	6 7 8	sylancr	$⊢ F \in (X H Y) \to (1^{st} \circ 1^{st}) (F) = 1^{st} (1^{st} (F))$
10	3 9	eqtrid	$⊢ F \in (X H Y) \to {dom}_{a} (F) = 1^{st} (1^{st} (F))$
11	1	homarel	$⊢ Rel (X H Y)$
12		1st2ndbr	$⊢ (Rel (X H Y) \land F \in (X H Y)) \to 1^{st} (F) (X H Y) 2^{nd} (F)$
13	11 12	mpan	$⊢ F \in (X H Y) \to 1^{st} (F) (X H Y) 2^{nd} (F)$
14	1	homa1	$⊢ 1^{st} (F) (X H Y) 2^{nd} (F) \to 1^{st} (F) = ⟨X, Y⟩$
15	13 14	syl	$⊢ F \in (X H Y) \to 1^{st} (F) = ⟨X, Y⟩$
16	15	fveq2d	$⊢ F \in (X H Y) \to 1^{st} (1^{st} (F)) = 1^{st} (⟨X, Y⟩)$
17		eqid	$⊢ {Base}_{C} = {Base}_{C}$
18	1 17	homarcl2	$⊢ F \in (X H Y) \to (X \in {Base}_{C} \land Y \in {Base}_{C})$
19		op1stg	$⊢ (X \in {Base}_{C} \land Y \in {Base}_{C}) \to 1^{st} (⟨X, Y⟩) = X$
20	18 19	syl	$⊢ F \in (X H Y) \to 1^{st} (⟨X, Y⟩) = X$
21	10 16 20	3eqtrd	$⊢ F \in (X H Y) \to {dom}_{a} (F) = X$

Metamath Proof Explorer