Metamath Proof Explorer


Theorem bj-projval

Description: Value of the class projection. (Contributed by BJ, 6-Apr-2019)

Ref Expression
Assertion bj-projval A V A Proj B × tag C = if B = A C

Proof

Step Hyp Ref Expression
1 elsng A V A B A = B
2 bj-xpima2sn A B B × tag C A = tag C
3 1 2 syl6bir A V A = B B × tag C A = tag C
4 3 imp A V A = B B × tag C A = tag C
5 4 eleq2d A V A = B x B × tag C A x tag C
6 5 abbidv A V A = B x | x B × tag C A = x | x tag C
7 df-bj-proj A Proj B × tag C = x | x B × tag C A
8 bj-taginv C = x | x tag C
9 6 7 8 3eqtr4g A V A = B A Proj B × tag C = C
10 9 ex A V A = B A Proj B × tag C = C
11 noel ¬ x
12 7 abeq2i x A Proj B × tag C x B × tag C A
13 elsni A B A = B
14 bj-xpima1sn ¬ A B B × tag C A =
15 13 14 nsyl5 ¬ A = B B × tag C A =
16 15 eleq2d ¬ A = B x B × tag C A x
17 12 16 syl5bb ¬ A = B x A Proj B × tag C x
18 11 17 mtbiri ¬ A = B ¬ x A Proj B × tag C
19 18 eq0rdv ¬ A = B A Proj B × tag C =
20 ifval A Proj B × tag C = if A = B C A = B A Proj B × tag C = C ¬ A = B A Proj B × tag C =
21 10 19 20 sylanblrc A V A Proj B × tag C = if A = B C
22 eqcom A = B B = A
23 ifbi A = B B = A if A = B C = if B = A C
24 22 23 ax-mp if A = B C = if B = A C
25 21 24 eqtrdi A V A Proj B × tag C = if B = A C