Theorem bj-pr21val

Description: Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-pr21val	$$⊢pr1⦅A,B⦆=A$$

Proof

Step	Hyp	Ref	Expression
1		df-bj-2upl	$$⊢⦅A,B⦆=⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)$$
2		bj-pr1eq	$$⊢⦅A,B⦆=⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\to pr1⦅A,B⦆=pr1\left(⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\right)$$
3	1 2	ax-mp	$$⊢pr1⦅A,B⦆=pr1\left(⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\right)$$
4		bj-pr1un	$$⊢pr1\left(⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\right)=pr1⦅A⦆\cup pr1\left(\left\{1_{𝑜}\right\}\times tagB\right)$$
5		bj-pr11val	$$⊢pr1⦅A⦆=A$$
6		bj-pr1val	$$⊢pr1\left(\left\{1_{𝑜}\right\}\times tagB\right)=if\left(1_{𝑜}=\varnothing ,B,\varnothing \right)$$
7		1n0	$$⊢1_{𝑜}\ne \varnothing$$
8	7	neii	$$⊢\neg 1_{𝑜}=\varnothing$$
9	8	iffalsei	$$⊢if\left(1_{𝑜}=\varnothing ,B,\varnothing \right)=\varnothing$$
10	6 9	eqtri	$$⊢pr1\left(\left\{1_{𝑜}\right\}\times tagB\right)=\varnothing$$
11	5 10	uneq12i	$$⊢pr1⦅A⦆\cup pr1\left(\left\{1_{𝑜}\right\}\times tagB\right)=A\cup \varnothing$$
12		un0	$$⊢A\cup \varnothing =A$$
13	11 12	eqtri	$$⊢pr1⦅A⦆\cup pr1\left(\left\{1_{𝑜}\right\}\times tagB\right)=A$$
14	3 4 13	3eqtri	$$⊢pr1⦅A,B⦆=A$$