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