Step | Hyp | Ref
| Expression |
1 | | brco 4883 |
. . 3
⊢ (x( AddC ∘ ◡(1st ↾ (V × {n})))y ↔
∃z(x◡(1st ↾ (V × {n}))z ∧ z AddC y)) |
2 | | brcnv 4892 |
. . . . . 6
⊢ (x◡(1st ↾ (V × {n}))z ↔
z(1st ↾ (V × {n}))x) |
3 | | brres 4949 |
. . . . . 6
⊢ (z(1st ↾ (V × {n}))x ↔
(z1st x ∧ z ∈ (V ×
{n}))) |
4 | | ancom 437 |
. . . . . . . . 9
⊢ ((z1st x ∧ z ∈ (V ×
{n})) ↔ (z ∈ (V ×
{n}) ∧
z1st x)) |
5 | | elxp2 4802 |
. . . . . . . . . . 11
⊢ (z ∈ (V ×
{n}) ↔ ∃p ∈ V ∃q ∈ {n}z = 〈p, q〉) |
6 | | rexv 2873 |
. . . . . . . . . . 11
⊢ (∃p ∈ V ∃q ∈ {n}z = 〈p, q〉 ↔ ∃p∃q ∈ {n}z = 〈p, q〉) |
7 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ n ∈
V |
8 | | opeq2 4579 |
. . . . . . . . . . . . . 14
⊢ (q = n →
〈p,
q〉 =
〈p,
n〉) |
9 | 8 | eqeq2d 2364 |
. . . . . . . . . . . . 13
⊢ (q = n →
(z = 〈p, q〉 ↔ z = 〈p, n〉)) |
10 | 7, 9 | rexsn 3768 |
. . . . . . . . . . . 12
⊢ (∃q ∈ {n}z = 〈p, q〉 ↔ z =
〈p,
n〉) |
11 | 10 | exbii 1582 |
. . . . . . . . . . 11
⊢ (∃p∃q ∈ {n}z = 〈p, q〉 ↔ ∃p z = 〈p, n〉) |
12 | 5, 6, 11 | 3bitri 262 |
. . . . . . . . . 10
⊢ (z ∈ (V ×
{n}) ↔ ∃p z = 〈p, n〉) |
13 | 12 | anbi1i 676 |
. . . . . . . . 9
⊢ ((z ∈ (V ×
{n}) ∧
z1st x) ↔ (∃p z = 〈p, n〉 ∧ z1st x)) |
14 | 4, 13 | bitri 240 |
. . . . . . . 8
⊢ ((z1st x ∧ z ∈ (V ×
{n})) ↔ (∃p z = 〈p, n〉 ∧ z1st x)) |
15 | | exancom 1586 |
. . . . . . . . 9
⊢ (∃p(z1st x ∧ z = 〈p, n〉) ↔ ∃p(z = 〈p, n〉 ∧ z1st x)) |
16 | | 19.41v 1901 |
. . . . . . . . 9
⊢ (∃p(z = 〈p, n〉 ∧ z1st x) ↔ (∃p z = 〈p, n〉 ∧ z1st x)) |
17 | 15, 16 | bitri 240 |
. . . . . . . 8
⊢ (∃p(z1st x ∧ z = 〈p, n〉) ↔ (∃p z = 〈p, n〉 ∧ z1st x)) |
18 | 14, 17 | bitr4i 243 |
. . . . . . 7
⊢ ((z1st x ∧ z ∈ (V ×
{n})) ↔ ∃p(z1st x ∧ z = 〈p, n〉)) |
19 | | vex 2862 |
. . . . . . . . . . . 12
⊢ x ∈
V |
20 | 19 | br1st 4858 |
. . . . . . . . . . 11
⊢ (z1st x ↔ ∃q z = 〈x, q〉) |
21 | 20 | anbi1i 676 |
. . . . . . . . . 10
⊢ ((z1st x ∧ z = 〈p, n〉) ↔ (∃q z = 〈x, q〉 ∧ z = 〈p, n〉)) |
22 | | 19.41v 1901 |
. . . . . . . . . 10
⊢ (∃q(z = 〈x, q〉 ∧ z = 〈p, n〉) ↔ (∃q z = 〈x, q〉 ∧ z = 〈p, n〉)) |
23 | 21, 22 | bitr4i 243 |
. . . . . . . . 9
⊢ ((z1st x ∧ z = 〈p, n〉) ↔ ∃q(z = 〈x, q〉 ∧ z = 〈p, n〉)) |
24 | 23 | exbii 1582 |
. . . . . . . 8
⊢ (∃p(z1st x ∧ z = 〈p, n〉) ↔ ∃p∃q(z = 〈x, q〉 ∧ z = 〈p, n〉)) |
25 | | eqeq1 2359 |
. . . . . . . . . . . . 13
⊢ (z = 〈p, n〉 → (z =
〈x,
q〉 ↔
〈p,
n〉 =
〈x,
q〉)) |
26 | | opth 4602 |
. . . . . . . . . . . . 13
⊢ (〈p, n〉 = 〈x, q〉 ↔
(p = x
∧ n =
q)) |
27 | 25, 26 | syl6bb 252 |
. . . . . . . . . . . 12
⊢ (z = 〈p, n〉 → (z =
〈x,
q〉 ↔
(p = x
∧ n =
q))) |
28 | 27 | pm5.32ri 619 |
. . . . . . . . . . 11
⊢ ((z = 〈x, q〉 ∧ z = 〈p, n〉) ↔ ((p =
x ∧
n = q)
∧ z =
〈p,
n〉)) |
29 | | equcom 1680 |
. . . . . . . . . . . . 13
⊢ (n = q ↔
q = n) |
30 | 29 | anbi2i 675 |
. . . . . . . . . . . 12
⊢ ((p = x ∧ n = q) ↔ (p =
x ∧
q = n)) |
31 | 30 | anbi1i 676 |
. . . . . . . . . . 11
⊢ (((p = x ∧ n = q) ∧ z = 〈p, n〉) ↔ ((p =
x ∧
q = n)
∧ z =
〈p,
n〉)) |
32 | | opeq2 4579 |
. . . . . . . . . . . . . . 15
⊢ (n = q →
〈p,
n〉 =
〈p,
q〉) |
33 | 32 | equcoms 1681 |
. . . . . . . . . . . . . 14
⊢ (q = n →
〈p,
n〉 =
〈p,
q〉) |
34 | 33 | adantl 452 |
. . . . . . . . . . . . 13
⊢ ((p = x ∧ q = n) → 〈p, n〉 = 〈p, q〉) |
35 | 34 | eqeq2d 2364 |
. . . . . . . . . . . 12
⊢ ((p = x ∧ q = n) → (z =
〈p,
n〉 ↔
z = 〈p, q〉)) |
36 | 35 | pm5.32i 618 |
. . . . . . . . . . 11
⊢ (((p = x ∧ q = n) ∧ z = 〈p, n〉) ↔ ((p =
x ∧
q = n)
∧ z =
〈p,
q〉)) |
37 | 28, 31, 36 | 3bitri 262 |
. . . . . . . . . 10
⊢ ((z = 〈x, q〉 ∧ z = 〈p, n〉) ↔ ((p =
x ∧
q = n)
∧ z =
〈p,
q〉)) |
38 | | df-3an 936 |
. . . . . . . . . 10
⊢ ((p = x ∧ q = n ∧ z = 〈p, q〉) ↔ ((p =
x ∧
q = n)
∧ z =
〈p,
q〉)) |
39 | 37, 38 | bitr4i 243 |
. . . . . . . . 9
⊢ ((z = 〈x, q〉 ∧ z = 〈p, n〉) ↔ (p =
x ∧
q = n
∧ z =
〈p,
q〉)) |
40 | 39 | 2exbii 1583 |
. . . . . . . 8
⊢ (∃p∃q(z = 〈x, q〉 ∧ z = 〈p, n〉) ↔ ∃p∃q(p = x ∧ q = n ∧ z = 〈p, q〉)) |
41 | 24, 40 | bitri 240 |
. . . . . . 7
⊢ (∃p(z1st x ∧ z = 〈p, n〉) ↔ ∃p∃q(p = x ∧ q = n ∧ z = 〈p, q〉)) |
42 | | opeq1 4578 |
. . . . . . . . 9
⊢ (p = x →
〈p,
q〉 =
〈x,
q〉) |
43 | 42 | eqeq2d 2364 |
. . . . . . . 8
⊢ (p = x →
(z = 〈p, q〉 ↔ z = 〈x, q〉)) |
44 | | opeq2 4579 |
. . . . . . . . 9
⊢ (q = n →
〈x,
q〉 =
〈x,
n〉) |
45 | 44 | eqeq2d 2364 |
. . . . . . . 8
⊢ (q = n →
(z = 〈x, q〉 ↔ z = 〈x, n〉)) |
46 | 19, 7, 43, 45 | ceqsex2v 2896 |
. . . . . . 7
⊢ (∃p∃q(p = x ∧ q = n ∧ z = 〈p, q〉) ↔ z =
〈x,
n〉) |
47 | 18, 41, 46 | 3bitri 262 |
. . . . . 6
⊢ ((z1st x ∧ z ∈ (V ×
{n})) ↔ z = 〈x, n〉) |
48 | 2, 3, 47 | 3bitri 262 |
. . . . 5
⊢ (x◡(1st ↾ (V × {n}))z ↔
z = 〈x, n〉) |
49 | 48 | anbi1i 676 |
. . . 4
⊢ ((x◡(1st ↾ (V × {n}))z ∧ z AddC y) ↔
(z = 〈x, n〉 ∧ z AddC y)) |
50 | 49 | exbii 1582 |
. . 3
⊢ (∃z(x◡(1st ↾ (V × {n}))z ∧ z AddC y) ↔ ∃z(z = 〈x, n〉 ∧ z AddC y)) |
51 | 19, 7 | opex 4588 |
. . . 4
⊢ 〈x, n〉 ∈ V |
52 | | breq1 4642 |
. . . 4
⊢ (z = 〈x, n〉 → (z
AddC y ↔
〈x,
n〉 AddC y)) |
53 | 51, 52 | ceqsexv 2894 |
. . 3
⊢ (∃z(z = 〈x, n〉 ∧ z AddC y) ↔ 〈x, n〉 AddC y) |
54 | 1, 50, 53 | 3bitri 262 |
. 2
⊢ (x( AddC ∘ ◡(1st ↾ (V × {n})))y ↔
〈x,
n〉 AddC y) |
55 | 19, 7 | braddcfn 5826 |
. 2
⊢ (〈x, n〉 AddC y ↔
(x +c n) = y) |
56 | | eqcom 2355 |
. 2
⊢ ((x +c n) = y ↔
y = (x
+c n)) |
57 | 54, 55, 56 | 3bitri 262 |
1
⊢ (x( AddC ∘ ◡(1st ↾ (V × {n})))y ↔
y = (x
+c n)) |