Metamath Proof Explorer


Theorem 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=HomaC
Assertion homadm FXHYdomaF=X

Proof

Step Hyp Ref Expression
1 homahom.h H=HomaC
2 df-doma doma=1st1st
3 2 fveq1i domaF=1st1stF
4 fo1st 1st:VontoV
5 fof 1st:VontoV1st:VV
6 4 5 ax-mp 1st:VV
7 elex FXHYFV
8 fvco3 1st:VVFV1st1stF=1st1stF
9 6 7 8 sylancr FXHY1st1stF=1st1stF
10 3 9 eqtrid FXHYdomaF=1st1stF
11 1 homarel RelXHY
12 1st2ndbr RelXHYFXHY1stFXHY2ndF
13 11 12 mpan FXHY1stFXHY2ndF
14 1 homa1 1stFXHY2ndF1stF=XY
15 13 14 syl FXHY1stF=XY
16 15 fveq2d FXHY1st1stF=1stXY
17 eqid BaseC=BaseC
18 1 17 homarcl2 FXHYXBaseCYBaseC
19 op1stg XBaseCYBaseC1stXY=X
20 18 19 syl FXHY1stXY=X
21 10 16 20 3eqtrd FXHYdomaF=X