Metamath Proof Explorer

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 |) u. ( { 1o } X. tag B ) )
2 bj-pr1eq 
 |-  ( (| A ,, B |) = ( (| A |) u. ( { 1o } X. tag B ) ) -> pr1 (| A ,, B |) = pr1 ( (| A |) u. ( { 1o } X. tag B ) ) )
3 1 2 ax-mp 
 |-  pr1 (| A ,, B |) = pr1 ( (| A |) u. ( { 1o } X. tag B ) )
4 bj-pr1un 
 |-  pr1 ( (| A |) u. ( { 1o } X. tag B ) ) = ( pr1 (| A |) u. pr1 ( { 1o } X. tag B ) )
5 bj-pr11val 
 |-  pr1 (| A |) = A
6 bj-pr1val 
 |-  pr1 ( { 1o } X. tag B ) = if ( 1o = (/) , B , (/) )
7 1n0 
 |-  1o =/= (/)
8 7 neii 
 |-  -. 1o = (/)
9 8 iffalsei 
 |-  if ( 1o = (/) , B , (/) ) = (/)
10 6 9 eqtri 
 |-  pr1 ( { 1o } X. tag B ) = (/)
11 5 10 uneq12i 
 |-  ( pr1 (| A |) u. pr1 ( { 1o } X. tag B ) ) = ( A u. (/) )
12 un0 
 |-  ( A u. (/) ) = A
13 11 12 eqtri 
 |-  ( pr1 (| A |) u. pr1 ( { 1o } X. tag B ) ) = A
14 3 4 13 3eqtri 
 |-  pr1 (| A ,, B |) = A