Metamath Proof Explorer


Theorem 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=xV,y1stxn1stx|φ
Assertion mpoxopoveq VXWYKVVWFK=nV|[˙VW/x]˙[˙K/y]˙φ

Proof

Step Hyp Ref Expression
1 mpoxopoveq.f F=xV,y1stxn1stx|φ
2 1 a1i VXWYKVF=xV,y1stxn1stx|φ
3 fveq2 x=VW1stx=1stVW
4 op1stg VXWY1stVW=V
5 4 adantr VXWYKV1stVW=V
6 3 5 sylan9eqr VXWYKVx=VW1stx=V
7 6 adantrr VXWYKVx=VWy=K1stx=V
8 sbceq1a y=Kφ[˙K/y]˙φ
9 8 adantl x=VWy=Kφ[˙K/y]˙φ
10 9 adantl VXWYKVx=VWy=Kφ[˙K/y]˙φ
11 sbceq1a x=VW[˙K/y]˙φ[˙VW/x]˙[˙K/y]˙φ
12 11 adantr x=VWy=K[˙K/y]˙φ[˙VW/x]˙[˙K/y]˙φ
13 12 adantl VXWYKVx=VWy=K[˙K/y]˙φ[˙VW/x]˙[˙K/y]˙φ
14 10 13 bitrd VXWYKVx=VWy=Kφ[˙VW/x]˙[˙K/y]˙φ
15 7 14 rabeqbidv VXWYKVx=VWy=Kn1stx|φ=nV|[˙VW/x]˙[˙K/y]˙φ
16 opex VWV
17 16 a1i VXWYKVVWV
18 simpr VXWYKVKV
19 rabexg VXnV|[˙VW/x]˙[˙K/y]˙φV
20 19 ad2antrr VXWYKVnV|[˙VW/x]˙[˙K/y]˙φV
21 equid z=z
22 nfvd z=zxVXWYKV
23 21 22 ax-mp xVXWYKV
24 nfvd z=zyVXWYKV
25 21 24 ax-mp yVXWYKV
26 nfcv _yVW
27 nfcv _xK
28 nfsbc1v x[˙VW/x]˙[˙K/y]˙φ
29 nfcv _xV
30 28 29 nfrabw _xnV|[˙VW/x]˙[˙K/y]˙φ
31 nfsbc1v y[˙K/y]˙φ
32 26 31 nfsbcw y[˙VW/x]˙[˙K/y]˙φ
33 nfcv _yV
34 32 33 nfrabw _ynV|[˙VW/x]˙[˙K/y]˙φ
35 2 15 6 17 18 20 23 25 26 27 30 34 ovmpodxf VXWYKVVWFK=nV|[˙VW/x]˙[˙K/y]˙φ