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

Metamath Proof Explorer

Theorem oemapval

Description: Value of the relation T . (Contributed by Mario Carneiro, 28-May-2015)

		Ref	Expression
	Hypotheses	cantnfs.s	\|- S = dom ( A CNF B )
		cantnfs.a	\|- ( ph -> A e. On )
		cantnfs.b	\|- ( ph -> B e. On )
		oemapval.t	\|- T = { <. x , y >. \| E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
		oemapval.f	\|- ( ph -> F e. S )
		oemapval.g	\|- ( ph -> G e. S )
	Assertion	oemapval	\|- ( ph -> ( F T G <-> E. z e. B ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	\|- S = dom ( A CNF B )
2		cantnfs.a	\|- ( ph -> A e. On )
3		cantnfs.b	\|- ( ph -> B e. On )
4		oemapval.t	\|- T = { <. x , y >. \| E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
5		oemapval.f	\|- ( ph -> F e. S )
6		oemapval.g	\|- ( ph -> G e. S )
7		fveq1	\|- ( x = F -> ( x ` z ) = ( F ` z ) )
8		fveq1	\|- ( y = G -> ( y ` z ) = ( G ` z ) )
9		eleq12	\|- ( ( ( x ` z ) = ( F ` z ) /\ ( y ` z ) = ( G ` z ) ) -> ( ( x ` z ) e. ( y ` z ) <-> ( F ` z ) e. ( G ` z ) ) )
10	7 8 9	syl2an	\|- ( ( x = F /\ y = G ) -> ( ( x ` z ) e. ( y ` z ) <-> ( F ` z ) e. ( G ` z ) ) )
11		fveq1	\|- ( x = F -> ( x ` w ) = ( F ` w ) )
12		fveq1	\|- ( y = G -> ( y ` w ) = ( G ` w ) )
13	11 12	eqeqan12d	\|- ( ( x = F /\ y = G ) -> ( ( x ` w ) = ( y ` w ) <-> ( F ` w ) = ( G ` w ) ) )
14	13	imbi2d	\|- ( ( x = F /\ y = G ) -> ( ( z e. w -> ( x ` w ) = ( y ` w ) ) <-> ( z e. w -> ( F ` w ) = ( G ` w ) ) ) )
15	14	ralbidv	\|- ( ( x = F /\ y = G ) -> ( A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) <-> A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) )
16	10 15	anbi12d	\|- ( ( x = F /\ y = G ) -> ( ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) )
17	16	rexbidv	\|- ( ( x = F /\ y = G ) -> ( E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) <-> E. z e. B ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) )
18	17 4	brabga	\|- ( ( F e. S /\ G e. S ) -> ( F T G <-> E. z e. B ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) )
19	5 6 18	syl2anc	\|- ( ph -> ( F T G <-> E. z e. B ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) )