evl1fval1lem

Step	Hyp	Ref	Expression
1		evl1fval1.q	$⊢ Q = {eval}_{1} (R)$
2		evl1fval1.b	$⊢ B = {Base}_{R}$
3		eqid	$⊢ {eval}_{1} (R) = {eval}_{1} (R)$
4		eqid	$⊢ 1_{𝑜} eval R = 1_{𝑜} eval R$
5	3 4 2	evl1fval	$⊢ {eval}_{1} (R) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} eval R)$
6	1	a1i	$⊢ R \in V \to Q = {eval}_{1} (R)$
7	2	fvexi	$⊢ B \in V$
8	7	pwid	$⊢ B \in 𝒫 B$
9		eqid	$⊢ R {evalSub}_{1} B = R {evalSub}_{1} B$
10		eqid	$⊢ 1_{𝑜} evalSub R = 1_{𝑜} evalSub R$
11	9 10 2	evls1fval	$⊢ (R \in V \land B \in 𝒫 B) \to R {evalSub}_{1} B = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub R) (B)$
12	8 11	mpan2	$⊢ R \in V \to R {evalSub}_{1} B = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub R) (B)$
13	4 2	evlval	$⊢ 1_{𝑜} eval R = (1_{𝑜} evalSub R) (B)$
14	13	eqcomi	$⊢ (1_{𝑜} evalSub R) (B) = 1_{𝑜} eval R$
15	14	coeq2i	$⊢ (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub R) (B) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} eval R)$
16	12 15	eqtrdi	$⊢ R \in V \to R {evalSub}_{1} B = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} eval R)$
17	5 6 16	3eqtr4a	$⊢ R \in V \to Q = R {evalSub}_{1} B$

Metamath Proof Explorer