Theorem bj-pr22val

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

	Ref	Expression
Assertion	bj-pr22val	$$⊢pr2⦅A,B⦆=B$$

Proof

Step	Hyp	Ref	Expression
1		df-bj-2upl	$$⊢⦅A,B⦆=⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)$$
2		bj-pr2eq	$$⊢⦅A,B⦆=⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\to pr2⦅A,B⦆=pr2\left(⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\right)$$
3	1 2	ax-mp	$$⊢pr2⦅A,B⦆=pr2\left(⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\right)$$
4		bj-pr2un	$$⊢pr2\left(⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\right)=pr2⦅A⦆\cup pr2\left(\left\{1_{𝑜}\right\}\times tagB\right)$$
5	3 4	eqtri	$$⊢pr2⦅A,B⦆=pr2⦅A⦆\cup pr2\left(\left\{1_{𝑜}\right\}\times tagB\right)$$
6		df-bj-1upl	$$⊢⦅A⦆=\left\{\varnothing \right\}\times tagA$$
7		bj-pr2eq	$$⊢⦅A⦆=\left\{\varnothing \right\}\times tagA\to pr2⦅A⦆=pr2\left(\left\{\varnothing \right\}\times tagA\right)$$
8	6 7	ax-mp	$$⊢pr2⦅A⦆=pr2\left(\left\{\varnothing \right\}\times tagA\right)$$
9		bj-pr2val	$$⊢pr2\left(\left\{\varnothing \right\}\times tagA\right)=if\left(\varnothing =1_{𝑜},A,\varnothing \right)$$
10		1n0	$$⊢1_{𝑜}\ne \varnothing$$
11	10	nesymi	$$⊢\neg \varnothing =1_{𝑜}$$
12	11	iffalsei	$$⊢if\left(\varnothing =1_{𝑜},A,\varnothing \right)=\varnothing$$
13	8 9 12	3eqtri	$$⊢pr2⦅A⦆=\varnothing$$
14		bj-pr2val	$$⊢pr2\left(\left\{1_{𝑜}\right\}\times tagB\right)=if\left(1_{𝑜}=1_{𝑜},B,\varnothing \right)$$
15		eqid	$$⊢1_{𝑜}=1_{𝑜}$$
16	15	iftruei	$$⊢if\left(1_{𝑜}=1_{𝑜},B,\varnothing \right)=B$$
17	14 16	eqtri	$$⊢pr2\left(\left\{1_{𝑜}\right\}\times tagB\right)=B$$
18	13 17	uneq12i	$$⊢pr2⦅A⦆\cup pr2\left(\left\{1_{𝑜}\right\}\times tagB\right)=\varnothing \cup B$$
19		0un	$$⊢\varnothing \cup B=B$$
20	5 18 19	3eqtri	$$⊢pr2⦅A,B⦆=B$$