Step | Hyp | Ref
| Expression |
1 | | elrn2 4898 |
. 2
⊢ (⟨n, b⟩ ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ ∃m⟨m, ⟨n, b⟩⟩ ∈ ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) |
2 | | elin 3220 |
. . . 4
⊢ (⟨m, ⟨n, b⟩⟩ ∈ ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ (⟨m, ⟨n, b⟩⟩ ∈ Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∧ ⟨m, ⟨n, b⟩⟩ ∈
(((1st ∘ 1st )
⊗ ((2nd ∘ 1st )
⊗ 2nd )) “ AddC
))) |
3 | | vex 2863 |
. . . . . . 7
⊢ b ∈
V |
4 | 3 | otelins3 5793 |
. . . . . 6
⊢ (⟨m, ⟨n, b⟩⟩ ∈ Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ↔ ⟨m, n⟩ ∈ ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC )) |
5 | | opelcnv 4894 |
. . . . . 6
⊢ (⟨m, n⟩ ∈ ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ↔ ⟨n, m⟩ ∈ ((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC )) |
6 | | trtxp 5782 |
. . . . . . . . . 10
⊢ (t(ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd )⟨n, m⟩ ↔
(tran (◡1st ⊗ (1st
∩ 2nd ))n ∧ t2nd m)) |
7 | | df-br 4641 |
. . . . . . . . . . . 12
⊢ (tran (◡1st ⊗ (1st
∩ 2nd ))n ↔ ⟨t, n⟩ ∈ ran (◡1st ⊗ (1st
∩ 2nd ))) |
8 | | elrn2 4898 |
. . . . . . . . . . . 12
⊢ (⟨t, n⟩ ∈ ran (◡1st ⊗ (1st
∩ 2nd )) ↔ ∃m⟨m, ⟨t, n⟩⟩ ∈ (◡1st ⊗ (1st
∩ 2nd ))) |
9 | | vex 2863 |
. . . . . . . . . . . . . . 15
⊢ t ∈
V |
10 | 9 | proj1ex 4594 |
. . . . . . . . . . . . . 14
⊢ Proj1 t ∈ V |
11 | 10 | eqvinc 2967 |
. . . . . . . . . . . . 13
⊢ ( Proj1 t = ⟨n, n⟩ ↔ ∃m(m = Proj1 t ∧ m = ⟨n, n⟩)) |
12 | | opeq 4620 |
. . . . . . . . . . . . . . 15
⊢ t = ⟨ Proj1 t, Proj2 t⟩ |
13 | 12 | breq1i 4647 |
. . . . . . . . . . . . . 14
⊢ (t1st ⟨n, n⟩ ↔ ⟨ Proj1 t, Proj2 t⟩1st
⟨n,
n⟩) |
14 | 9 | proj2ex 4595 |
. . . . . . . . . . . . . . 15
⊢ Proj2 t ∈ V |
15 | 10, 14 | opbr1st 5502 |
. . . . . . . . . . . . . 14
⊢ (⟨ Proj1 t, Proj2 t⟩1st
⟨n,
n⟩ ↔
Proj1 t =
⟨n,
n⟩) |
16 | 13, 15 | bitri 240 |
. . . . . . . . . . . . 13
⊢ (t1st ⟨n, n⟩ ↔ Proj1 t = ⟨n, n⟩) |
17 | | oteltxp 5783 |
. . . . . . . . . . . . . . 15
⊢ (⟨m, ⟨t, n⟩⟩ ∈ (◡1st ⊗ (1st
∩ 2nd )) ↔ (⟨m, t⟩ ∈ ◡1st ∧ ⟨m, n⟩ ∈
(1st ∩ 2nd ))) |
18 | | opelcnv 4894 |
. . . . . . . . . . . . . . . . 17
⊢ (⟨m, t⟩ ∈ ◡1st ↔ ⟨t, m⟩ ∈ 1st ) |
19 | | df-br 4641 |
. . . . . . . . . . . . . . . . 17
⊢ (t1st m ↔ ⟨t, m⟩ ∈
1st ) |
20 | 12 | breq1i 4647 |
. . . . . . . . . . . . . . . . . 18
⊢ (t1st m ↔ ⟨ Proj1 t, Proj2 t⟩1st m) |
21 | 10, 14 | opbr1st 5502 |
. . . . . . . . . . . . . . . . . 18
⊢ (⟨ Proj1 t, Proj2 t⟩1st
m ↔ Proj1
t = m) |
22 | | eqcom 2355 |
. . . . . . . . . . . . . . . . . 18
⊢ ( Proj1 t = m ↔ m =
Proj1 t) |
23 | 20, 21, 22 | 3bitri 262 |
. . . . . . . . . . . . . . . . 17
⊢ (t1st m ↔ m =
Proj1 t) |
24 | 18, 19, 23 | 3bitr2i 264 |
. . . . . . . . . . . . . . . 16
⊢ (⟨m, t⟩ ∈ ◡1st ↔ m = Proj1 t) |
25 | | elin 3220 |
. . . . . . . . . . . . . . . . 17
⊢ (⟨m, n⟩ ∈ (1st ∩ 2nd ) ↔
(⟨m,
n⟩ ∈ 1st ∧
⟨m,
n⟩ ∈ 2nd )) |
26 | | df-br 4641 |
. . . . . . . . . . . . . . . . . 18
⊢ (m1st n ↔ ⟨m, n⟩ ∈
1st ) |
27 | | df-br 4641 |
. . . . . . . . . . . . . . . . . 18
⊢ (m2nd n ↔ ⟨m, n⟩ ∈
2nd ) |
28 | 26, 27 | anbi12i 678 |
. . . . . . . . . . . . . . . . 17
⊢ ((m1st n ∧ m2nd n) ↔ (⟨m, n⟩ ∈ 1st ∧
⟨m,
n⟩ ∈ 2nd )) |
29 | | vex 2863 |
. . . . . . . . . . . . . . . . . 18
⊢ n ∈
V |
30 | 29, 29 | op1st2nd 5791 |
. . . . . . . . . . . . . . . . 17
⊢ ((m1st n ∧ m2nd n) ↔ m =
⟨n,
n⟩) |
31 | 25, 28, 30 | 3bitr2i 264 |
. . . . . . . . . . . . . . . 16
⊢ (⟨m, n⟩ ∈ (1st ∩ 2nd ) ↔
m = ⟨n, n⟩) |
32 | 24, 31 | anbi12i 678 |
. . . . . . . . . . . . . . 15
⊢ ((⟨m, t⟩ ∈ ◡1st ∧ ⟨m, n⟩ ∈
(1st ∩ 2nd )) ↔ (m = Proj1 t ∧ m = ⟨n, n⟩)) |
33 | 17, 32 | bitri 240 |
. . . . . . . . . . . . . 14
⊢ (⟨m, ⟨t, n⟩⟩ ∈ (◡1st ⊗ (1st
∩ 2nd )) ↔ (m = Proj1 t ∧ m = ⟨n, n⟩)) |
34 | 33 | exbii 1582 |
. . . . . . . . . . . . 13
⊢ (∃m⟨m, ⟨t, n⟩⟩ ∈ (◡1st ⊗ (1st
∩ 2nd )) ↔ ∃m(m = Proj1 t ∧ m = ⟨n, n⟩)) |
35 | 11, 16, 34 | 3bitr4ri 269 |
. . . . . . . . . . . 12
⊢ (∃m⟨m, ⟨t, n⟩⟩ ∈ (◡1st ⊗ (1st
∩ 2nd )) ↔ t1st ⟨n, n⟩) |
36 | 7, 8, 35 | 3bitri 262 |
. . . . . . . . . . 11
⊢ (tran (◡1st ⊗ (1st
∩ 2nd ))n ↔ t1st ⟨n, n⟩) |
37 | 36 | anbi1i 676 |
. . . . . . . . . 10
⊢ ((tran (◡1st ⊗ (1st
∩ 2nd ))n ∧ t2nd m) ↔ (t1st ⟨n, n⟩ ∧ t2nd m)) |
38 | 29, 29 | opex 4589 |
. . . . . . . . . . 11
⊢ ⟨n, n⟩ ∈ V |
39 | | vex 2863 |
. . . . . . . . . . 11
⊢ m ∈
V |
40 | 38, 39 | op1st2nd 5791 |
. . . . . . . . . 10
⊢ ((t1st ⟨n, n⟩ ∧ t2nd m) ↔ t =
⟨⟨n, n⟩, m⟩) |
41 | 6, 37, 40 | 3bitri 262 |
. . . . . . . . 9
⊢ (t(ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd )⟨n, m⟩ ↔ t = ⟨⟨n, n⟩, m⟩) |
42 | 41 | rexbii 2640 |
. . . . . . . 8
⊢ (∃t ∈ AddC t(ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd )⟨n, m⟩ ↔ ∃t ∈ AddC t = ⟨⟨n, n⟩, m⟩) |
43 | | elima 4755 |
. . . . . . . 8
⊢ (⟨n, m⟩ ∈ ((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ↔ ∃t ∈ AddC t(ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd )⟨n, m⟩) |
44 | | df-br 4641 |
. . . . . . . . 9
⊢ (⟨n, n⟩ AddC m ↔ ⟨⟨n, n⟩, m⟩ ∈ AddC ) |
45 | | risset 2662 |
. . . . . . . . 9
⊢ (⟨⟨n, n⟩, m⟩ ∈ AddC ↔ ∃t ∈ AddC t = ⟨⟨n, n⟩, m⟩) |
46 | 44, 45 | bitri 240 |
. . . . . . . 8
⊢ (⟨n, n⟩ AddC m ↔ ∃t ∈ AddC t = ⟨⟨n, n⟩, m⟩) |
47 | 42, 43, 46 | 3bitr4i 268 |
. . . . . . 7
⊢ (⟨n, m⟩ ∈ ((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ↔ ⟨n, n⟩ AddC m) |
48 | 29, 29 | braddcfn 5827 |
. . . . . . 7
⊢ (⟨n, n⟩ AddC m ↔
(n +c n) = m) |
49 | | eqcom 2355 |
. . . . . . 7
⊢ ((n +c n) = m ↔
m = (n
+c n)) |
50 | 47, 48, 49 | 3bitri 262 |
. . . . . 6
⊢ (⟨n, m⟩ ∈ ((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ↔ m =
(n +c n)) |
51 | 4, 5, 50 | 3bitri 262 |
. . . . 5
⊢ (⟨m, ⟨n, b⟩⟩ ∈ Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ↔ m =
(n +c n)) |
52 | | elima 4755 |
. . . . . . 7
⊢ (⟨m, ⟨n, b⟩⟩ ∈
(((1st ∘ 1st )
⊗ ((2nd ∘ 1st )
⊗ 2nd )) “ AddC ) ↔
∃t ∈ AddC t((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))⟨m, ⟨n, b⟩⟩) |
53 | | trtxp 5782 |
. . . . . . . . 9
⊢ (t((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))⟨m, ⟨n, b⟩⟩ ↔ (t(1st ∘ 1st )m ∧ t((2nd ∘ 1st ) ⊗ 2nd )⟨n, b⟩)) |
54 | | trtxp 5782 |
. . . . . . . . . . 11
⊢ (t((2nd ∘ 1st ) ⊗ 2nd )⟨n, b⟩ ↔
(t(2nd ∘ 1st )n ∧ t2nd b)) |
55 | 54 | anbi2i 675 |
. . . . . . . . . 10
⊢ ((t(1st ∘ 1st )m ∧ t((2nd ∘ 1st ) ⊗ 2nd )⟨n, b⟩) ↔
(t(1st ∘ 1st )m ∧ (t(2nd ∘ 1st )n ∧ t2nd b))) |
56 | | anass 630 |
. . . . . . . . . 10
⊢ (((t(1st ∘ 1st )m ∧ t(2nd ∘ 1st )n) ∧ t2nd b) ↔ (t(1st ∘ 1st )m ∧ (t(2nd ∘ 1st )n ∧ t2nd b))) |
57 | 39, 29 | op1st2nd 5791 |
. . . . . . . . . . . 12
⊢ (( Proj1 t1st m ∧ Proj1 t2nd n) ↔ Proj1
t = ⟨m, n⟩) |
58 | | brco 4884 |
. . . . . . . . . . . . . 14
⊢ (t(1st ∘ 1st )m ↔ ∃n(t1st n ∧ n1st m)) |
59 | 12 | breq1i 4647 |
. . . . . . . . . . . . . . . . 17
⊢ (t1st n ↔ ⟨ Proj1 t, Proj2 t⟩1st n) |
60 | 10, 14 | opbr1st 5502 |
. . . . . . . . . . . . . . . . 17
⊢ (⟨ Proj1 t, Proj2 t⟩1st
n ↔ Proj1
t = n) |
61 | | eqcom 2355 |
. . . . . . . . . . . . . . . . 17
⊢ ( Proj1 t = n ↔ n =
Proj1 t) |
62 | 59, 60, 61 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
⊢ (t1st n ↔ n =
Proj1 t) |
63 | 62 | anbi1i 676 |
. . . . . . . . . . . . . . 15
⊢ ((t1st n ∧ n1st m) ↔ (n =
Proj1 t ∧ n1st m)) |
64 | 63 | exbii 1582 |
. . . . . . . . . . . . . 14
⊢ (∃n(t1st n ∧ n1st m) ↔ ∃n(n = Proj1 t ∧ n1st m)) |
65 | | breq1 4643 |
. . . . . . . . . . . . . . 15
⊢ (n = Proj1 t → (n1st m ↔ Proj1
t1st m)) |
66 | 10, 65 | ceqsexv 2895 |
. . . . . . . . . . . . . 14
⊢ (∃n(n = Proj1 t ∧ n1st m) ↔ Proj1
t1st m) |
67 | 58, 64, 66 | 3bitri 262 |
. . . . . . . . . . . . 13
⊢ (t(1st ∘ 1st )m ↔ Proj1
t1st m) |
68 | | brco 4884 |
. . . . . . . . . . . . . 14
⊢ (t(2nd ∘ 1st )n ↔ ∃m(t1st m ∧ m2nd n)) |
69 | 23 | anbi1i 676 |
. . . . . . . . . . . . . . 15
⊢ ((t1st m ∧ m2nd n) ↔ (m =
Proj1 t ∧ m2nd n)) |
70 | 69 | exbii 1582 |
. . . . . . . . . . . . . 14
⊢ (∃m(t1st m ∧ m2nd n) ↔ ∃m(m = Proj1 t ∧ m2nd n)) |
71 | | breq1 4643 |
. . . . . . . . . . . . . . 15
⊢ (m = Proj1 t → (m2nd n ↔ Proj1
t2nd n)) |
72 | 10, 71 | ceqsexv 2895 |
. . . . . . . . . . . . . 14
⊢ (∃m(m = Proj1 t ∧ m2nd n) ↔ Proj1
t2nd n) |
73 | 68, 70, 72 | 3bitri 262 |
. . . . . . . . . . . . 13
⊢ (t(2nd ∘ 1st )n ↔ Proj1
t2nd n) |
74 | 67, 73 | anbi12i 678 |
. . . . . . . . . . . 12
⊢ ((t(1st ∘ 1st )m ∧ t(2nd ∘ 1st )n) ↔ ( Proj1
t1st m ∧ Proj1 t2nd n)) |
75 | 12 | breq1i 4647 |
. . . . . . . . . . . . 13
⊢ (t1st ⟨m, n⟩ ↔ ⟨ Proj1 t, Proj2 t⟩1st
⟨m,
n⟩) |
76 | 10, 14 | opbr1st 5502 |
. . . . . . . . . . . . 13
⊢ (⟨ Proj1 t, Proj2 t⟩1st
⟨m,
n⟩ ↔
Proj1 t =
⟨m,
n⟩) |
77 | 75, 76 | bitri 240 |
. . . . . . . . . . . 12
⊢ (t1st ⟨m, n⟩ ↔ Proj1 t = ⟨m, n⟩) |
78 | 57, 74, 77 | 3bitr4i 268 |
. . . . . . . . . . 11
⊢ ((t(1st ∘ 1st )m ∧ t(2nd ∘ 1st )n) ↔ t1st ⟨m, n⟩) |
79 | 78 | anbi1i 676 |
. . . . . . . . . 10
⊢ (((t(1st ∘ 1st )m ∧ t(2nd ∘ 1st )n) ∧ t2nd b) ↔ (t1st ⟨m, n⟩ ∧ t2nd b)) |
80 | 55, 56, 79 | 3bitr2i 264 |
. . . . . . . . 9
⊢ ((t(1st ∘ 1st )m ∧ t((2nd ∘ 1st ) ⊗ 2nd )⟨n, b⟩) ↔
(t1st ⟨m, n⟩ ∧ t2nd b)) |
81 | 39, 29 | opex 4589 |
. . . . . . . . . 10
⊢ ⟨m, n⟩ ∈ V |
82 | 81, 3 | op1st2nd 5791 |
. . . . . . . . 9
⊢ ((t1st ⟨m, n⟩ ∧ t2nd b) ↔ t =
⟨⟨m, n⟩, b⟩) |
83 | 53, 80, 82 | 3bitri 262 |
. . . . . . . 8
⊢ (t((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))⟨m, ⟨n, b⟩⟩ ↔ t =
⟨⟨m, n⟩, b⟩) |
84 | 83 | rexbii 2640 |
. . . . . . 7
⊢ (∃t ∈ AddC t((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))⟨m, ⟨n, b⟩⟩ ↔ ∃t ∈ AddC t = ⟨⟨m, n⟩, b⟩) |
85 | 52, 84 | bitri 240 |
. . . . . 6
⊢ (⟨m, ⟨n, b⟩⟩ ∈
(((1st ∘ 1st )
⊗ ((2nd ∘ 1st )
⊗ 2nd )) “ AddC ) ↔
∃t ∈ AddC t = ⟨⟨m, n⟩, b⟩) |
86 | | df-br 4641 |
. . . . . . 7
⊢ (⟨m, n⟩ AddC b ↔ ⟨⟨m, n⟩, b⟩ ∈ AddC ) |
87 | | risset 2662 |
. . . . . . 7
⊢ (⟨⟨m, n⟩, b⟩ ∈ AddC ↔ ∃t ∈ AddC t = ⟨⟨m, n⟩, b⟩) |
88 | 86, 87 | bitr2i 241 |
. . . . . 6
⊢ (∃t ∈ AddC t = ⟨⟨m, n⟩, b⟩ ↔ ⟨m, n⟩ AddC b) |
89 | 39, 29 | braddcfn 5827 |
. . . . . . 7
⊢ (⟨m, n⟩ AddC b ↔
(m +c n) = b) |
90 | | eqcom 2355 |
. . . . . . 7
⊢ ((m +c n) = b ↔
b = (m
+c n)) |
91 | 89, 90 | bitri 240 |
. . . . . 6
⊢ (⟨m, n⟩ AddC b ↔
b = (m
+c n)) |
92 | 85, 88, 91 | 3bitri 262 |
. . . . 5
⊢ (⟨m, ⟨n, b⟩⟩ ∈
(((1st ∘ 1st )
⊗ ((2nd ∘ 1st )
⊗ 2nd )) “ AddC ) ↔
b = (m
+c n)) |
93 | 51, 92 | anbi12i 678 |
. . . 4
⊢ ((⟨m, ⟨n, b⟩⟩ ∈ Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∧ ⟨m, ⟨n, b⟩⟩ ∈
(((1st ∘ 1st )
⊗ ((2nd ∘ 1st )
⊗ 2nd )) “ AddC )) ↔
(m = (n
+c n) ∧ b = (m +c n))) |
94 | 2, 93 | bitri 240 |
. . 3
⊢ (⟨m, ⟨n, b⟩⟩ ∈ ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ (m = (n
+c n) ∧ b = (m +c n))) |
95 | 94 | exbii 1582 |
. 2
⊢ (∃m⟨m, ⟨n, b⟩⟩ ∈ ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ ∃m(m = (n
+c n) ∧ b = (m +c n))) |
96 | 29, 29 | addcex 4395 |
. . 3
⊢ (n +c n) ∈
V |
97 | | addceq1 4384 |
. . . 4
⊢ (m = (n
+c n) → (m +c n) = ((n
+c n)
+c n)) |
98 | 97 | eqeq2d 2364 |
. . 3
⊢ (m = (n
+c n) → (b = (m
+c n) ↔ b = ((n
+c n)
+c n))) |
99 | 96, 98 | ceqsexv 2895 |
. 2
⊢ (∃m(m = (n
+c n) ∧ b = (m +c n)) ↔ b =
((n +c n) +c n)) |
100 | 1, 95, 99 | 3bitri 262 |
1
⊢ (⟨n, b⟩ ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ b = ((n
+c n)
+c n)) |