Theorem prdsbascl

Description: An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypotheses	prdsbasmpt2.y	$$⊢Y=S{⨉}_{𝑠}\left(x\in I⟼R\right)$$
	prdsbasmpt2.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsbasmpt2.s	$$⊢\phi \to S\in V$$
	prdsbasmpt2.i	$$⊢\phi \to I\in W$$
	prdsbasmpt2.r	$$⊢\phi \to \forall x\in IR\in X$$
	prdsbasmpt2.k	$$⊢K={\mathrm{Base}}_R$$
	prdsbascl.f	$$⊢\phi \to F\in B$$
Assertion	prdsbascl	$$⊢\phi \to \forall x\in IF\left(x\right)\in K$$

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt2.y	$$⊢Y=S{⨉}_{𝑠}\left(x\in I⟼R\right)$$
2		prdsbasmpt2.b	$$⊢B={\mathrm{Base}}_Y$$
3		prdsbasmpt2.s	$$⊢\phi \to S\in V$$
4		prdsbasmpt2.i	$$⊢\phi \to I\in W$$
5		prdsbasmpt2.r	$$⊢\phi \to \forall x\in IR\in X$$
6		prdsbasmpt2.k	$$⊢K={\mathrm{Base}}_R$$
7		prdsbascl.f	$$⊢\phi \to F\in B$$
8		eqid	$$⊢\left(x\in I⟼R\right)=\left(x\in I⟼R\right)$$
9	8	fnmpt	$$⊢\forall x\in IR\in X\to \left(x\in I⟼R\right)FnI$$
10	5 9	syl	$$⊢\phi \to \left(x\in I⟼R\right)FnI$$
11	1 2 3 4 10 7	prdsbasfn	$$⊢\phi \to FFnI$$
12		dffn5	$$⊢FFnI\leftrightarrow F=\left(x\in I⟼F\left(x\right)\right)$$
13	11 12	sylib	$$⊢\phi \to F=\left(x\in I⟼F\left(x\right)\right)$$
14	13 7	eqeltrrd	$$⊢\phi \to \left(x\in I⟼F\left(x\right)\right)\in B$$
15	1 2 3 4 5 6	prdsbasmpt2	$$⊢\phi \to \left(\left(x\in I⟼F\left(x\right)\right)\in B\leftrightarrow \forall x\in IF\left(x\right)\in K\right)$$
16	14 15	mpbid	$$⊢\phi \to \forall x\in IF\left(x\right)\in K$$