Step | Hyp | Ref
| Expression |
1 | | elsng 4581 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) |
2 | | bj-xpima2sn 34273 |
. . . . . . . . 9
⊢ (𝐴 ∈ {𝐵} → (({𝐵} × tag 𝐶) “ {𝐴}) = tag 𝐶) |
3 | 1, 2 | syl6bir 256 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → (({𝐵} × tag 𝐶) “ {𝐴}) = tag 𝐶)) |
4 | 3 | imp 409 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵) → (({𝐵} × tag 𝐶) “ {𝐴}) = tag 𝐶) |
5 | 4 | eleq2d 2898 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵) → ({𝑥} ∈ (({𝐵} × tag 𝐶) “ {𝐴}) ↔ {𝑥} ∈ tag 𝐶)) |
6 | 5 | abbidv 2885 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵) → {𝑥 ∣ {𝑥} ∈ (({𝐵} × tag 𝐶) “ {𝐴})} = {𝑥 ∣ {𝑥} ∈ tag 𝐶}) |
7 | | df-bj-proj 34306 |
. . . . 5
⊢ (𝐴 Proj ({𝐵} × tag 𝐶)) = {𝑥 ∣ {𝑥} ∈ (({𝐵} × tag 𝐶) “ {𝐴})} |
8 | | bj-taginv 34301 |
. . . . 5
⊢ 𝐶 = {𝑥 ∣ {𝑥} ∈ tag 𝐶} |
9 | 6, 7, 8 | 3eqtr4g 2881 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵) → (𝐴 Proj ({𝐵} × tag 𝐶)) = 𝐶) |
10 | 9 | ex 415 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → (𝐴 Proj ({𝐵} × tag 𝐶)) = 𝐶)) |
11 | | noel 4296 |
. . . . 5
⊢ ¬
{𝑥} ∈
∅ |
12 | 7 | abeq2i 2948 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 Proj ({𝐵} × tag 𝐶)) ↔ {𝑥} ∈ (({𝐵} × tag 𝐶) “ {𝐴})) |
13 | | elsni 4584 |
. . . . . . . . 9
⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) |
14 | 13 | con3i 157 |
. . . . . . . 8
⊢ (¬
𝐴 = 𝐵 → ¬ 𝐴 ∈ {𝐵}) |
15 | | bj-xpima1sn 34271 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ {𝐵} → (({𝐵} × tag 𝐶) “ {𝐴}) = ∅) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (¬
𝐴 = 𝐵 → (({𝐵} × tag 𝐶) “ {𝐴}) = ∅) |
17 | 16 | eleq2d 2898 |
. . . . . 6
⊢ (¬
𝐴 = 𝐵 → ({𝑥} ∈ (({𝐵} × tag 𝐶) “ {𝐴}) ↔ {𝑥} ∈ ∅)) |
18 | 12, 17 | syl5bb 285 |
. . . . 5
⊢ (¬
𝐴 = 𝐵 → (𝑥 ∈ (𝐴 Proj ({𝐵} × tag 𝐶)) ↔ {𝑥} ∈ ∅)) |
19 | 11, 18 | mtbiri 329 |
. . . 4
⊢ (¬
𝐴 = 𝐵 → ¬ 𝑥 ∈ (𝐴 Proj ({𝐵} × tag 𝐶))) |
20 | 19 | eq0rdv 4357 |
. . 3
⊢ (¬
𝐴 = 𝐵 → (𝐴 Proj ({𝐵} × tag 𝐶)) = ∅) |
21 | | ifval 4508 |
. . 3
⊢ ((𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐴 = 𝐵, 𝐶, ∅) ↔ ((𝐴 = 𝐵 → (𝐴 Proj ({𝐵} × tag 𝐶)) = 𝐶) ∧ (¬ 𝐴 = 𝐵 → (𝐴 Proj ({𝐵} × tag 𝐶)) = ∅))) |
22 | 10, 20, 21 | sylanblrc 592 |
. 2
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐴 = 𝐵, 𝐶, ∅)) |
23 | | eqcom 2828 |
. . 3
⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) |
24 | | ifbi 4488 |
. . 3
⊢ ((𝐴 = 𝐵 ↔ 𝐵 = 𝐴) → if(𝐴 = 𝐵, 𝐶, ∅) = if(𝐵 = 𝐴, 𝐶, ∅)) |
25 | 23, 24 | ax-mp 5 |
. 2
⊢ if(𝐴 = 𝐵, 𝐶, ∅) = if(𝐵 = 𝐴, 𝐶, ∅) |
26 | 22, 25 | syl6eq 2872 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐵 = 𝐴, 𝐶, ∅)) |