Theorem cnfldex

Description: The field of complex numbers is a set. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 14-Aug-2015) (Revised by Thierry Arnoux, 17-Dec-2017) Avoid complex number axioms and ax-pow . (Revised by GG, 16-Mar-2025)

	Ref	Expression
Assertion	cnfldex	⊢ ℂfld ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-cnfld	⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
2		tpex	⊢ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ } ∈ V
3		snex	⊢ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∈ V
4	2 3	unex	⊢ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∈ V
5		tpex	⊢ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∈ V
6		snex	⊢ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ∈ V
7	5 6	unex	⊢ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ∈ V
8	4 7	unex	⊢ ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ∈ V
9	1 8	eqeltri	⊢ ℂfld ∈ V