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 |) u. ( { 1o } X. tag B ) )
2		bj-pr2eq	|- ( (| A ,, B |) = ( (| A |) u. ( { 1o } X. tag B ) ) -> pr2 (| A ,, B |) = pr2 ( (| A |) u. ( { 1o } X. tag B ) ) )
3	1 2	ax-mp	|- pr2 (| A ,, B |) = pr2 ( (| A |) u. ( { 1o } X. tag B ) )
4		bj-pr2un	|- pr2 ( (| A |) u. ( { 1o } X. tag B ) ) = ( pr2 (| A |) u. pr2 ( { 1o } X. tag B ) )
5	3 4	eqtri	|- pr2 (| A ,, B |) = ( pr2 (| A |) u. pr2 ( { 1o } X. tag B ) )
6		df-bj-1upl	|- (| A |) = ( { (/) } X. tag A )
7		bj-pr2eq	|- ( (| A |) = ( { (/) } X. tag A ) -> pr2 (| A |) = pr2 ( { (/) } X. tag A ) )
8	6 7	ax-mp	|- pr2 (| A |) = pr2 ( { (/) } X. tag A )
9		bj-pr2val	|- pr2 ( { (/) } X. tag A ) = if ( (/) = 1o , A , (/) )
10		1n0	|- 1o =/= (/)
11	10	nesymi	|- -. (/) = 1o
12	11	iffalsei	|- if ( (/) = 1o , A , (/) ) = (/)
13	8 9 12	3eqtri	|- pr2 (| A |) = (/)
14		bj-pr2val	|- pr2 ( { 1o } X. tag B ) = if ( 1o = 1o , B , (/) )
15		eqid	|- 1o = 1o
16	15	iftruei	|- if ( 1o = 1o , B , (/) ) = B
17	14 16	eqtri	|- pr2 ( { 1o } X. tag B ) = B
18	13 17	uneq12i	|- ( pr2 (| A |) u. pr2 ( { 1o } X. tag B ) ) = ( (/) u. B )
19		0un	|- ( (/) u. B ) = B
20	5 18 19	3eqtri	|- pr2 (| A ,, B |) = B