Metamath Proof Explorer

Theorem bj-projval

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

Ref Expression
Assertion bj-projval 
|- ( A e. V -> ( A Proj ( { B } X. tag C ) ) = if ( B = A , C , (/) ) )

Proof

Step Hyp Ref Expression
1 elsng 
 |-  ( A e. V -> ( A e. { B } <-> A = B ) )
2 bj-xpima2sn 
 |-  ( A e. { B } -> ( ( { B } X. tag C ) " { A } ) = tag C )
3 1 2 syl6bir 
 |-  ( A e. V -> ( A = B -> ( ( { B } X. tag C ) " { A } ) = tag C ) )
4 3 imp 
 |-  ( ( A e. V /\ A = B ) -> ( ( { B } X. tag C ) " { A } ) = tag C )
5 4 eleq2d 
 |-  ( ( A e. V /\ A = B ) -> ( { x } e. ( ( { B } X. tag C ) " { A } ) <-> { x } e. tag C ) )
6 5 abbidv 
 |-  ( ( A e. V /\ A = B ) -> { x | { x } e. ( ( { B } X. tag C ) " { A } ) } = { x | { x } e. tag C } )
7 df-bj-proj 
 |-  ( A Proj ( { B } X. tag C ) ) = { x | { x } e. ( ( { B } X. tag C ) " { A } ) }
8 bj-taginv 
 |-  C = { x | { x } e. tag C }
9 6 7 8 3eqtr4g 
 |-  ( ( A e. V /\ A = B ) -> ( A Proj ( { B } X. tag C ) ) = C )
10 9 ex 
 |-  ( A e. V -> ( A = B -> ( A Proj ( { B } X. tag C ) ) = C ) )
11 noel 
 |-  -. { x } e. (/)
12 7 abeq2i 
 |-  ( x e. ( A Proj ( { B } X. tag C ) ) <-> { x } e. ( ( { B } X. tag C ) " { A } ) )
13 elsni 
 |-  ( A e. { B } -> A = B )
14 bj-xpima1sn 
 |-  ( -. A e. { B } -> ( ( { B } X. tag C ) " { A } ) = (/) )
15 13 14 nsyl5 
 |-  ( -. A = B -> ( ( { B } X. tag C ) " { A } ) = (/) )
16 15 eleq2d 
 |-  ( -. A = B -> ( { x } e. ( ( { B } X. tag C ) " { A } ) <-> { x } e. (/) ) )
17 12 16 syl5bb 
 |-  ( -. A = B -> ( x e. ( A Proj ( { B } X. tag C ) ) <-> { x } e. (/) ) )
18 11 17 mtbiri 
 |-  ( -. A = B -> -. x e. ( A Proj ( { B } X. tag C ) ) )
19 18 eq0rdv 
 |-  ( -. A = B -> ( A Proj ( { B } X. tag C ) ) = (/) )
20 ifval 
 |-  ( ( A Proj ( { B } X. tag C ) ) = if ( A = B , C , (/) ) <-> ( ( A = B -> ( A Proj ( { B } X. tag C ) ) = C ) /\ ( -. A = B -> ( A Proj ( { B } X. tag C ) ) = (/) ) ) )
21 10 19 20 sylanblrc 
 |-  ( A e. V -> ( A Proj ( { B } X. 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 e. V -> ( A Proj ( { B } X. tag C ) ) = if ( B = A , C , (/) ) )