homadm

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

		Ref	Expression
	Hypothesis	homahom.h	⊢ 𝐻 = ( Hom_a ‘ 𝐶 )
	Assertion	homadm	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( dom_a ‘ 𝐹 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		homahom.h	⊢ 𝐻 = ( Hom_a ‘ 𝐶 )
2		df-doma	⊢ dom_a = ( 1^st ∘ 1^st )
3	2	fveq1i	⊢ ( dom_a ‘ 𝐹 ) = ( ( 1^st ∘ 1^st ) ‘ 𝐹 )
4		fo1st	⊢ 1^st : V –onto→ V
5		fof	⊢ ( 1^st : V –onto→ V → 1^st : V ⟶ V )
6	4 5	ax-mp	⊢ 1^st : V ⟶ V
7		elex	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐹 ∈ V )
8		fvco3	⊢ ( ( 1^st : V ⟶ V ∧ 𝐹 ∈ V ) → ( ( 1^st ∘ 1^st ) ‘ 𝐹 ) = ( 1^st ‘ ( 1^st ‘ 𝐹 ) ) )
9	6 7 8	sylancr	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( ( 1^st ∘ 1^st ) ‘ 𝐹 ) = ( 1^st ‘ ( 1^st ‘ 𝐹 ) ) )
10	3 9	eqtrid	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( dom_a ‘ 𝐹 ) = ( 1^st ‘ ( 1^st ‘ 𝐹 ) ) )
11	1	homarel	⊢ Rel ( 𝑋 𝐻 𝑌 )
12		1st2ndbr	⊢ ( ( Rel ( 𝑋 𝐻 𝑌 ) ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( 1^st ‘ 𝐹 ) ( 𝑋 𝐻 𝑌 ) ( 2^nd ‘ 𝐹 ) )
13	11 12	mpan	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 1^st ‘ 𝐹 ) ( 𝑋 𝐻 𝑌 ) ( 2^nd ‘ 𝐹 ) )
14	1	homa1	⊢ ( ( 1^st ‘ 𝐹 ) ( 𝑋 𝐻 𝑌 ) ( 2^nd ‘ 𝐹 ) → ( 1^st ‘ 𝐹 ) = ⟨ 𝑋 , 𝑌 ⟩ )
15	13 14	syl	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 1^st ‘ 𝐹 ) = ⟨ 𝑋 , 𝑌 ⟩ )
16	15	fveq2d	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 1^st ‘ ( 1^st ‘ 𝐹 ) ) = ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
17		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
18	1 17	homarcl2	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
19		op1stg	⊢ ( ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
20	18 19	syl	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
21	10 16 20	3eqtrd	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( dom_a ‘ 𝐹 ) = 𝑋 )

Metamath Proof Explorer

Theorem homadm

Proof