Step | Hyp | Ref
| Expression |
1 | | elsng 4191 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) |
2 | | bj-xpima2sn 32945 |
. . . . . . . . 9
⊢ (𝐴 ∈ {𝐵} → (({𝐵} × tag 𝐶) “ {𝐴}) = tag 𝐶) |
3 | 1, 2 | syl6bir 244 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → (({𝐵} × tag 𝐶) “ {𝐴}) = tag 𝐶)) |
4 | 3 | imp 445 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵) → (({𝐵} × tag 𝐶) “ {𝐴}) = tag 𝐶) |
5 | 4 | eleq2d 2687 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵) → ({𝑥} ∈ (({𝐵} × tag 𝐶) “ {𝐴}) ↔ {𝑥} ∈ tag 𝐶)) |
6 | 5 | abbidv 2741 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵) → {𝑥 ∣ {𝑥} ∈ (({𝐵} × tag 𝐶) “ {𝐴})} = {𝑥 ∣ {𝑥} ∈ tag 𝐶}) |
7 | | df-bj-proj 32979 |
. . . . 5
⊢ (𝐴 Proj ({𝐵} × tag 𝐶)) = {𝑥 ∣ {𝑥} ∈ (({𝐵} × tag 𝐶) “ {𝐴})} |
8 | | bj-taginv 32974 |
. . . . 5
⊢ 𝐶 = {𝑥 ∣ {𝑥} ∈ tag 𝐶} |
9 | 6, 7, 8 | 3eqtr4g 2681 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 = 𝐵) → (𝐴 Proj ({𝐵} × tag 𝐶)) = 𝐶) |
10 | 9 | ex 450 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → (𝐴 Proj ({𝐵} × tag 𝐶)) = 𝐶)) |
11 | | noel 3919 |
. . . . 5
⊢ ¬
{𝑥} ∈
∅ |
12 | 7 | abeq2i 2735 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 Proj ({𝐵} × tag 𝐶)) ↔ {𝑥} ∈ (({𝐵} × tag 𝐶) “ {𝐴})) |
13 | | elsni 4194 |
. . . . . . . . . 10
⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) |
14 | 13 | con3i 150 |
. . . . . . . . 9
⊢ (¬
𝐴 = 𝐵 → ¬ 𝐴 ∈ {𝐵}) |
15 | | df-nel 2898 |
. . . . . . . . 9
⊢ (𝐴 ∉ {𝐵} ↔ ¬ 𝐴 ∈ {𝐵}) |
16 | 14, 15 | sylibr 224 |
. . . . . . . 8
⊢ (¬
𝐴 = 𝐵 → 𝐴 ∉ {𝐵}) |
17 | | bj-xpima1sn 32943 |
. . . . . . . 8
⊢ (𝐴 ∉ {𝐵} → (({𝐵} × tag 𝐶) “ {𝐴}) = ∅) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (¬
𝐴 = 𝐵 → (({𝐵} × tag 𝐶) “ {𝐴}) = ∅) |
19 | 18 | eleq2d 2687 |
. . . . . 6
⊢ (¬
𝐴 = 𝐵 → ({𝑥} ∈ (({𝐵} × tag 𝐶) “ {𝐴}) ↔ {𝑥} ∈ ∅)) |
20 | 12, 19 | syl5bb 272 |
. . . . 5
⊢ (¬
𝐴 = 𝐵 → (𝑥 ∈ (𝐴 Proj ({𝐵} × tag 𝐶)) ↔ {𝑥} ∈ ∅)) |
21 | 11, 20 | mtbiri 317 |
. . . 4
⊢ (¬
𝐴 = 𝐵 → ¬ 𝑥 ∈ (𝐴 Proj ({𝐵} × tag 𝐶))) |
22 | 21 | eq0rdv 3979 |
. . 3
⊢ (¬
𝐴 = 𝐵 → (𝐴 Proj ({𝐵} × tag 𝐶)) = ∅) |
23 | | ifval 4127 |
. . 3
⊢ ((𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐴 = 𝐵, 𝐶, ∅) ↔ ((𝐴 = 𝐵 → (𝐴 Proj ({𝐵} × tag 𝐶)) = 𝐶) ∧ (¬ 𝐴 = 𝐵 → (𝐴 Proj ({𝐵} × tag 𝐶)) = ∅))) |
24 | 10, 22, 23 | sylanblrc 697 |
. 2
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐴 = 𝐵, 𝐶, ∅)) |
25 | | eqcom 2629 |
. . 3
⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) |
26 | | ifbi 4107 |
. . 3
⊢ ((𝐴 = 𝐵 ↔ 𝐵 = 𝐴) → if(𝐴 = 𝐵, 𝐶, ∅) = if(𝐵 = 𝐴, 𝐶, ∅)) |
27 | 25, 26 | ax-mp 5 |
. 2
⊢ if(𝐴 = 𝐵, 𝐶, ∅) = if(𝐵 = 𝐴, 𝐶, ∅) |
28 | 24, 27 | syl6eq 2672 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐵 = 𝐴, 𝐶, ∅)) |