Step |
Hyp |
Ref |
Expression |
1 |
|
2fveq3 |
⊢ ( 𝑥 = 𝐴 → ( {R ‘ ( 1st ‘ 𝑥 ) ) = ( {R ‘ ( 1st ‘ 𝐴 ) ) ) |
2 |
1
|
opeq1d |
⊢ ( 𝑥 = 𝐴 → 〈 ( {R ‘ ( 1st ‘ 𝑥 ) ) , { R } 〉 = 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 ) |
3 |
|
df-bj-inftyexpitau |
⊢ +∞eiτ = ( 𝑥 ∈ ℝ ↦ 〈 ( {R ‘ ( 1st ‘ 𝑥 ) ) , { R } 〉 ) |
4 |
|
opex |
⊢ 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 ∈ V |
5 |
2 3 4
|
fvmpt |
⊢ ( 𝐴 ∈ ℝ → ( +∞eiτ ‘ 𝐴 ) = 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 ) |
6 |
|
opex |
⊢ 〈 ( {R ‘ ( 1st ‘ 𝑦 ) ) , { R } 〉 ∈ V |
7 |
|
df-bj-inftyexpitau |
⊢ +∞eiτ = ( 𝑦 ∈ ℝ ↦ 〈 ( {R ‘ ( 1st ‘ 𝑦 ) ) , { R } 〉 ) |
8 |
6 7
|
dmmpti |
⊢ dom +∞eiτ = ℝ |
9 |
5 8
|
eleq2s |
⊢ ( 𝐴 ∈ dom +∞eiτ → ( +∞eiτ ‘ 𝐴 ) = 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 ) |
10 |
|
nrex1 |
⊢ R ∈ V |
11 |
|
bj-nsnid |
⊢ ( R ∈ V → ¬ { R } ∈ R ) |
12 |
10 11
|
ax-mp |
⊢ ¬ { R } ∈ R |
13 |
12
|
intnan |
⊢ ¬ ( ( {R ‘ ( 1st ‘ 𝐴 ) ) ∈ R ∧ { R } ∈ R ) |
14 |
|
opelxp |
⊢ ( 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 ∈ ( R × R ) ↔ ( ( {R ‘ ( 1st ‘ 𝐴 ) ) ∈ R ∧ { R } ∈ R ) ) |
15 |
13 14
|
mtbir |
⊢ ¬ 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 ∈ ( R × R ) |
16 |
|
df-c |
⊢ ℂ = ( R × R ) |
17 |
16
|
eleq2i |
⊢ ( 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 ∈ ℂ ↔ 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 ∈ ( R × R ) ) |
18 |
15 17
|
mtbir |
⊢ ¬ 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 ∈ ℂ |
19 |
|
eqcom |
⊢ ( ( +∞eiτ ‘ 𝐴 ) = 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 ↔ 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 = ( +∞eiτ ‘ 𝐴 ) ) |
20 |
19
|
biimpi |
⊢ ( ( +∞eiτ ‘ 𝐴 ) = 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 → 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 = ( +∞eiτ ‘ 𝐴 ) ) |
21 |
20
|
eleq1d |
⊢ ( ( +∞eiτ ‘ 𝐴 ) = 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 → ( 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 ∈ ℂ ↔ ( +∞eiτ ‘ 𝐴 ) ∈ ℂ ) ) |
22 |
18 21
|
mtbii |
⊢ ( ( +∞eiτ ‘ 𝐴 ) = 〈 ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } 〉 → ¬ ( +∞eiτ ‘ 𝐴 ) ∈ ℂ ) |
23 |
9 22
|
syl |
⊢ ( 𝐴 ∈ dom +∞eiτ → ¬ ( +∞eiτ ‘ 𝐴 ) ∈ ℂ ) |
24 |
|
0ncn |
⊢ ¬ ∅ ∈ ℂ |
25 |
|
ndmfv |
⊢ ( ¬ 𝐴 ∈ dom +∞eiτ → ( +∞eiτ ‘ 𝐴 ) = ∅ ) |
26 |
25
|
eleq1d |
⊢ ( ¬ 𝐴 ∈ dom +∞eiτ → ( ( +∞eiτ ‘ 𝐴 ) ∈ ℂ ↔ ∅ ∈ ℂ ) ) |
27 |
24 26
|
mtbiri |
⊢ ( ¬ 𝐴 ∈ dom +∞eiτ → ¬ ( +∞eiτ ‘ 𝐴 ) ∈ ℂ ) |
28 |
23 27
|
pm2.61i |
⊢ ¬ ( +∞eiτ ‘ 𝐴 ) ∈ ℂ |