Theorem bj-projval

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

	Ref	Expression
Assertion	bj-projval	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 Proj ( { 𝐵 } × tag 𝐶 ) ) = if ( 𝐵 = 𝐴 , 𝐶 , ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		elsng	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 } ↔ 𝐴 = 𝐵 ) )
2		bj-xpima2sn	⊢ ( 𝐴 ∈ { 𝐵 } → ( ( { 𝐵 } × tag 𝐶 ) “ { 𝐴 } ) = tag 𝐶 )
3	1 2	syl6bir	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 → ( ( { 𝐵 } × tag 𝐶 ) “ { 𝐴 } ) = tag 𝐶 ) )
4	3	imp	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → ( ( { 𝐵 } × tag 𝐶 ) “ { 𝐴 } ) = tag 𝐶 )
5	4	eleq2d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → ( { 𝑥 } ∈ ( ( { 𝐵 } × tag 𝐶 ) “ { 𝐴 } ) ↔ { 𝑥 } ∈ tag 𝐶 ) )
6	5	abbidv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → { 𝑥 ∣ { 𝑥 } ∈ ( ( { 𝐵 } × tag 𝐶 ) “ { 𝐴 } ) } = { 𝑥 ∣ { 𝑥 } ∈ tag 𝐶 } )
7		df-bj-proj	⊢ ( 𝐴 Proj ( { 𝐵 } × tag 𝐶 ) ) = { 𝑥 ∣ { 𝑥 } ∈ ( ( { 𝐵 } × tag 𝐶 ) “ { 𝐴 } ) }
8		bj-taginv	⊢ 𝐶 = { 𝑥 ∣ { 𝑥 } ∈ tag 𝐶 }
9	6 7 8	3eqtr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → ( 𝐴 Proj ( { 𝐵 } × tag 𝐶 ) ) = 𝐶 )
10	9	ex	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 → ( 𝐴 Proj ( { 𝐵 } × tag 𝐶 ) ) = 𝐶 ) )
11		noel	⊢ ¬ { 𝑥 } ∈ ∅
12	7	abeq2i	⊢ ( 𝑥 ∈ ( 𝐴 Proj ( { 𝐵 } × tag 𝐶 ) ) ↔ { 𝑥 } ∈ ( ( { 𝐵 } × tag 𝐶 ) “ { 𝐴 } ) )
13		elsni	⊢ ( 𝐴 ∈ { 𝐵 } → 𝐴 = 𝐵 )
14		bj-xpima1sn	⊢ ( ¬ 𝐴 ∈ { 𝐵 } → ( ( { 𝐵 } × tag 𝐶 ) “ { 𝐴 } ) = ∅ )
15	13 14	nsyl5	⊢ ( ¬ 𝐴 = 𝐵 → ( ( { 𝐵 } × tag 𝐶 ) “ { 𝐴 } ) = ∅ )
16	15	eleq2d	⊢ ( ¬ 𝐴 = 𝐵 → ( { 𝑥 } ∈ ( ( { 𝐵 } × tag 𝐶 ) “ { 𝐴 } ) ↔ { 𝑥 } ∈ ∅ ) )
17	12 16	syl5bb	⊢ ( ¬ 𝐴 = 𝐵 → ( 𝑥 ∈ ( 𝐴 Proj ( { 𝐵 } × tag 𝐶 ) ) ↔ { 𝑥 } ∈ ∅ ) )
18	11 17	mtbiri	⊢ ( ¬ 𝐴 = 𝐵 → ¬ 𝑥 ∈ ( 𝐴 Proj ( { 𝐵 } × tag 𝐶 ) ) )
19	18	eq0rdv	⊢ ( ¬ 𝐴 = 𝐵 → ( 𝐴 Proj ( { 𝐵 } × tag 𝐶 ) ) = ∅ )
20		ifval	⊢ ( ( 𝐴 Proj ( { 𝐵 } × tag 𝐶 ) ) = if ( 𝐴 = 𝐵 , 𝐶 , ∅ ) ↔ ( ( 𝐴 = 𝐵 → ( 𝐴 Proj ( { 𝐵 } × tag 𝐶 ) ) = 𝐶 ) ∧ ( ¬ 𝐴 = 𝐵 → ( 𝐴 Proj ( { 𝐵 } × tag 𝐶 ) ) = ∅ ) ) )
21	10 19 20	sylanblrc	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 Proj ( { 𝐵 } × tag 𝐶 ) ) = if ( 𝐴 = 𝐵 , 𝐶 , ∅ ) )
22		eqcom	⊢ ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 )
23		ifbi	⊢ ( ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 ) → if ( 𝐴 = 𝐵 , 𝐶 , ∅ ) = if ( 𝐵 = 𝐴 , 𝐶 , ∅ ) )
24	22 23	ax-mp	⊢ if ( 𝐴 = 𝐵 , 𝐶 , ∅ ) = if ( 𝐵 = 𝐴 , 𝐶 , ∅ )
25	21 24	eqtrdi	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 Proj ( { 𝐵 } × tag 𝐶 ) ) = if ( 𝐵 = 𝐴 , 𝐶 , ∅ ) )