Theorem bj-projval

Description: Value of the class projection. (Contributed by BJ, 6-Apr-2019)

	Ref	Expression
Assertion	bj-projval	$$⊢A\in V\to \left(AProj\left(\left\{B\right\}\times tagC\right)\right)=if\left(B=A,C,\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		elsng	$$⊢A\in V\to \left(A\in \left\{B\right\}\leftrightarrow A=B\right)$$
2		bj-xpima2sn	$$⊢A\in \left\{B\right\}\to \left(\left\{B\right\}\times tagC\right)\left[\left\{A\right\}\right]=tagC$$
3	1 2	syl6bir	$$⊢A\in V\to \left(A=B\to \left(\left\{B\right\}\times tagC\right)\left[\left\{A\right\}\right]=tagC\right)$$
4	3	imp	$$⊢\left(A\in V\wedge A=B\right)\to \left(\left\{B\right\}\times tagC\right)\left[\left\{A\right\}\right]=tagC$$
5	4	eleq2d	$$⊢\left(A\in V\wedge A=B\right)\to \left(\left\{x\right\}\in \left(\left\{B\right\}\times tagC\right)\left[\left\{A\right\}\right]\leftrightarrow \left\{x\right\}\in tagC\right)$$
6	5	abbidv	$$⊢\left(A\in V\wedge A=B\right)\to \left\{x|\left\{x\right\}\in \left(\left\{B\right\}\times tagC\right)\left[\left\{A\right\}\right]\right\}=\left\{x|\left\{x\right\}\in tagC\right\}$$
7		df-bj-proj	$$⊢\left(AProj\left(\left\{B\right\}\times tagC\right)\right)=\left\{x|\left\{x\right\}\in \left(\left\{B\right\}\times tagC\right)\left[\left\{A\right\}\right]\right\}$$
8		bj-taginv	$$⊢C=\left\{x|\left\{x\right\}\in tagC\right\}$$
9	6 7 8	3eqtr4g	$$⊢\left(A\in V\wedge A=B\right)\to \left(AProj\left(\left\{B\right\}\times tagC\right)\right)=C$$
10	9	ex	$$⊢A\in V\to \left(A=B\to \left(AProj\left(\left\{B\right\}\times tagC\right)\right)=C\right)$$
11		noel	$$⊢\neg \left\{x\right\}\in \varnothing$$
12	7	abeq2i	$$⊢x\in \left(AProj\left(\left\{B\right\}\times tagC\right)\right)\leftrightarrow \left\{x\right\}\in \left(\left\{B\right\}\times tagC\right)\left[\left\{A\right\}\right]$$
13		elsni	$$⊢A\in \left\{B\right\}\to A=B$$
14		bj-xpima1sn	$$⊢\neg A\in \left\{B\right\}\to \left(\left\{B\right\}\times tagC\right)\left[\left\{A\right\}\right]=\varnothing$$
15	13 14	nsyl5	$$⊢\neg A=B\to \left(\left\{B\right\}\times tagC\right)\left[\left\{A\right\}\right]=\varnothing$$
16	15	eleq2d	$$⊢\neg A=B\to \left(\left\{x\right\}\in \left(\left\{B\right\}\times tagC\right)\left[\left\{A\right\}\right]\leftrightarrow \left\{x\right\}\in \varnothing \right)$$
17	12 16	syl5bb	$$⊢\neg A=B\to \left(x\in \left(AProj\left(\left\{B\right\}\times tagC\right)\right)\leftrightarrow \left\{x\right\}\in \varnothing \right)$$
18	11 17	mtbiri	$$⊢\neg A=B\to \neg x\in \left(AProj\left(\left\{B\right\}\times tagC\right)\right)$$
19	18	eq0rdv	$$⊢\neg A=B\to \left(AProj\left(\left\{B\right\}\times tagC\right)\right)=\varnothing$$
20		ifval	$$⊢\left(AProj\left(\left\{B\right\}\times tagC\right)\right)=if\left(A=B,C,\varnothing \right)\leftrightarrow \left(\left(A=B\to \left(AProj\left(\left\{B\right\}\times tagC\right)\right)=C\right)\wedge \left(\neg A=B\to \left(AProj\left(\left\{B\right\}\times tagC\right)\right)=\varnothing \right)\right)$$
21	10 19 20	sylanblrc	$$⊢A\in V\to \left(AProj\left(\left\{B\right\}\times tagC\right)\right)=if\left(A=B,C,\varnothing \right)$$
22		eqcom	$$⊢A=B\leftrightarrow B=A$$
23		ifbi	$$⊢\left(A=B\leftrightarrow B=A\right)\to if\left(A=B,C,\varnothing \right)=if\left(B=A,C,\varnothing \right)$$
24	22 23	ax-mp	$$⊢if\left(A=B,C,\varnothing \right)=if\left(B=A,C,\varnothing \right)$$
25	21 24	eqtrdi	$$⊢A\in V\to \left(AProj\left(\left\{B\right\}\times tagC\right)\right)=if\left(B=A,C,\varnothing \right)$$