This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem issect

Description: The property " F is a section of G ". (Contributed by Mario Carneiro, 2-Jan-2017)

		Ref	Expression
	Hypotheses	issect.b	\|- B = ( Base ` C )
		issect.h	\|- H = ( Hom ` C )
		issect.o	\|- .x. = ( comp ` C )
		issect.i	\|- .1. = ( Id ` C )
		issect.s	\|- S = ( Sect ` C )
		issect.c	\|- ( ph -> C e. Cat )
		issect.x	\|- ( ph -> X e. B )
		issect.y	\|- ( ph -> Y e. B )
	Assertion	issect	\|- ( ph -> ( F ( X S Y ) G <-> ( F e. ( X H Y ) /\ G e. ( Y H X ) /\ ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		issect.b	\|- B = ( Base ` C )
2		issect.h	\|- H = ( Hom ` C )
3		issect.o	\|- .x. = ( comp ` C )
4		issect.i	\|- .1. = ( Id ` C )
5		issect.s	\|- S = ( Sect ` C )
6		issect.c	\|- ( ph -> C e. Cat )
7		issect.x	\|- ( ph -> X e. B )
8		issect.y	\|- ( ph -> Y e. B )
9	1 2 3 4 5 6 7 8	sectfval	\|- ( ph -> ( X S Y ) = { <. f , g >. \| ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. .x. X ) f ) = ( .1. ` X ) ) } )
10	9	breqd	\|- ( ph -> ( F ( X S Y ) G <-> F { <. f , g >. \| ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. .x. X ) f ) = ( .1. ` X ) ) } G ) )
11		oveq12	\|- ( ( g = G /\ f = F ) -> ( g ( <. X , Y >. .x. X ) f ) = ( G ( <. X , Y >. .x. X ) F ) )
12	11	ancoms	\|- ( ( f = F /\ g = G ) -> ( g ( <. X , Y >. .x. X ) f ) = ( G ( <. X , Y >. .x. X ) F ) )
13	12	eqeq1d	\|- ( ( f = F /\ g = G ) -> ( ( g ( <. X , Y >. .x. X ) f ) = ( .1. ` X ) <-> ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) ) )
14		eqid	\|- { <. f , g >. \| ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. .x. X ) f ) = ( .1. ` X ) ) } = { <. f , g >. \| ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. .x. X ) f ) = ( .1. ` X ) ) }
15	13 14	brab2a	\|- ( F { <. f , g >. \| ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. .x. X ) f ) = ( .1. ` X ) ) } G <-> ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) ) )
16		df-3an	\|- ( ( F e. ( X H Y ) /\ G e. ( Y H X ) /\ ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) ) <-> ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) ) )
17	15 16	bitr4i	\|- ( F { <. f , g >. \| ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. .x. X ) f ) = ( .1. ` X ) ) } G <-> ( F e. ( X H Y ) /\ G e. ( Y H X ) /\ ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) ) )
18	10 17	bitrdi	\|- ( ph -> ( F ( X S Y ) G <-> ( F e. ( X H Y ) /\ G e. ( Y H X ) /\ ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) ) ) )