Step | Hyp | Ref
| Expression |
1 | | fvpr0o 17505 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅) = 𝐴) |
2 | 1 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) →
({⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩}‘∅) = 𝐴) |
3 | 2 | adantr 482 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = ∅) →
({⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩}‘∅) = 𝐴) |
4 | | simpr 486 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = ∅) → 𝐶 = ∅) |
5 | 4 | fveq2d 6896 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = ∅) →
({⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩}‘𝐶) = ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅)) |
6 | 4 | iftrued 4537 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = ∅) → if(𝐶 = ∅, 𝐴, 𝐵) = 𝐴) |
7 | 3, 5, 6 | 3eqtr4d 2783 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = ∅) →
({⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩}‘𝐶) = if(𝐶 = ∅, 𝐴, 𝐵)) |
8 | | fvpr1o 17506 |
. . . . 5
⊢ (𝐵 ∈ 𝑊 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o) =
𝐵) |
9 | 8 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) →
({⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩}‘1o) = 𝐵) |
10 | 9 | adantr 482 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) →
({⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩}‘1o) = 𝐵) |
11 | | simpr 486 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) → 𝐶 =
1o) |
12 | 11 | fveq2d 6896 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) →
({⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩}‘𝐶) = ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o)) |
13 | | 1n0 8488 |
. . . . . 6
⊢
1o ≠ ∅ |
14 | 13 | neii 2943 |
. . . . 5
⊢ ¬
1o = ∅ |
15 | 11 | eqeq1d 2735 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) → (𝐶 = ∅ ↔ 1o
= ∅)) |
16 | 14, 15 | mtbiri 327 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) → ¬
𝐶 =
∅) |
17 | 16 | iffalsed 4540 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) →
if(𝐶 = ∅, 𝐴, 𝐵) = 𝐵) |
18 | 10, 12, 17 | 3eqtr4d 2783 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) →
({⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩}‘𝐶) = if(𝐶 = ∅, 𝐴, 𝐵)) |
19 | | elpri 4651 |
. . . 4
⊢ (𝐶 ∈ {∅, 1o}
→ (𝐶 = ∅ ∨
𝐶 =
1o)) |
20 | | df2o3 8474 |
. . . 4
⊢
2o = {∅, 1o} |
21 | 19, 20 | eleq2s 2852 |
. . 3
⊢ (𝐶 ∈ 2o →
(𝐶 = ∅ ∨ 𝐶 =
1o)) |
22 | 21 | 3ad2ant3 1136 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) → (𝐶 = ∅ ∨ 𝐶 =
1o)) |
23 | 7, 18, 22 | mpjaodan 958 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) →
({⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩}‘𝐶) = if(𝐶 = ∅, 𝐴, 𝐵)) |