mpoxopoveq

Description: Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens, 11-Oct-2017)

		Ref	Expression
	Hypothesis	mpoxopoveq.f	\|- F = ( x e. _V , y e. ( 1st ` x ) \|-> { n e. ( 1st ` x ) \| ph } )
	Assertion	mpoxopoveq	\|- ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> ( <. V , W >. F K ) = { n e. V \| [. <. V , W >. / x ]. [. K / y ]. ph } )

Proof

Step	Hyp	Ref	Expression
1		mpoxopoveq.f	\|- F = ( x e. _V , y e. ( 1st ` x ) \|-> { n e. ( 1st ` x ) \| ph } )
2	1	a1i	\|- ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> F = ( x e. _V , y e. ( 1st ` x ) \|-> { n e. ( 1st ` x ) \| ph } ) )
3		fveq2	\|- ( x = <. V , W >. -> ( 1st ` x ) = ( 1st ` <. V , W >. ) )
4		op1stg	\|- ( ( V e. X /\ W e. Y ) -> ( 1st ` <. V , W >. ) = V )
5	4	adantr	\|- ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> ( 1st ` <. V , W >. ) = V )
6	3 5	sylan9eqr	\|- ( ( ( ( V e. X /\ W e. Y ) /\ K e. V ) /\ x = <. V , W >. ) -> ( 1st ` x ) = V )
7	6	adantrr	\|- ( ( ( ( V e. X /\ W e. Y ) /\ K e. V ) /\ ( x = <. V , W >. /\ y = K ) ) -> ( 1st ` x ) = V )
8		sbceq1a	\|- ( y = K -> ( ph <-> [. K / y ]. ph ) )
9	8	adantl	\|- ( ( x = <. V , W >. /\ y = K ) -> ( ph <-> [. K / y ]. ph ) )
10	9	adantl	\|- ( ( ( ( V e. X /\ W e. Y ) /\ K e. V ) /\ ( x = <. V , W >. /\ y = K ) ) -> ( ph <-> [. K / y ]. ph ) )
11		sbceq1a	\|- ( x = <. V , W >. -> ( [. K / y ]. ph <-> [. <. V , W >. / x ]. [. K / y ]. ph ) )
12	11	adantr	\|- ( ( x = <. V , W >. /\ y = K ) -> ( [. K / y ]. ph <-> [. <. V , W >. / x ]. [. K / y ]. ph ) )
13	12	adantl	\|- ( ( ( ( V e. X /\ W e. Y ) /\ K e. V ) /\ ( x = <. V , W >. /\ y = K ) ) -> ( [. K / y ]. ph <-> [. <. V , W >. / x ]. [. K / y ]. ph ) )
14	10 13	bitrd	\|- ( ( ( ( V e. X /\ W e. Y ) /\ K e. V ) /\ ( x = <. V , W >. /\ y = K ) ) -> ( ph <-> [. <. V , W >. / x ]. [. K / y ]. ph ) )
15	7 14	rabeqbidv	\|- ( ( ( ( V e. X /\ W e. Y ) /\ K e. V ) /\ ( x = <. V , W >. /\ y = K ) ) -> { n e. ( 1st ` x ) \| ph } = { n e. V \| [. <. V , W >. / x ]. [. K / y ]. ph } )
16		opex	\|- <. V , W >. e. _V
17	16	a1i	\|- ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> <. V , W >. e. _V )
18		simpr	\|- ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> K e. V )
19		rabexg	\|- ( V e. X -> { n e. V \| [. <. V , W >. / x ]. [. K / y ]. ph } e. _V )
20	19	ad2antrr	\|- ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> { n e. V \| [. <. V , W >. / x ]. [. K / y ]. ph } e. _V )
21		equid	\|- z = z
22		nfvd	\|- ( z = z -> F/ x ( ( V e. X /\ W e. Y ) /\ K e. V ) )
23	21 22	ax-mp	\|- F/ x ( ( V e. X /\ W e. Y ) /\ K e. V )
24		nfvd	\|- ( z = z -> F/ y ( ( V e. X /\ W e. Y ) /\ K e. V ) )
25	21 24	ax-mp	\|- F/ y ( ( V e. X /\ W e. Y ) /\ K e. V )
26		nfcv	\|- F/_ y <. V , W >.
27		nfcv	\|- F/_ x K
28		nfsbc1v	\|- F/ x [. <. V , W >. / x ]. [. K / y ]. ph
29		nfcv	\|- F/_ x V
30	28 29	nfrabw	\|- F/_ x { n e. V \| [. <. V , W >. / x ]. [. K / y ]. ph }
31		nfsbc1v	\|- F/ y [. K / y ]. ph
32	26 31	nfsbcw	\|- F/ y [. <. V , W >. / x ]. [. K / y ]. ph
33		nfcv	\|- F/_ y V
34	32 33	nfrabw	\|- F/_ y { n e. V \| [. <. V , W >. / x ]. [. K / y ]. ph }
35	2 15 6 17 18 20 23 25 26 27 30 34	ovmpodxf	\|- ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> ( <. V , W >. F K ) = { n e. V \| [. <. V , W >. / x ]. [. K / y ]. ph } )

Metamath Proof Explorer

Theorem mpoxopoveq

Proof