Proof of Theorem fvprif
| Step | Hyp | Ref
| Expression |
| 1 | | fvpr0o 17604 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ({〈∅, 𝐴〉, 〈1o, 𝐵〉}‘∅) = 𝐴) |
| 2 | 1 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) →
({〈∅, 𝐴〉,
〈1o, 𝐵〉}‘∅) = 𝐴) |
| 3 | 2 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = ∅) →
({〈∅, 𝐴〉,
〈1o, 𝐵〉}‘∅) = 𝐴) |
| 4 | | simpr 484 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = ∅) → 𝐶 = ∅) |
| 5 | 4 | fveq2d 6910 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = ∅) →
({〈∅, 𝐴〉,
〈1o, 𝐵〉}‘𝐶) = ({〈∅, 𝐴〉, 〈1o, 𝐵〉}‘∅)) |
| 6 | 4 | iftrued 4533 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = ∅) → if(𝐶 = ∅, 𝐴, 𝐵) = 𝐴) |
| 7 | 3, 5, 6 | 3eqtr4d 2787 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = ∅) →
({〈∅, 𝐴〉,
〈1o, 𝐵〉}‘𝐶) = if(𝐶 = ∅, 𝐴, 𝐵)) |
| 8 | | fvpr1o 17605 |
. . . . 5
⊢ (𝐵 ∈ 𝑊 → ({〈∅, 𝐴〉, 〈1o, 𝐵〉}‘1o) =
𝐵) |
| 9 | 8 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) →
({〈∅, 𝐴〉,
〈1o, 𝐵〉}‘1o) = 𝐵) |
| 10 | 9 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) →
({〈∅, 𝐴〉,
〈1o, 𝐵〉}‘1o) = 𝐵) |
| 11 | | simpr 484 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) → 𝐶 =
1o) |
| 12 | 11 | fveq2d 6910 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) →
({〈∅, 𝐴〉,
〈1o, 𝐵〉}‘𝐶) = ({〈∅, 𝐴〉, 〈1o, 𝐵〉}‘1o)) |
| 13 | | 1n0 8526 |
. . . . . 6
⊢
1o ≠ ∅ |
| 14 | 13 | neii 2942 |
. . . . 5
⊢ ¬
1o = ∅ |
| 15 | 11 | eqeq1d 2739 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) → (𝐶 = ∅ ↔ 1o
= ∅)) |
| 16 | 14, 15 | mtbiri 327 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) → ¬
𝐶 =
∅) |
| 17 | 16 | iffalsed 4536 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) →
if(𝐶 = ∅, 𝐴, 𝐵) = 𝐵) |
| 18 | 10, 12, 17 | 3eqtr4d 2787 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) ∧ 𝐶 = 1o) →
({〈∅, 𝐴〉,
〈1o, 𝐵〉}‘𝐶) = if(𝐶 = ∅, 𝐴, 𝐵)) |
| 19 | | elpri 4649 |
. . . 4
⊢ (𝐶 ∈ {∅, 1o}
→ (𝐶 = ∅ ∨
𝐶 =
1o)) |
| 20 | | df2o3 8514 |
. . . 4
⊢
2o = {∅, 1o} |
| 21 | 19, 20 | eleq2s 2859 |
. . 3
⊢ (𝐶 ∈ 2o →
(𝐶 = ∅ ∨ 𝐶 =
1o)) |
| 22 | 21 | 3ad2ant3 1136 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) → (𝐶 = ∅ ∨ 𝐶 =
1o)) |
| 23 | 7, 18, 22 | mpjaodan 961 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) →
({〈∅, 𝐴〉,
〈1o, 𝐵〉}‘𝐶) = if(𝐶 = ∅, 𝐴, 𝐵)) |