Step | Hyp | Ref
| Expression |
1 | | plusffval.3 |
. 2
⊢ ⨣ =
(+𝑓‘𝐺) |
2 | | fveq2 6103 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
3 | | plusffval.1 |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
4 | 2, 3 | syl6eqr 2662 |
. . . . 5
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝐵) |
5 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (+g‘𝑔) = (+g‘𝐺)) |
6 | | plusffval.2 |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
7 | 5, 6 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (+g‘𝑔) = + ) |
8 | 7 | oveqd 6566 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝑥(+g‘𝑔)𝑦) = (𝑥 + 𝑦)) |
9 | 4, 4, 8 | mpt2eq123dv 6615 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦))) |
10 | | df-plusf 17064 |
. . . 4
⊢
+𝑓 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)𝑦))) |
11 | | df-ov 6552 |
. . . . . . . 8
⊢ (𝑥 + 𝑦) = ( + ‘〈𝑥, 𝑦〉) |
12 | | fvrn0 6126 |
. . . . . . . 8
⊢ ( +
‘〈𝑥, 𝑦〉) ∈ (ran + ∪
{∅}) |
13 | 11, 12 | eqeltri 2684 |
. . . . . . 7
⊢ (𝑥 + 𝑦) ∈ (ran + ∪
{∅}) |
14 | 13 | rgen2w 2909 |
. . . . . 6
⊢
∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) ∈ (ran + ∪
{∅}) |
15 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)) |
16 | 15 | fmpt2 7126 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) ∈ (ran + ∪ {∅}) ↔
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)):(𝐵 × 𝐵)⟶(ran + ∪
{∅})) |
17 | 14, 16 | mpbi 219 |
. . . . 5
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)):(𝐵 × 𝐵)⟶(ran + ∪
{∅}) |
18 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐺)
∈ V |
19 | 3, 18 | eqeltri 2684 |
. . . . . 6
⊢ 𝐵 ∈ V |
20 | 19, 19 | xpex 6860 |
. . . . 5
⊢ (𝐵 × 𝐵) ∈ V |
21 | | fvex 6113 |
. . . . . . . 8
⊢
(+g‘𝐺) ∈ V |
22 | 6, 21 | eqeltri 2684 |
. . . . . . 7
⊢ + ∈
V |
23 | 22 | rnex 6992 |
. . . . . 6
⊢ ran + ∈
V |
24 | | p0ex 4779 |
. . . . . 6
⊢ {∅}
∈ V |
25 | 23, 24 | unex 6854 |
. . . . 5
⊢ (ran
+ ∪
{∅}) ∈ V |
26 | | fex2 7014 |
. . . . 5
⊢ (((𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)):(𝐵 × 𝐵)⟶(ran + ∪ {∅}) ∧
(𝐵 × 𝐵) ∈ V ∧ (ran + ∪
{∅}) ∈ V) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)) ∈ V) |
27 | 17, 20, 25, 26 | mp3an 1416 |
. . . 4
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)) ∈ V |
28 | 9, 10, 27 | fvmpt 6191 |
. . 3
⊢ (𝐺 ∈ V →
(+𝑓‘𝐺) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦))) |
29 | | fvprc 6097 |
. . . . 5
⊢ (¬
𝐺 ∈ V →
(+𝑓‘𝐺) = ∅) |
30 | | mpt20 6623 |
. . . . 5
⊢ (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑥 + 𝑦)) = ∅ |
31 | 29, 30 | syl6eqr 2662 |
. . . 4
⊢ (¬
𝐺 ∈ V →
(+𝑓‘𝐺) = (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑥 + 𝑦))) |
32 | | fvprc 6097 |
. . . . . 6
⊢ (¬
𝐺 ∈ V →
(Base‘𝐺) =
∅) |
33 | 3, 32 | syl5eq 2656 |
. . . . 5
⊢ (¬
𝐺 ∈ V → 𝐵 = ∅) |
34 | | mpt2eq12 6613 |
. . . . 5
⊢ ((𝐵 = ∅ ∧ 𝐵 = ∅) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)) = (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑥 + 𝑦))) |
35 | 33, 33, 34 | syl2anc 691 |
. . . 4
⊢ (¬
𝐺 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)) = (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑥 + 𝑦))) |
36 | 31, 35 | eqtr4d 2647 |
. . 3
⊢ (¬
𝐺 ∈ V →
(+𝑓‘𝐺) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦))) |
37 | 28, 36 | pm2.61i 175 |
. 2
⊢
(+𝑓‘𝐺) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)) |
38 | 1, 37 | eqtri 2632 |
1
⊢ ⨣ =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)) |