Theorem bj-pr21val

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

	Ref	Expression
Assertion	bj-pr21val	⊢ pr1 ⦅ 𝐴 , 𝐵 ⦆ = 𝐴

Proof

Step	Hyp	Ref	Expression
1		df-bj-2upl	⊢ ⦅ 𝐴 , 𝐵 ⦆ = ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) )
2		bj-pr1eq	⊢ ( ⦅ 𝐴 , 𝐵 ⦆ = ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) ) → pr1 ⦅ 𝐴 , 𝐵 ⦆ = pr1 ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) ) )
3	1 2	ax-mp	⊢ pr1 ⦅ 𝐴 , 𝐵 ⦆ = pr1 ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) )
4		bj-pr1un	⊢ pr1 ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) ) = ( pr1 ⦅ 𝐴 ⦆ ∪ pr1 ( { 1o } × tag 𝐵 ) )
5		bj-pr11val	⊢ pr1 ⦅ 𝐴 ⦆ = 𝐴
6		bj-pr1val	⊢ pr1 ( { 1o } × tag 𝐵 ) = if ( 1o = ∅ , 𝐵 , ∅ )
7		1n0	⊢ 1o ≠ ∅
8	7	neii	⊢ ¬ 1o = ∅
9	8	iffalsei	⊢ if ( 1o = ∅ , 𝐵 , ∅ ) = ∅
10	6 9	eqtri	⊢ pr1 ( { 1o } × tag 𝐵 ) = ∅
11	5 10	uneq12i	⊢ ( pr1 ⦅ 𝐴 ⦆ ∪ pr1 ( { 1o } × tag 𝐵 ) ) = ( 𝐴 ∪ ∅ )
12		un0	⊢ ( 𝐴 ∪ ∅ ) = 𝐴
13	11 12	eqtri	⊢ ( pr1 ⦅ 𝐴 ⦆ ∪ pr1 ( { 1o } × tag 𝐵 ) ) = 𝐴
14	3 4 13	3eqtri	⊢ pr1 ⦅ 𝐴 , 𝐵 ⦆ = 𝐴