Theorem bj-pr22val

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

	Ref	Expression
Assertion	bj-pr22val	⊢ pr2 ⦅ 𝐴 , 𝐵 ⦆ = 𝐵

Proof

Step	Hyp	Ref	Expression
1		df-bj-2upl	⊢ ⦅ 𝐴 , 𝐵 ⦆ = ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) )
2		bj-pr2eq	⊢ ( ⦅ 𝐴 , 𝐵 ⦆ = ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) ) → pr2 ⦅ 𝐴 , 𝐵 ⦆ = pr2 ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) ) )
3	1 2	ax-mp	⊢ pr2 ⦅ 𝐴 , 𝐵 ⦆ = pr2 ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) )
4		bj-pr2un	⊢ pr2 ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) ) = ( pr2 ⦅ 𝐴 ⦆ ∪ pr2 ( { 1o } × tag 𝐵 ) )
5	3 4	eqtri	⊢ pr2 ⦅ 𝐴 , 𝐵 ⦆ = ( pr2 ⦅ 𝐴 ⦆ ∪ pr2 ( { 1o } × tag 𝐵 ) )
6		df-bj-1upl	⊢ ⦅ 𝐴 ⦆ = ( { ∅ } × tag 𝐴 )
7		bj-pr2eq	⊢ ( ⦅ 𝐴 ⦆ = ( { ∅ } × tag 𝐴 ) → pr2 ⦅ 𝐴 ⦆ = pr2 ( { ∅ } × tag 𝐴 ) )
8	6 7	ax-mp	⊢ pr2 ⦅ 𝐴 ⦆ = pr2 ( { ∅ } × tag 𝐴 )
9		bj-pr2val	⊢ pr2 ( { ∅ } × tag 𝐴 ) = if ( ∅ = 1o , 𝐴 , ∅ )
10		1n0	⊢ 1o ≠ ∅
11	10	nesymi	⊢ ¬ ∅ = 1o
12	11	iffalsei	⊢ if ( ∅ = 1o , 𝐴 , ∅ ) = ∅
13	8 9 12	3eqtri	⊢ pr2 ⦅ 𝐴 ⦆ = ∅
14		bj-pr2val	⊢ pr2 ( { 1o } × tag 𝐵 ) = if ( 1o = 1o , 𝐵 , ∅ )
15		eqid	⊢ 1o = 1o
16	15	iftruei	⊢ if ( 1o = 1o , 𝐵 , ∅ ) = 𝐵
17	14 16	eqtri	⊢ pr2 ( { 1o } × tag 𝐵 ) = 𝐵
18	13 17	uneq12i	⊢ ( pr2 ⦅ 𝐴 ⦆ ∪ pr2 ( { 1o } × tag 𝐵 ) ) = ( ∅ ∪ 𝐵 )
19		0un	⊢ ( ∅ ∪ 𝐵 ) = 𝐵
20	5 18 19	3eqtri	⊢ pr2 ⦅ 𝐴 , 𝐵 ⦆ = 𝐵