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 ) ) ) ) )