Step | Hyp | Ref
| Expression |
1 | | caddcc 32097 |
. 2
class
+_{ℂ̅} |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cc 9790 |
. . . . . 6
class
ℂ |
4 | | cccbar 32075 |
. . . . . 6
class
ℂ̅ |
5 | 3, 4 | cxp 5026 |
. . . . 5
class (ℂ
× ℂ̅) |
6 | 4, 3 | cxp 5026 |
. . . . 5
class
(ℂ̅ × ℂ) |
7 | 5, 6 | cun 3537 |
. . . 4
class ((ℂ
× ℂ̅) ∪ (ℂ̅ ×
ℂ)) |
8 | | ccchat 32092 |
. . . . . 6
class
ℂ̂ |
9 | 8, 8 | cxp 5026 |
. . . . 5
class
(ℂ̂ × ℂ̂) |
10 | | cccinfty 32071 |
. . . . . 6
class
ℂ_{∞} |
11 | | cdiag2 32061 |
. . . . . 6
class
Diag |
12 | 10, 11 | cfv 5790 |
. . . . 5
class
(Diag‘ℂ_{∞}) |
13 | 9, 12 | cun 3537 |
. . . 4
class
((ℂ̂ × ℂ̂) ∪
(Diag‘ℂ_{∞})) |
14 | 7, 13 | cun 3537 |
. . 3
class
(((ℂ × ℂ̅) ∪ (ℂ̅ ×
ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪
(Diag‘ℂ_{∞}))) |
15 | 2 | cv 1473 |
. . . . . . 7
class 𝑥 |
16 | | c1st 7034 |
. . . . . . 7
class
1^{st} |
17 | 15, 16 | cfv 5790 |
. . . . . 6
class
(1^{st} ‘𝑥) |
18 | | cinfty 32090 |
. . . . . 6
class
∞ |
19 | 17, 18 | wceq 1474 |
. . . . 5
wff
(1^{st} ‘𝑥) = ∞ |
20 | | c2nd 7035 |
. . . . . . 7
class
2^{nd} |
21 | 15, 20 | cfv 5790 |
. . . . . 6
class
(2^{nd} ‘𝑥) |
22 | 21, 18 | wceq 1474 |
. . . . 5
wff
(2^{nd} ‘𝑥) = ∞ |
23 | 19, 22 | wo 381 |
. . . 4
wff
((1^{st} ‘𝑥) = ∞ ∨ (2^{nd} ‘𝑥) = ∞) |
24 | 17, 3 | wcel 1976 |
. . . . 5
wff
(1^{st} ‘𝑥) ∈ ℂ |
25 | 21, 3 | wcel 1976 |
. . . . . 6
wff
(2^{nd} ‘𝑥) ∈ ℂ |
26 | | caddc 9795 |
. . . . . . 7
class
+ |
27 | 17, 21, 26 | co 6527 |
. . . . . 6
class
((1^{st} ‘𝑥) + (2^{nd} ‘𝑥)) |
28 | 25, 27, 21 | cif 4035 |
. . . . 5
class
if((2^{nd} ‘𝑥) ∈ ℂ, ((1^{st}
‘𝑥) + (2^{nd}
‘𝑥)), (2^{nd}
‘𝑥)) |
29 | 24, 28, 17 | cif 4035 |
. . . 4
class
if((1^{st} ‘𝑥) ∈ ℂ, if((2^{nd}
‘𝑥) ∈ ℂ,
((1^{st} ‘𝑥)
+ (2^{nd} ‘𝑥)), (2^{nd} ‘𝑥)), (1^{st} ‘𝑥)) |
30 | 23, 18, 29 | cif 4035 |
. . 3
class
if(((1^{st} ‘𝑥) = ∞ ∨ (2^{nd} ‘𝑥) = ∞), ∞,
if((1^{st} ‘𝑥) ∈ ℂ, if((2^{nd}
‘𝑥) ∈ ℂ,
((1^{st} ‘𝑥)
+ (2^{nd} ‘𝑥)), (2^{nd} ‘𝑥)), (1^{st} ‘𝑥))) |
31 | 2, 14, 30 | cmpt 4637 |
. 2
class (𝑥 ∈ (((ℂ ×
ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂
× ℂ̂) ∪ (Diag‘ℂ_{∞}))) ↦
if(((1^{st} ‘𝑥) = ∞ ∨ (2^{nd} ‘𝑥) = ∞), ∞,
if((1^{st} ‘𝑥) ∈ ℂ, if((2^{nd}
‘𝑥) ∈ ℂ,
((1^{st} ‘𝑥)
+ (2^{nd} ‘𝑥)), (2^{nd} ‘𝑥)), (1^{st} ‘𝑥)))) |
32 | 1, 31 | wceq 1474 |
1
wff
+_{ℂ̅} = (𝑥 ∈ (((ℂ × ℂ̅)
∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ ×
ℂ̂) ∪ (Diag‘ℂ_{∞}))) ↦
if(((1^{st} ‘𝑥) = ∞ ∨ (2^{nd} ‘𝑥) = ∞), ∞,
if((1^{st} ‘𝑥) ∈ ℂ, if((2^{nd}
‘𝑥) ∈ ℂ,
((1^{st} ‘𝑥)
+ (2^{nd} ‘𝑥)), (2^{nd} ‘𝑥)), (1^{st} ‘𝑥)))) |