Metamath Proof Explorer


Theorem bj-inftyexpitaudisj

Description: An element of the circle at infinity is not a complex number. (Contributed by BJ, 4-Feb-2023)

Ref Expression
Assertion bj-inftyexpitaudisj ¬ ( +∞e𝐴 ) ∈ ℂ

Proof

Step Hyp Ref Expression
1 2fveq3 ( 𝑥 = 𝐴 → ( {R ‘ ( 1st𝑥 ) ) = ( {R ‘ ( 1st𝐴 ) ) )
2 1 opeq1d ( 𝑥 = 𝐴 → ⟨ ( {R ‘ ( 1st𝑥 ) ) , { R } ⟩ = ⟨ ( {R ‘ ( 1st𝐴 ) ) , { R } ⟩ )
3 df-bj-inftyexpitau +∞e = ( 𝑥 ∈ ℝ ↦ ⟨ ( {R ‘ ( 1st𝑥 ) ) , { R } ⟩ )
4 opex ⟨ ( {R ‘ ( 1st𝐴 ) ) , { R } ⟩ ∈ V
5 2 3 4 fvmpt ( 𝐴 ∈ ℝ → ( +∞e𝐴 ) = ⟨ ( {R ‘ ( 1st𝐴 ) ) , { R } ⟩ )
6 opex ⟨ ( {R ‘ ( 1st𝑦 ) ) , { R } ⟩ ∈ V
7 df-bj-inftyexpitau +∞e = ( 𝑦 ∈ ℝ ↦ ⟨ ( {R ‘ ( 1st𝑦 ) ) , { R } ⟩ )
8 6 7 dmmpti dom +∞e = ℝ
9 5 8 eleq2s ( 𝐴 ∈ dom +∞e → ( +∞e𝐴 ) = ⟨ ( {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 ( ( +∞e𝐴 ) = ⟨ ( {R ‘ ( 1st𝐴 ) ) , { R } ⟩ ↔ ⟨ ( {R ‘ ( 1st𝐴 ) ) , { R } ⟩ = ( +∞e𝐴 ) )
20 19 biimpi ( ( +∞e𝐴 ) = ⟨ ( {R ‘ ( 1st𝐴 ) ) , { R } ⟩ → ⟨ ( {R ‘ ( 1st𝐴 ) ) , { R } ⟩ = ( +∞e𝐴 ) )
21 20 eleq1d ( ( +∞e𝐴 ) = ⟨ ( {R ‘ ( 1st𝐴 ) ) , { R } ⟩ → ( ⟨ ( {R ‘ ( 1st𝐴 ) ) , { R } ⟩ ∈ ℂ ↔ ( +∞e𝐴 ) ∈ ℂ ) )
22 18 21 mtbii ( ( +∞e𝐴 ) = ⟨ ( {R ‘ ( 1st𝐴 ) ) , { R } ⟩ → ¬ ( +∞e𝐴 ) ∈ ℂ )
23 9 22 syl ( 𝐴 ∈ dom +∞e → ¬ ( +∞e𝐴 ) ∈ ℂ )
24 0ncn ¬ ∅ ∈ ℂ
25 ndmfv ( ¬ 𝐴 ∈ dom +∞e → ( +∞e𝐴 ) = ∅ )
26 25 eleq1d ( ¬ 𝐴 ∈ dom +∞e → ( ( +∞e𝐴 ) ∈ ℂ ↔ ∅ ∈ ℂ ) )
27 24 26 mtbiri ( ¬ 𝐴 ∈ dom +∞e → ¬ ( +∞e𝐴 ) ∈ ℂ )
28 23 27 pm2.61i ¬ ( +∞e𝐴 ) ∈ ℂ