Step | Hyp | Ref
| Expression |
1 | | elima 4754 |
. . . 4
⊢ (a ∈ (((ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∪ ran (◡ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
))) “ Nn ) ↔ ∃n ∈ Nn n((ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∪ ran (◡ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)))a) |
2 | | df-br 4640 |
. . . . . 6
⊢ (n((ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∪ ran (◡ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)))a ↔ 〈n, a〉 ∈ ((ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∪ ran (◡ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)))) |
3 | | elun 3220 |
. . . . . . . . 9
⊢ (〈n, a〉 ∈ (ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ↔ (〈n, a〉 ∈ ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∨
〈n,
a〉 ∈ ran (◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
)))) |
4 | | nncdiv3lem1 6275 |
. . . . . . . . . 10
⊢ (〈n, a〉 ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ a = ((n
+c n)
+c n)) |
5 | | elrn2 4897 |
. . . . . . . . . . 11
⊢ (〈n, a〉 ∈ ran (◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
)) ↔ ∃b〈b, 〈n, a〉〉 ∈ (◡ran (
Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) |
6 | | oteltxp 5782 |
. . . . . . . . . . . . 13
⊢ (〈b, 〈n, a〉〉 ∈ (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
)) ↔ (〈b, n〉 ∈ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∧
〈b,
a〉 ∈ ran ((1st ∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) |
7 | | opelcnv 4893 |
. . . . . . . . . . . . . . 15
⊢ (〈b, n〉 ∈ ◡ran (
Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ 〈n, b〉 ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) |
8 | | nncdiv3lem1 6275 |
. . . . . . . . . . . . . . 15
⊢ (〈n, b〉 ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ b = ((n
+c n)
+c n)) |
9 | 7, 8 | bitri 240 |
. . . . . . . . . . . . . 14
⊢ (〈b, n〉 ∈ ◡ran (
Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ b = ((n
+c n)
+c n)) |
10 | | elrn2 4897 |
. . . . . . . . . . . . . . . 16
⊢ (〈b, a〉 ∈ ran ((1st ∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
) ↔ ∃n〈n, 〈b, a〉〉 ∈ ((1st ∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
)) |
11 | | oteltxp 5782 |
. . . . . . . . . . . . . . . . . 18
⊢ (〈n, 〈b, a〉〉 ∈
((1st ∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
) ↔ (〈n, b〉 ∈
(1st ∩ ((◡2nd
“ {1c}) × V)) ∧
〈n,
a〉 ∈ AddC
)) |
12 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (〈n, b〉 ∈ (1st ∩ ((◡2nd “
{1c}) × V)) ↔ (〈n, b〉 ∈ 1st ∧
〈n,
b〉 ∈ ((◡2nd “
{1c}) × V))) |
13 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (n1st b ↔ 〈n, b〉 ∈
1st ) |
14 | 13 | bicomi 193 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (〈n, b〉 ∈ 1st ↔ n1st b) |
15 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ b ∈
V |
16 | | opelxp 4811 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (〈n, b〉 ∈ ((◡2nd “
{1c}) × V) ↔ (n ∈ (◡2nd “
{1c}) ∧ b ∈
V)) |
17 | 15, 16 | mpbiran2 885 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (〈n, b〉 ∈ ((◡2nd “
{1c}) × V) ↔ n
∈ (◡2nd “
{1c})) |
18 | | eliniseg 5020 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (n ∈ (◡2nd “
{1c}) ↔ n2nd
1c) |
19 | 17, 18 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (〈n, b〉 ∈ ((◡2nd “
{1c}) × V) ↔ n2nd
1c) |
20 | 14, 19 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((〈n, b〉 ∈ 1st ∧
〈n,
b〉 ∈ ((◡2nd “
{1c}) × V)) ↔ (n1st b ∧ n2nd
1c)) |
21 | | 1cex 4142 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
1c ∈
V |
22 | 15, 21 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((n1st b ∧ n2nd 1c) ↔
n = 〈b,
1c〉) |
23 | 12, 20, 22 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . 19
⊢ (〈n, b〉 ∈ (1st ∩ ((◡2nd “
{1c}) × V)) ↔ n = 〈b, 1c〉) |
24 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (n AddC a ↔ 〈n, a〉 ∈ AddC ) |
25 | 24 | bicomi 193 |
. . . . . . . . . . . . . . . . . . 19
⊢ (〈n, a〉 ∈ AddC ↔ n AddC a) |
26 | 23, 25 | anbi12i 678 |
. . . . . . . . . . . . . . . . . 18
⊢ ((〈n, b〉 ∈ (1st ∩ ((◡2nd “
{1c}) × V)) ∧ 〈n, a〉 ∈ AddC ) ↔
(n = 〈b,
1c〉 ∧ n AddC a)) |
27 | 11, 26 | bitri 240 |
. . . . . . . . . . . . . . . . 17
⊢ (〈n, 〈b, a〉〉 ∈
((1st ∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
) ↔ (n = 〈b,
1c〉 ∧ n AddC a)) |
28 | 27 | exbii 1582 |
. . . . . . . . . . . . . . . 16
⊢ (∃n〈n, 〈b, a〉〉 ∈
((1st ∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
) ↔ ∃n(n = 〈b,
1c〉 ∧ n AddC a)) |
29 | 10, 28 | bitri 240 |
. . . . . . . . . . . . . . 15
⊢ (〈b, a〉 ∈ ran ((1st ∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
) ↔ ∃n(n = 〈b,
1c〉 ∧ n AddC a)) |
30 | 15, 21 | opex 4588 |
. . . . . . . . . . . . . . . 16
⊢ 〈b,
1c〉 ∈ V |
31 | | breq1 4642 |
. . . . . . . . . . . . . . . 16
⊢ (n = 〈b, 1c〉 → (n
AddC a ↔
〈b,
1c〉 AddC a)) |
32 | 30, 31 | ceqsexv 2894 |
. . . . . . . . . . . . . . 15
⊢ (∃n(n = 〈b, 1c〉 ∧ n AddC a) ↔ 〈b,
1c〉 AddC a) |
33 | 15, 21 | braddcfn 5826 |
. . . . . . . . . . . . . . . 16
⊢ (〈b,
1c〉 AddC a ↔
(b +c
1c) = a) |
34 | | eqcom 2355 |
. . . . . . . . . . . . . . . 16
⊢ ((b +c 1c) =
a ↔ a = (b
+c 1c)) |
35 | 33, 34 | bitri 240 |
. . . . . . . . . . . . . . 15
⊢ (〈b,
1c〉 AddC a ↔
a = (b
+c 1c)) |
36 | 29, 32, 35 | 3bitri 262 |
. . . . . . . . . . . . . 14
⊢ (〈b, a〉 ∈ ran ((1st ∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
) ↔ a = (b +c
1c)) |
37 | 9, 36 | anbi12i 678 |
. . . . . . . . . . . . 13
⊢ ((〈b, n〉 ∈ ◡ran (
Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∧
〈b,
a〉 ∈ ran ((1st ∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
)) ↔ (b = ((n +c n) +c n) ∧ a = (b
+c 1c))) |
38 | 6, 37 | bitri 240 |
. . . . . . . . . . . 12
⊢ (〈b, 〈n, a〉〉 ∈ (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
)) ↔ (b = ((n +c n) +c n) ∧ a = (b
+c 1c))) |
39 | 38 | exbii 1582 |
. . . . . . . . . . 11
⊢ (∃b〈b, 〈n, a〉〉 ∈ (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
)) ↔ ∃b(b = ((n +c n) +c n) ∧ a = (b
+c 1c))) |
40 | | vex 2862 |
. . . . . . . . . . . . . 14
⊢ n ∈
V |
41 | 40, 40 | addcex 4394 |
. . . . . . . . . . . . 13
⊢ (n +c n) ∈
V |
42 | 41, 40 | addcex 4394 |
. . . . . . . . . . . 12
⊢ ((n +c n) +c n) ∈
V |
43 | | addceq1 4383 |
. . . . . . . . . . . . 13
⊢ (b = ((n
+c n)
+c n) → (b +c 1c) =
(((n +c n) +c n) +c
1c)) |
44 | 43 | eqeq2d 2364 |
. . . . . . . . . . . 12
⊢ (b = ((n
+c n)
+c n) → (a = (b
+c 1c) ↔ a = (((n
+c n)
+c n)
+c 1c))) |
45 | 42, 44 | ceqsexv 2894 |
. . . . . . . . . . 11
⊢ (∃b(b = ((n
+c n)
+c n) ∧ a = (b +c 1c)) ↔
a = (((n +c n) +c n) +c
1c)) |
46 | 5, 39, 45 | 3bitri 262 |
. . . . . . . . . 10
⊢ (〈n, a〉 ∈ ran (◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
)) ↔ a = (((n +c n) +c n) +c
1c)) |
47 | 4, 46 | orbi12i 507 |
. . . . . . . . 9
⊢ ((〈n, a〉 ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∨
〈n,
a〉 ∈ ran (◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ↔ (a = ((n +c n) +c n) ∨ a = (((n
+c n)
+c n)
+c 1c))) |
48 | 3, 47 | bitri 240 |
. . . . . . . 8
⊢ (〈n, a〉 ∈ (ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ↔ (a = ((n +c n) +c n) ∨ a = (((n
+c n)
+c n)
+c 1c))) |
49 | | elrn2 4897 |
. . . . . . . . 9
⊢ (〈n, a〉 ∈ ran (◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)) ↔ ∃b〈b, 〈n, a〉〉 ∈ (◡ran (
Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
))) |
50 | | oteltxp 5782 |
. . . . . . . . . . 11
⊢ (〈b, 〈n, a〉〉 ∈ (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)) ↔ (〈b, n〉 ∈ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∧
〈b,
a〉 ∈ ran ((1st ∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
))) |
51 | | elrn2 4897 |
. . . . . . . . . . . . . 14
⊢ (〈b, a〉 ∈ ran ((1st ∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
) ↔ ∃n〈n, 〈b, a〉〉 ∈ ((1st ∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)) |
52 | | oteltxp 5782 |
. . . . . . . . . . . . . . . 16
⊢ (〈n, 〈b, a〉〉 ∈
((1st ∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
) ↔ (〈n, b〉 ∈
(1st ∩ ((◡2nd
“ {2c}) × V)) ∧
〈n,
a〉 ∈ AddC
)) |
53 | | elin 3219 |
. . . . . . . . . . . . . . . . . 18
⊢ (〈n, b〉 ∈ (1st ∩ ((◡2nd “
{2c}) × V)) ↔ (〈n, b〉 ∈ 1st ∧
〈n,
b〉 ∈ ((◡2nd “
{2c}) × V))) |
54 | | opelxp 4811 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (〈n, b〉 ∈ ((◡2nd “
{2c}) × V) ↔ (n ∈ (◡2nd “
{2c}) ∧ b ∈
V)) |
55 | 15, 54 | mpbiran2 885 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (〈n, b〉 ∈ ((◡2nd “
{2c}) × V) ↔ n
∈ (◡2nd “
{2c})) |
56 | | eliniseg 5020 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (n ∈ (◡2nd “
{2c}) ↔ n2nd
2c) |
57 | 55, 56 | bitri 240 |
. . . . . . . . . . . . . . . . . . 19
⊢ (〈n, b〉 ∈ ((◡2nd “
{2c}) × V) ↔ n2nd
2c) |
58 | 14, 57 | anbi12i 678 |
. . . . . . . . . . . . . . . . . 18
⊢ ((〈n, b〉 ∈ 1st ∧
〈n,
b〉 ∈ ((◡2nd “
{2c}) × V)) ↔ (n1st b ∧ n2nd
2c)) |
59 | | df-2c 6104 |
. . . . . . . . . . . . . . . . . . . 20
⊢
2c = Nc {∅, V} |
60 | | ncex 6117 |
. . . . . . . . . . . . . . . . . . . 20
⊢ Nc {∅, V} ∈ V |
61 | 59, 60 | eqeltri 2423 |
. . . . . . . . . . . . . . . . . . 19
⊢
2c ∈
V |
62 | 15, 61 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . . 18
⊢ ((n1st b ∧ n2nd 2c) ↔
n = 〈b,
2c〉) |
63 | 53, 58, 62 | 3bitri 262 |
. . . . . . . . . . . . . . . . 17
⊢ (〈n, b〉 ∈ (1st ∩ ((◡2nd “
{2c}) × V)) ↔ n = 〈b, 2c〉) |
64 | 63, 25 | anbi12i 678 |
. . . . . . . . . . . . . . . 16
⊢ ((〈n, b〉 ∈ (1st ∩ ((◡2nd “
{2c}) × V)) ∧ 〈n, a〉 ∈ AddC ) ↔
(n = 〈b,
2c〉 ∧ n AddC a)) |
65 | 52, 64 | bitri 240 |
. . . . . . . . . . . . . . 15
⊢ (〈n, 〈b, a〉〉 ∈
((1st ∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
) ↔ (n = 〈b,
2c〉 ∧ n AddC a)) |
66 | 65 | exbii 1582 |
. . . . . . . . . . . . . 14
⊢ (∃n〈n, 〈b, a〉〉 ∈
((1st ∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
) ↔ ∃n(n = 〈b,
2c〉 ∧ n AddC a)) |
67 | 15, 61 | opex 4588 |
. . . . . . . . . . . . . . 15
⊢ 〈b,
2c〉 ∈ V |
68 | | breq1 4642 |
. . . . . . . . . . . . . . 15
⊢ (n = 〈b, 2c〉 → (n
AddC a ↔
〈b,
2c〉 AddC a)) |
69 | 67, 68 | ceqsexv 2894 |
. . . . . . . . . . . . . 14
⊢ (∃n(n = 〈b, 2c〉 ∧ n AddC a) ↔ 〈b,
2c〉 AddC a) |
70 | 51, 66, 69 | 3bitri 262 |
. . . . . . . . . . . . 13
⊢ (〈b, a〉 ∈ ran ((1st ∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
) ↔ 〈b, 2c〉 AddC a) |
71 | 15, 61 | braddcfn 5826 |
. . . . . . . . . . . . 13
⊢ (〈b,
2c〉 AddC a ↔
(b +c
2c) = a) |
72 | | eqcom 2355 |
. . . . . . . . . . . . 13
⊢ ((b +c 2c) =
a ↔ a = (b
+c 2c)) |
73 | 70, 71, 72 | 3bitri 262 |
. . . . . . . . . . . 12
⊢ (〈b, a〉 ∈ ran ((1st ∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
) ↔ a = (b +c
2c)) |
74 | 9, 73 | anbi12i 678 |
. . . . . . . . . . 11
⊢ ((〈b, n〉 ∈ ◡ran (
Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∧
〈b,
a〉 ∈ ran ((1st ∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)) ↔ (b = ((n +c n) +c n) ∧ a = (b
+c 2c))) |
75 | 50, 74 | bitri 240 |
. . . . . . . . . 10
⊢ (〈b, 〈n, a〉〉 ∈ (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)) ↔ (b = ((n +c n) +c n) ∧ a = (b
+c 2c))) |
76 | 75 | exbii 1582 |
. . . . . . . . 9
⊢ (∃b〈b, 〈n, a〉〉 ∈ (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)) ↔ ∃b(b = ((n +c n) +c n) ∧ a = (b
+c 2c))) |
77 | | addceq1 4383 |
. . . . . . . . . . 11
⊢ (b = ((n
+c n)
+c n) → (b +c 2c) =
(((n +c n) +c n) +c
2c)) |
78 | 77 | eqeq2d 2364 |
. . . . . . . . . 10
⊢ (b = ((n
+c n)
+c n) → (a = (b
+c 2c) ↔ a = (((n
+c n)
+c n)
+c 2c))) |
79 | 42, 78 | ceqsexv 2894 |
. . . . . . . . 9
⊢ (∃b(b = ((n
+c n)
+c n) ∧ a = (b +c 2c)) ↔
a = (((n +c n) +c n) +c
2c)) |
80 | 49, 76, 79 | 3bitri 262 |
. . . . . . . 8
⊢ (〈n, a〉 ∈ ran (◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)) ↔ a = (((n +c n) +c n) +c
2c)) |
81 | 48, 80 | orbi12i 507 |
. . . . . . 7
⊢ ((〈n, a〉 ∈ (ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∨ 〈n, a〉 ∈ ran (◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
))) ↔ ((a = ((n +c n) +c n) ∨ a = (((n
+c n)
+c n)
+c 1c)) ∨
a = (((n +c n) +c n) +c
2c))) |
82 | | elun 3220 |
. . . . . . 7
⊢ (〈n, a〉 ∈ ((ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∪ ran (◡ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
))) ↔ (〈n, a〉 ∈ (ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∨ 〈n, a〉 ∈ ran (◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)))) |
83 | | df-3or 935 |
. . . . . . 7
⊢ ((a = ((n
+c n)
+c n) ∨ a =
(((n +c n) +c n) +c 1c) ∨ a =
(((n +c n) +c n) +c 2c))
↔ ((a = ((n +c n) +c n) ∨ a = (((n
+c n)
+c n)
+c 1c)) ∨
a = (((n +c n) +c n) +c
2c))) |
84 | 81, 82, 83 | 3bitr4i 268 |
. . . . . 6
⊢ (〈n, a〉 ∈ ((ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∪ ran (◡ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
))) ↔ (a = ((n +c n) +c n) ∨ a = (((n
+c n)
+c n)
+c 1c) ∨
a = (((n +c n) +c n) +c
2c))) |
85 | 2, 84 | bitri 240 |
. . . . 5
⊢ (n((ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∪ ran (◡ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)))a ↔ (a = ((n
+c n)
+c n) ∨ a =
(((n +c n) +c n) +c 1c) ∨ a =
(((n +c n) +c n) +c
2c))) |
86 | 85 | rexbii 2639 |
. . . 4
⊢ (∃n ∈ Nn n((ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∪ ran (◡ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)))a ↔ ∃n ∈ Nn (a = ((n
+c n)
+c n) ∨ a =
(((n +c n) +c n) +c 1c) ∨ a =
(((n +c n) +c n) +c
2c))) |
87 | 1, 86 | bitri 240 |
. . 3
⊢ (a ∈ (((ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∪ ran (◡ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
))) “ Nn ) ↔ ∃n ∈ Nn (a = ((n
+c n)
+c n) ∨ a =
(((n +c n) +c n) +c 1c) ∨ a =
(((n +c n) +c n) +c
2c))) |
88 | 87 | abbi2i 2464 |
. 2
⊢ (((ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∪ ran (◡ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
))) “ Nn ) = {a ∣ ∃n ∈ Nn (a = ((n
+c n)
+c n) ∨ a =
(((n +c n) +c n) +c 1c) ∨ a =
(((n +c n) +c n) +c
2c))} |
89 | | 1stex 4739 |
. . . . . . . . . . . . . 14
⊢ 1st
∈ V |
90 | 89 | cnvex 5102 |
. . . . . . . . . . . . 13
⊢ ◡1st ∈ V |
91 | | 2ndex 5112 |
. . . . . . . . . . . . . 14
⊢ 2nd
∈ V |
92 | 89, 91 | inex 4105 |
. . . . . . . . . . . . 13
⊢ (1st
∩ 2nd ) ∈ V |
93 | 90, 92 | txpex 5785 |
. . . . . . . . . . . 12
⊢ (◡1st ⊗ (1st
∩ 2nd )) ∈ V |
94 | 93 | rnex 5107 |
. . . . . . . . . . 11
⊢ ran (◡1st ⊗ (1st
∩ 2nd )) ∈ V |
95 | 94, 91 | txpex 5785 |
. . . . . . . . . 10
⊢ (ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) ∈ V |
96 | | addcfnex 5824 |
. . . . . . . . . 10
⊢ AddC ∈
V |
97 | 95, 96 | imaex 4747 |
. . . . . . . . 9
⊢ ((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∈
V |
98 | 97 | cnvex 5102 |
. . . . . . . 8
⊢ ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∈
V |
99 | 98 | ins3ex 5798 |
. . . . . . 7
⊢ Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∈
V |
100 | 89, 89 | coex 4750 |
. . . . . . . . 9
⊢ (1st
∘ 1st ) ∈ V |
101 | 91, 89 | coex 4750 |
. . . . . . . . . 10
⊢ (2nd
∘ 1st ) ∈ V |
102 | 101, 91 | txpex 5785 |
. . . . . . . . 9
⊢ ((2nd
∘ 1st ) ⊗ 2nd )
∈ V |
103 | 100, 102 | txpex 5785 |
. . . . . . . 8
⊢ ((1st
∘ 1st ) ⊗ ((2nd
∘ 1st ) ⊗ 2nd
)) ∈ V |
104 | 103, 96 | imaex 4747 |
. . . . . . 7
⊢ (((1st
∘ 1st ) ⊗ ((2nd
∘ 1st ) ⊗ 2nd
)) “ AddC ) ∈ V |
105 | 99, 104 | inex 4105 |
. . . . . 6
⊢ ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∈ V |
106 | 105 | rnex 5107 |
. . . . 5
⊢ ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∈ V |
107 | 106 | cnvex 5102 |
. . . . . . 7
⊢ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∈ V |
108 | 91 | cnvex 5102 |
. . . . . . . . . . . 12
⊢ ◡2nd ∈ V |
109 | | snex 4111 |
. . . . . . . . . . . 12
⊢
{1c} ∈
V |
110 | 108, 109 | imaex 4747 |
. . . . . . . . . . 11
⊢ (◡2nd “
{1c}) ∈ V |
111 | | vvex 4109 |
. . . . . . . . . . 11
⊢ V ∈ V |
112 | 110, 111 | xpex 5115 |
. . . . . . . . . 10
⊢ ((◡2nd “
{1c}) × V) ∈
V |
113 | 89, 112 | inex 4105 |
. . . . . . . . 9
⊢ (1st
∩ ((◡2nd “
{1c}) × V)) ∈
V |
114 | 113, 96 | txpex 5785 |
. . . . . . . 8
⊢ ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
) ∈ V |
115 | 114 | rnex 5107 |
. . . . . . 7
⊢ ran
((1st ∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
) ∈ V |
116 | 107, 115 | txpex 5785 |
. . . . . 6
⊢ (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
)) ∈ V |
117 | 116 | rnex 5107 |
. . . . 5
⊢ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
)) ∈ V |
118 | 106, 117 | unex 4106 |
. . . 4
⊢ (ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∈ V |
119 | | snex 4111 |
. . . . . . . . . . 11
⊢
{2c} ∈
V |
120 | 108, 119 | imaex 4747 |
. . . . . . . . . 10
⊢ (◡2nd “
{2c}) ∈ V |
121 | 120, 111 | xpex 5115 |
. . . . . . . . 9
⊢ ((◡2nd “
{2c}) × V) ∈
V |
122 | 89, 121 | inex 4105 |
. . . . . . . 8
⊢ (1st
∩ ((◡2nd “
{2c}) × V)) ∈
V |
123 | 122, 96 | txpex 5785 |
. . . . . . 7
⊢ ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
) ∈ V |
124 | 123 | rnex 5107 |
. . . . . 6
⊢ ran
((1st ∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
) ∈ V |
125 | 107, 124 | txpex 5785 |
. . . . 5
⊢ (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)) ∈ V |
126 | 125 | rnex 5107 |
. . . 4
⊢ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
)) ∈ V |
127 | 118, 126 | unex 4106 |
. . 3
⊢ ((ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∪ ran (◡ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
))) ∈ V |
128 | | nncex 4396 |
. . 3
⊢ Nn ∈
V |
129 | 127, 128 | imaex 4747 |
. 2
⊢ (((ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∪ ran (◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{1c}) × V)) ⊗ AddC
))) ∪ ran (◡ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ⊗ ran ((1st
∩ ((◡2nd “
{2c}) × V)) ⊗ AddC
))) “ Nn ) ∈ V |
130 | 88, 129 | eqeltrri 2424 |
1
⊢ {a ∣ ∃n ∈ Nn (a = ((n
+c n)
+c n) ∨ a =
(((n +c n) +c n) +c 1c) ∨ a =
(((n +c n) +c n) +c 2c))}
∈ V |