Metamath Proof Explorer


Theorem mpoxopovel

Description: Element of the 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 and Mario Carneiro, 10-Oct-2017)

Ref Expression
Hypothesis mpoxopoveq.f F = x V , y 1 st x n 1 st x | φ
Assertion mpoxopovel V X W Y N V W F K K V N V [˙ V W / x]˙ [˙K / y]˙ [˙N / n]˙ φ

Proof

Step Hyp Ref Expression
1 mpoxopoveq.f F = x V , y 1 st x n 1 st x | φ
2 1 mpoxopn0yelv V X W Y N V W F K K V
3 2 pm4.71rd V X W Y N V W F K K V N V W F K
4 1 mpoxopoveq V X W Y K V V W F K = n V | [˙ V W / x]˙ [˙K / y]˙ φ
5 4 eleq2d V X W Y K V N V W F K N n V | [˙ V W / x]˙ [˙K / y]˙ φ
6 nfcv _ n V
7 6 elrabsf N n V | [˙ V W / x]˙ [˙K / y]˙ φ N V [˙N / n]˙ [˙ V W / x]˙ [˙K / y]˙ φ
8 sbccom [˙N / n]˙ [˙ V W / x]˙ [˙K / y]˙ φ [˙ V W / x]˙ [˙N / n]˙ [˙K / y]˙ φ
9 sbccom [˙N / n]˙ [˙K / y]˙ φ [˙K / y]˙ [˙N / n]˙ φ
10 9 sbcbii [˙ V W / x]˙ [˙N / n]˙ [˙K / y]˙ φ [˙ V W / x]˙ [˙K / y]˙ [˙N / n]˙ φ
11 8 10 bitri [˙N / n]˙ [˙ V W / x]˙ [˙K / y]˙ φ [˙ V W / x]˙ [˙K / y]˙ [˙N / n]˙ φ
12 11 anbi2i N V [˙N / n]˙ [˙ V W / x]˙ [˙K / y]˙ φ N V [˙ V W / x]˙ [˙K / y]˙ [˙N / n]˙ φ
13 7 12 bitri N n V | [˙ V W / x]˙ [˙K / y]˙ φ N V [˙ V W / x]˙ [˙K / y]˙ [˙N / n]˙ φ
14 5 13 bitrdi V X W Y K V N V W F K N V [˙ V W / x]˙ [˙K / y]˙ [˙N / n]˙ φ
15 14 pm5.32da V X W Y K V N V W F K K V N V [˙ V W / x]˙ [˙K / y]˙ [˙N / n]˙ φ
16 3anass K V N V [˙ V W / x]˙ [˙K / y]˙ [˙N / n]˙ φ K V N V [˙ V W / x]˙ [˙K / y]˙ [˙N / n]˙ φ
17 15 16 bitr4di V X W Y K V N V W F K K V N V [˙ V W / x]˙ [˙K / y]˙ [˙N / n]˙ φ
18 3 17 bitrd V X W Y N V W F K K V N V [˙ V W / x]˙ [˙K / y]˙ [˙N / n]˙ φ