Theorem fnwe2lem1

Description: Lemma for fnwe2 . Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015)

	Ref	Expression
Hypotheses	fnwe2.su	$$⊢z=F\left(x\right)\to S=U$$
	fnwe2.t	$$⊢T=\left\{⟨x,y⟩|\left(F\left(x\right)RF\left(y\right)\vee \left(F\left(x\right)=F\left(y\right)\wedge xUy\right)\right)\right\}$$
	fnwe2.s	$$⊢\left(\phi \wedge x\in A\right)\to U\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(x\right)\right\}$$
Assertion	fnwe2lem1	$$⊢\left(\phi \wedge a\in A\right)\to ⦋F\left(a\right)/z⦌S\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(a\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fnwe2.su	$$⊢z=F\left(x\right)\to S=U$$
2		fnwe2.t	$$⊢T=\left\{⟨x,y⟩|\left(F\left(x\right)RF\left(y\right)\vee \left(F\left(x\right)=F\left(y\right)\wedge xUy\right)\right)\right\}$$
3		fnwe2.s	$$⊢\left(\phi \wedge x\in A\right)\to U\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(x\right)\right\}$$
4	3	ralrimiva	$$⊢\phi \to \forall x\in AU\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(x\right)\right\}$$
5		fveq2	$$⊢a=x\to F\left(a\right)=F\left(x\right)$$
6	5	csbeq1d	$$⊢a=x\to ⦋F\left(a\right)/z⦌S=⦋F\left(x\right)/z⦌S$$
7		fvex	$$⊢F\left(x\right)\in \mathrm{V}$$
8	7 1	csbie	$$⊢⦋F\left(x\right)/z⦌S=U$$
9	6 8	eqtrdi	$$⊢a=x\to ⦋F\left(a\right)/z⦌S=U$$
10	5	eqeq2d	$$⊢a=x\to \left(F\left(y\right)=F\left(a\right)\leftrightarrow F\left(y\right)=F\left(x\right)\right)$$
11	10	rabbidv	$$⊢a=x\to \left\{y\in A|F\left(y\right)=F\left(a\right)\right\}=\left\{y\in A|F\left(y\right)=F\left(x\right)\right\}$$
12	9 11	weeq12d	$$⊢a=x\to \left(⦋F\left(a\right)/z⦌S\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(a\right)\right\}\leftrightarrow U\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(x\right)\right\}\right)$$
13	12	cbvralvw	$$⊢\forall a\in A⦋F\left(a\right)/z⦌S\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(a\right)\right\}\leftrightarrow \forall x\in AU\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(x\right)\right\}$$
14	4 13	sylibr	$$⊢\phi \to \forall a\in A⦋F\left(a\right)/z⦌S\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(a\right)\right\}$$
15	14	r19.21bi	$$⊢\left(\phi \wedge a\in A\right)\to ⦋F\left(a\right)/z⦌S\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(a\right)\right\}$$