Metamath Proof Explorer


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 1 𝑜 × tag B
2 bj-pr2eq A B = A 1 𝑜 × tag B pr2 A B = pr2 A 1 𝑜 × tag B
3 1 2 ax-mp pr2 A B = pr2 A 1 𝑜 × tag B
4 bj-pr2un pr2 A 1 𝑜 × tag B = pr2 A pr2 1 𝑜 × tag B
5 3 4 eqtri pr2 A B = pr2 A pr2 1 𝑜 × tag B
6 df-bj-1upl A = × tag A
7 bj-pr2eq A = × tag A pr2 A = pr2 × tag A
8 6 7 ax-mp pr2 A = pr2 × tag A
9 bj-pr2val pr2 × tag A = if = 1 𝑜 A
10 1n0 1 𝑜
11 10 nesymi ¬ = 1 𝑜
12 11 iffalsei if = 1 𝑜 A =
13 8 9 12 3eqtri pr2 A =
14 bj-pr2val pr2 1 𝑜 × tag B = if 1 𝑜 = 1 𝑜 B
15 eqid 1 𝑜 = 1 𝑜
16 15 iftruei if 1 𝑜 = 1 𝑜 B = B
17 14 16 eqtri pr2 1 𝑜 × tag B = B
18 13 17 uneq12i pr2 A pr2 1 𝑜 × tag B = B
19 0un B = B
20 5 18 19 3eqtri pr2 A B = B