Step | Hyp | Ref
| Expression |
1 | | addceq2 4385 |
. . . . . . 7
⊢ (n = N →
(m +c n) = (m
+c N)) |
2 | 1 | neeq1d 2530 |
. . . . . 6
⊢ (n = N →
((m +c n) ≠ ∅ ↔
(m +c N) ≠ ∅)) |
3 | 1 | eqeq1d 2361 |
. . . . . 6
⊢ (n = N →
((m +c n) = (m
+c p) ↔ (m +c N) = (m
+c p))) |
4 | 2, 3 | anbi12d 691 |
. . . . 5
⊢ (n = N →
(((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p)) ↔ ((m
+c N) ≠ ∅ ∧ (m +c N) = (m
+c p)))) |
5 | 4 | imbi1d 308 |
. . . 4
⊢ (n = N →
((((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p)) → N =
P) ↔ (((m +c N) ≠ ∅ ∧ (m
+c N) = (m +c p)) → N =
P))) |
6 | 5 | abbidv 2468 |
. . 3
⊢ (n = N →
{m ∣
(((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p)) → N =
P)} = {m ∣ (((m +c N) ≠ ∅ ∧ (m
+c N) = (m +c p)) → N =
P)}) |
7 | 6 | eleq1d 2419 |
. 2
⊢ (n = N →
({m ∣
(((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p)) → N =
P)} ∈ V
↔ {m ∣ (((m
+c N) ≠ ∅ ∧ (m +c N) = (m
+c p)) → N = P)} ∈ V)) |
8 | | addceq2 4385 |
. . . . . . 7
⊢ (p = P →
(m +c p) = (m
+c P)) |
9 | 8 | eqeq2d 2364 |
. . . . . 6
⊢ (p = P →
((m +c N) = (m
+c p) ↔ (m +c N) = (m
+c P))) |
10 | 9 | anbi2d 684 |
. . . . 5
⊢ (p = P →
(((m +c N) ≠ ∅ ∧ (m
+c N) = (m +c p)) ↔ ((m
+c N) ≠ ∅ ∧ (m +c N) = (m
+c P)))) |
11 | 10 | imbi1d 308 |
. . . 4
⊢ (p = P →
((((m +c N) ≠ ∅ ∧ (m
+c N) = (m +c p)) → N =
P) ↔ (((m +c N) ≠ ∅ ∧ (m
+c N) = (m +c P)) → N =
P))) |
12 | 11 | abbidv 2468 |
. . 3
⊢ (p = P →
{m ∣
(((m +c N) ≠ ∅ ∧ (m
+c N) = (m +c p)) → N =
P)} = {m ∣ (((m +c N) ≠ ∅ ∧ (m
+c N) = (m +c P)) → N =
P)}) |
13 | 12 | eleq1d 2419 |
. 2
⊢ (p = P →
({m ∣
(((m +c N) ≠ ∅ ∧ (m
+c N) = (m +c p)) → N =
P)} ∈ V
↔ {m ∣ (((m
+c N) ≠ ∅ ∧ (m +c N) = (m
+c P)) → N = P)} ∈ V)) |
14 | | imor 401 |
. . . . 5
⊢ ((((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p)) → N =
P) ↔ (¬ ((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p)) ∨ N = P)) |
15 | 14 | abbii 2466 |
. . . 4
⊢ {m ∣ (((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p)) → N =
P)} = {m ∣ (¬
((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p)) ∨ N = P)} |
16 | | unab 3522 |
. . . 4
⊢ ({m ∣ ¬
((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p))} ∪ {m
∣ N =
P}) = {m ∣ (¬
((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p)) ∨ N = P)} |
17 | 15, 16 | eqtr4i 2376 |
. . 3
⊢ {m ∣ (((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p)) → N =
P)} = ({m ∣ ¬
((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p))} ∪ {m
∣ N =
P}) |
18 | | vex 2863 |
. . . . . . . 8
⊢ m ∈
V |
19 | 18 | elcompl 3226 |
. . . . . . 7
⊢ (m ∈ ∼ ( ∼
(◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ∩ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V)) ↔ ¬
m ∈ ( ∼
(◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
“k {∅}) ∩ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V))) |
20 | | elin 3220 |
. . . . . . . . 9
⊢ (m ∈ ( ∼ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ∩ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V)) ↔ (m ∈ ∼ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
“k {∅}) ∧ m ∈ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V))) |
21 | | 0ex 4111 |
. . . . . . . . . . . . . 14
⊢ ∅ ∈
V |
22 | 21, 18 | opkelcnvk 4251 |
. . . . . . . . . . . . 13
⊢ (⟪∅, m⟫
∈ ◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) ↔ ⟪m, ∅⟫ ∈ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)) |
23 | 21, 18 | elimaksn 4284 |
. . . . . . . . . . . . 13
⊢ (m ∈ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ↔ ⟪∅, m⟫
∈ ◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)) |
24 | | dfaddc2 4382 |
. . . . . . . . . . . . . . 15
⊢ (m +c n) = ((( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k m) |
25 | 24 | eqeq2i 2363 |
. . . . . . . . . . . . . 14
⊢ (∅ = (m
+c n) ↔ ∅ = ((( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k m)) |
26 | | eqcom 2355 |
. . . . . . . . . . . . . 14
⊢ ((m +c n) = ∅ ↔
∅ = (m
+c n)) |
27 | 18, 21 | opkelimagek 4273 |
. . . . . . . . . . . . . 14
⊢ (⟪m, ∅⟫
∈ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) ↔ ∅ = (((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k m)) |
28 | 25, 26, 27 | 3bitr4i 268 |
. . . . . . . . . . . . 13
⊢ ((m +c n) = ∅ ↔
⟪m, ∅⟫ ∈
Imagek(( Ins3k
∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)) |
29 | 22, 23, 28 | 3bitr4i 268 |
. . . . . . . . . . . 12
⊢ (m ∈ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ↔ (m
+c n) = ∅) |
30 | 29 | notbii 287 |
. . . . . . . . . . 11
⊢ (¬ m ∈ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ↔ ¬ (m +c n) = ∅) |
31 | 18 | elcompl 3226 |
. . . . . . . . . . 11
⊢ (m ∈ ∼ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ↔ ¬ m ∈ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅})) |
32 | | df-ne 2519 |
. . . . . . . . . . 11
⊢ ((m +c n) ≠ ∅ ↔
¬ (m +c n) = ∅) |
33 | 30, 31, 32 | 3bitr4i 268 |
. . . . . . . . . 10
⊢ (m ∈ ∼ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ↔ (m
+c n) ≠ ∅) |
34 | | rexv 2874 |
. . . . . . . . . . . 12
⊢ (∃t ∈ V ⟪t,
m⟫ ∈ ◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) ↔ ∃t⟪t,
m⟫ ∈
◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p))) |
35 | | vex 2863 |
. . . . . . . . . . . . . . 15
⊢ t ∈
V |
36 | 35, 18 | opkelcnvk 4251 |
. . . . . . . . . . . . . 14
⊢ (⟪t, m⟫
∈ ◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) ↔ ⟪m, t⟫ ∈ (Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p))) |
37 | | elin 3220 |
. . . . . . . . . . . . . . 15
⊢ (⟪m, t⟫
∈ (Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) ∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) ↔ (⟪m, t⟫
∈ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) ∧
⟪m, t⟫ ∈
Imagek(( Ins3k
∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p))) |
38 | 18, 35 | opkelimagek 4273 |
. . . . . . . . . . . . . . . . 17
⊢ (⟪m, t⟫
∈ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) ↔ t =
((( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k m)) |
39 | 24 | eqeq2i 2363 |
. . . . . . . . . . . . . . . . 17
⊢ (t = (m
+c n) ↔ t = ((( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k m)) |
40 | 38, 39 | bitr4i 243 |
. . . . . . . . . . . . . . . 16
⊢ (⟪m, t⟫
∈ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) ↔ t =
(m +c n)) |
41 | 18, 35 | opkelimagek 4273 |
. . . . . . . . . . . . . . . . 17
⊢ (⟪m, t⟫
∈ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p) ↔ t =
((( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p) “k m)) |
42 | | dfaddc2 4382 |
. . . . . . . . . . . . . . . . . 18
⊢ (m +c p) = ((( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p) “k m) |
43 | 42 | eqeq2i 2363 |
. . . . . . . . . . . . . . . . 17
⊢ (t = (m
+c p) ↔ t = ((( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p) “k m)) |
44 | 41, 43 | bitr4i 243 |
. . . . . . . . . . . . . . . 16
⊢ (⟪m, t⟫
∈ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p) ↔ t =
(m +c p)) |
45 | 40, 44 | anbi12i 678 |
. . . . . . . . . . . . . . 15
⊢ ((⟪m, t⟫
∈ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) ∧
⟪m, t⟫ ∈
Imagek(( Ins3k
∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) ↔ (t =
(m +c n) ∧ t = (m
+c p))) |
46 | 37, 45 | bitri 240 |
. . . . . . . . . . . . . 14
⊢ (⟪m, t⟫
∈ (Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) ∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) ↔ (t =
(m +c n) ∧ t = (m
+c p))) |
47 | 36, 46 | bitri 240 |
. . . . . . . . . . . . 13
⊢ (⟪t, m⟫
∈ ◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) ↔ (t =
(m +c n) ∧ t = (m
+c p))) |
48 | 47 | exbii 1582 |
. . . . . . . . . . . 12
⊢ (∃t⟪t,
m⟫ ∈ ◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) ↔ ∃t(t = (m
+c n) ∧ t = (m +c p))) |
49 | 34, 48 | bitri 240 |
. . . . . . . . . . 11
⊢ (∃t ∈ V ⟪t,
m⟫ ∈ ◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) ↔ ∃t(t = (m
+c n) ∧ t = (m +c p))) |
50 | 18 | elimak 4260 |
. . . . . . . . . . 11
⊢ (m ∈ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V) ↔ ∃t ∈ V ⟪t,
m⟫ ∈
◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p))) |
51 | | vex 2863 |
. . . . . . . . . . . . 13
⊢ n ∈
V |
52 | 18, 51 | addcex 4395 |
. . . . . . . . . . . 12
⊢ (m +c n) ∈
V |
53 | 52 | eqvinc 2967 |
. . . . . . . . . . 11
⊢ ((m +c n) = (m
+c p) ↔ ∃t(t = (m
+c n) ∧ t = (m +c p))) |
54 | 49, 50, 53 | 3bitr4i 268 |
. . . . . . . . . 10
⊢ (m ∈ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V) ↔ (m +c n) = (m
+c p)) |
55 | 33, 54 | anbi12i 678 |
. . . . . . . . 9
⊢ ((m ∈ ∼ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ∧ m ∈ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V)) ↔ ((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p))) |
56 | 20, 55 | bitri 240 |
. . . . . . . 8
⊢ (m ∈ ( ∼ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ∩ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V)) ↔ ((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p))) |
57 | 56 | notbii 287 |
. . . . . . 7
⊢ (¬ m ∈ ( ∼ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ∩ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V)) ↔ ¬
((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p))) |
58 | 19, 57 | bitri 240 |
. . . . . 6
⊢ (m ∈ ∼ ( ∼
(◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ∩ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V)) ↔ ¬
((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p))) |
59 | 58 | abbi2i 2465 |
. . . . 5
⊢ ∼ ( ∼
(◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ∩ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V)) = {m ∣ ¬
((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p))} |
60 | | addcexlem 4383 |
. . . . . . . . . . . 12
⊢ ( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) ∈ V |
61 | 51 | pw1ex 4304 |
. . . . . . . . . . . . 13
⊢ ℘1n ∈
V |
62 | 61 | pw1ex 4304 |
. . . . . . . . . . . 12
⊢ ℘1℘1n ∈
V |
63 | 60, 62 | imakex 4301 |
. . . . . . . . . . 11
⊢ (( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) ∈
V |
64 | 63 | imagekex 4313 |
. . . . . . . . . 10
⊢
Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) ∈
V |
65 | 64 | cnvkex 4288 |
. . . . . . . . 9
⊢ ◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) ∈
V |
66 | | snex 4112 |
. . . . . . . . 9
⊢ {∅} ∈
V |
67 | 65, 66 | imakex 4301 |
. . . . . . . 8
⊢ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ∈
V |
68 | 67 | complex 4105 |
. . . . . . 7
⊢ ∼ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ∈
V |
69 | | vex 2863 |
. . . . . . . . . . . . . 14
⊢ p ∈
V |
70 | 69 | pw1ex 4304 |
. . . . . . . . . . . . 13
⊢ ℘1p ∈
V |
71 | 70 | pw1ex 4304 |
. . . . . . . . . . . 12
⊢ ℘1℘1p ∈
V |
72 | 60, 71 | imakex 4301 |
. . . . . . . . . . 11
⊢ (( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p) ∈
V |
73 | 72 | imagekex 4313 |
. . . . . . . . . 10
⊢
Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p) ∈
V |
74 | 64, 73 | inex 4106 |
. . . . . . . . 9
⊢
(Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) ∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) ∈
V |
75 | 74 | cnvkex 4288 |
. . . . . . . 8
⊢ ◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) ∈
V |
76 | | vvex 4110 |
. . . . . . . 8
⊢ V ∈ V |
77 | 75, 76 | imakex 4301 |
. . . . . . 7
⊢ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V) ∈ V |
78 | 68, 77 | inex 4106 |
. . . . . 6
⊢ ( ∼ (◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ∩ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V)) ∈ V |
79 | 78 | complex 4105 |
. . . . 5
⊢ ∼ ( ∼
(◡kImagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n) “k {∅}) ∩ (◡k(Imagek((
Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1n)
∩ Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘1p)) “k V)) ∈ V |
80 | 59, 79 | eqeltrri 2424 |
. . . 4
⊢ {m ∣ ¬
((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p))} ∈
V |
81 | | abexv 4325 |
. . . 4
⊢ {m ∣ N = P} ∈ V |
82 | 80, 81 | unex 4107 |
. . 3
⊢ ({m ∣ ¬
((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p))} ∪ {m
∣ N =
P}) ∈
V |
83 | 17, 82 | eqeltri 2423 |
. 2
⊢ {m ∣ (((m +c n) ≠ ∅ ∧ (m
+c n) = (m +c p)) → N =
P)} ∈
V |
84 | 7, 13, 83 | vtocl2g 2919 |
1
⊢ ((N ∈ Nn ∧ P ∈ Nn ) → {m ∣ (((m
+c N) ≠ ∅ ∧ (m +c N) = (m
+c P)) → N = P)} ∈ V) |