Step | Hyp | Ref
| Expression |
1 | | unab 3521 |
. . 3
⊢ ({x ∣ ¬
(x +c N) = (x
+c P)} ∪ {x ∣ N = P}) =
{x ∣
(¬ (x +c N) = (x
+c P) ∨ N = P)} |
2 | | complab 3524 |
. . . 4
⊢ ∼ {x ∣ (x +c N) = (x
+c P)} = {x ∣ ¬
(x +c N) = (x
+c P)} |
3 | 2 | uneq1i 3414 |
. . 3
⊢ ( ∼ {x ∣ (x +c N) = (x
+c P)} ∪ {x ∣ N = P}) =
({x ∣
¬ (x +c N) = (x
+c P)} ∪ {x ∣ N = P}) |
4 | | imor 401 |
. . . 4
⊢ (((x +c N) = (x
+c P) → N = P) ↔
(¬ (x +c N) = (x
+c P) ∨ N = P)) |
5 | 4 | abbii 2465 |
. . 3
⊢ {x ∣ ((x +c N) = (x
+c P) → N = P)} =
{x ∣
(¬ (x +c N) = (x
+c P) ∨ N = P)} |
6 | 1, 3, 5 | 3eqtr4i 2383 |
. 2
⊢ ( ∼ {x ∣ (x +c N) = (x
+c P)} ∪ {x ∣ N = P}) =
{x ∣
((x +c N) = (x
+c P) → N = P)} |
7 | | addceq2 4384 |
. . . . . . . 8
⊢ (n = N →
(x +c n) = (x
+c N)) |
8 | 7 | eqeq1d 2361 |
. . . . . . 7
⊢ (n = N →
((x +c n) = (x
+c p) ↔ (x +c N) = (x
+c p))) |
9 | 8 | abbidv 2467 |
. . . . . 6
⊢ (n = N →
{x ∣
(x +c n) = (x
+c p)} = {x ∣ (x +c N) = (x
+c p)}) |
10 | 9 | eleq1d 2419 |
. . . . 5
⊢ (n = N →
({x ∣
(x +c n) = (x
+c p)} ∈ V ↔ {x
∣ (x
+c N) = (x +c p)} ∈
V)) |
11 | | addceq2 4384 |
. . . . . . . 8
⊢ (p = P →
(x +c p) = (x
+c P)) |
12 | 11 | eqeq2d 2364 |
. . . . . . 7
⊢ (p = P →
((x +c N) = (x
+c p) ↔ (x +c N) = (x
+c P))) |
13 | 12 | abbidv 2467 |
. . . . . 6
⊢ (p = P →
{x ∣
(x +c N) = (x
+c p)} = {x ∣ (x +c N) = (x
+c P)}) |
14 | 13 | eleq1d 2419 |
. . . . 5
⊢ (p = P →
({x ∣
(x +c N) = (x
+c p)} ∈ V ↔ {x
∣ (x
+c N) = (x +c P)} ∈
V)) |
15 | | elfix 5787 |
. . . . . . . 8
⊢ (x ∈ Fix (◡( AddC ∘ ◡(1st ↾ (V × {p}))) ∘ ( AddC ∘ ◡(1st ↾ (V × {n})))) ↔ x(◡( AddC ∘ ◡(1st ↾ (V × {p}))) ∘ ( AddC ∘ ◡(1st ↾ (V × {n}))))x) |
16 | | brco 4883 |
. . . . . . . . 9
⊢ (x(◡( AddC ∘ ◡(1st ↾ (V × {p}))) ∘ ( AddC ∘ ◡(1st ↾ (V × {n}))))x ↔
∃y(x( AddC ∘ ◡(1st ↾ (V × {n})))y ∧ y◡( AddC ∘ ◡(1st ↾ (V × {p})))x)) |
17 | | addccan2nclem1 6263 |
. . . . . . . . . . 11
⊢ (x( AddC ∘ ◡(1st ↾ (V × {n})))y ↔
y = (x
+c n)) |
18 | | brcnv 4892 |
. . . . . . . . . . . 12
⊢ (y◡( AddC ∘ ◡(1st ↾ (V × {p})))x ↔
x( AddC ∘ ◡(1st ↾ (V × {p})))y) |
19 | | addccan2nclem1 6263 |
. . . . . . . . . . . 12
⊢ (x( AddC ∘ ◡(1st ↾ (V × {p})))y ↔
y = (x
+c p)) |
20 | 18, 19 | bitri 240 |
. . . . . . . . . . 11
⊢ (y◡( AddC ∘ ◡(1st ↾ (V × {p})))x ↔
y = (x
+c p)) |
21 | 17, 20 | anbi12i 678 |
. . . . . . . . . 10
⊢ ((x( AddC ∘ ◡(1st ↾ (V × {n})))y ∧ y◡( AddC ∘ ◡(1st ↾ (V × {p})))x) ↔
(y = (x
+c n) ∧ y = (x +c p))) |
22 | 21 | exbii 1582 |
. . . . . . . . 9
⊢ (∃y(x( AddC ∘ ◡(1st ↾ (V × {n})))y ∧ y◡( AddC ∘ ◡(1st ↾ (V × {p})))x) ↔
∃y(y = (x +c n) ∧ y = (x
+c p))) |
23 | 16, 22 | bitri 240 |
. . . . . . . 8
⊢ (x(◡( AddC ∘ ◡(1st ↾ (V × {p}))) ∘ ( AddC ∘ ◡(1st ↾ (V × {n}))))x ↔
∃y(y = (x +c n) ∧ y = (x
+c p))) |
24 | | vex 2862 |
. . . . . . . . . 10
⊢ x ∈
V |
25 | | vex 2862 |
. . . . . . . . . 10
⊢ n ∈
V |
26 | 24, 25 | addcex 4394 |
. . . . . . . . 9
⊢ (x +c n) ∈
V |
27 | | eqeq1 2359 |
. . . . . . . . 9
⊢ (y = (x
+c n) → (y = (x
+c p) ↔ (x +c n) = (x
+c p))) |
28 | 26, 27 | ceqsexv 2894 |
. . . . . . . 8
⊢ (∃y(y = (x
+c n) ∧ y = (x +c p)) ↔ (x
+c n) = (x +c p)) |
29 | 15, 23, 28 | 3bitri 262 |
. . . . . . 7
⊢ (x ∈ Fix (◡( AddC ∘ ◡(1st ↾ (V × {p}))) ∘ ( AddC ∘ ◡(1st ↾ (V × {n})))) ↔ (x
+c n) = (x +c p)) |
30 | 29 | abbi2i 2464 |
. . . . . 6
⊢ Fix (◡( AddC ∘ ◡(1st ↾ (V × {p}))) ∘ ( AddC ∘ ◡(1st ↾ (V × {n})))) = {x
∣ (x
+c n) = (x +c p)} |
31 | | addcfnex 5824 |
. . . . . . . . . 10
⊢ AddC ∈
V |
32 | | 1stex 4739 |
. . . . . . . . . . . 12
⊢ 1st
∈ V |
33 | | vvex 4109 |
. . . . . . . . . . . . 13
⊢ V ∈ V |
34 | | snex 4111 |
. . . . . . . . . . . . 13
⊢ {p} ∈
V |
35 | 33, 34 | xpex 5115 |
. . . . . . . . . . . 12
⊢ (V ×
{p}) ∈
V |
36 | 32, 35 | resex 5117 |
. . . . . . . . . . 11
⊢ (1st
↾ (V × {p})) ∈
V |
37 | 36 | cnvex 5102 |
. . . . . . . . . 10
⊢ ◡(1st ↾ (V × {p})) ∈
V |
38 | 31, 37 | coex 4750 |
. . . . . . . . 9
⊢ ( AddC ∘ ◡(1st ↾ (V × {p}))) ∈
V |
39 | 38 | cnvex 5102 |
. . . . . . . 8
⊢ ◡( AddC ∘ ◡(1st ↾ (V × {p}))) ∈
V |
40 | | snex 4111 |
. . . . . . . . . . . 12
⊢ {n} ∈
V |
41 | 33, 40 | xpex 5115 |
. . . . . . . . . . 11
⊢ (V ×
{n}) ∈
V |
42 | 32, 41 | resex 5117 |
. . . . . . . . . 10
⊢ (1st
↾ (V × {n})) ∈
V |
43 | 42 | cnvex 5102 |
. . . . . . . . 9
⊢ ◡(1st ↾ (V × {n})) ∈
V |
44 | 31, 43 | coex 4750 |
. . . . . . . 8
⊢ ( AddC ∘ ◡(1st ↾ (V × {n}))) ∈
V |
45 | 39, 44 | coex 4750 |
. . . . . . 7
⊢ (◡( AddC ∘ ◡(1st ↾ (V × {p}))) ∘ ( AddC ∘ ◡(1st ↾ (V × {n})))) ∈
V |
46 | 45 | fixex 5789 |
. . . . . 6
⊢ Fix (◡( AddC ∘ ◡(1st ↾ (V × {p}))) ∘ ( AddC ∘ ◡(1st ↾ (V × {n})))) ∈
V |
47 | 30, 46 | eqeltrri 2424 |
. . . . 5
⊢ {x ∣ (x +c n) = (x
+c p)} ∈ V |
48 | 10, 14, 47 | vtocl2g 2918 |
. . . 4
⊢ ((N ∈ V ∧ P ∈ W) → {x
∣ (x
+c N) = (x +c P)} ∈
V) |
49 | | complexg 4099 |
. . . 4
⊢ ({x ∣ (x +c N) = (x
+c P)} ∈ V → ∼ {x ∣ (x +c N) = (x
+c P)} ∈ V) |
50 | 48, 49 | syl 15 |
. . 3
⊢ ((N ∈ V ∧ P ∈ W) → ∼ {x ∣ (x +c N) = (x
+c P)} ∈ V) |
51 | | abexv 4324 |
. . 3
⊢ {x ∣ N = P} ∈ V |
52 | | unexg 4101 |
. . 3
⊢ (( ∼ {x ∣ (x +c N) = (x
+c P)} ∈ V ∧ {x ∣ N = P} ∈ V) → ( ∼ {x ∣ (x +c N) = (x
+c P)} ∪ {x ∣ N = P}) ∈ V) |
53 | 50, 51, 52 | sylancl 643 |
. 2
⊢ ((N ∈ V ∧ P ∈ W) → ( ∼ {x ∣ (x +c N) = (x
+c P)} ∪ {x ∣ N = P}) ∈ V) |
54 | 6, 53 | syl5eqelr 2438 |
1
⊢ ((N ∈ V ∧ P ∈ W) → {x
∣ ((x
+c N) = (x +c P) → N =
P)} ∈
V) |