Theorem cffldtocusgr

Description: The field of complex numbers can be made a complete simple graph with the set of pairs of complex numbers regarded as edges. This theorem demonstrates the capabilities of the current definitions for graphs applied to extensible structures. (Contributed by AV, 14-Nov-2021) (Proof shortened by AV, 17-Nov-2021) Revise df-cnfld . (Revised by GG, 31-Mar-2025)

	Ref	Expression
Hypotheses	cffldtocusgr.p	⊢ 𝑃 = { 𝑥 ∈ 𝒫 ℂ ∣ ( ♯ ‘ 𝑥 ) = 2 }
	cffldtocusgr.g	⊢ 𝐺 = ( ℂfld sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ )
Assertion	cffldtocusgr	⊢ 𝐺 ∈ ComplUSGraph

Proof

Step	Hyp	Ref	Expression
1		cffldtocusgr.p	⊢ 𝑃 = { 𝑥 ∈ 𝒫 ℂ ∣ ( ♯ ‘ 𝑥 ) = 2 }
2		cffldtocusgr.g	⊢ 𝐺 = ( ℂfld sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ )
3		opex	⊢ ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ V
4	3	tpid1	⊢ ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ }
5	4	orci	⊢ ( ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∨ ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } )
6		elun	⊢ ( ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ↔ ( ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∨ ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) )
7	5 6	mpbir	⊢ ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } )
8	7	orci	⊢ ( ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∨ ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
9		df-cnfld	⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
10	9	eleq2i	⊢ ( ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ℂfld ↔ ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) )
11		elun	⊢ ( ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ↔ ( ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∨ ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) )
12	10 11	bitri	⊢ ( ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ℂfld ↔ ( ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∨ ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) )
13	8 12	mpbir	⊢ ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ℂfld
14		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
15	14	pweqi	⊢ 𝒫 ℂ = 𝒫 ( Base ‘ ℂfld )
16	15	rabeqi	⊢ { 𝑥 ∈ 𝒫 ℂ ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 ( Base ‘ ℂfld ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
17	1 16	eqtri	⊢ 𝑃 = { 𝑥 ∈ 𝒫 ( Base ‘ ℂfld ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
18		cnfldstr	⊢ ℂfld Struct ⟨ 1 , ; 1 3 ⟩
19	18	a1i	⊢ ( ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ℂfld → ℂfld Struct ⟨ 1 , ; 1 3 ⟩ )
20		fvex	⊢ ( Base ‘ ndx ) ∈ V
21		cnex	⊢ ℂ ∈ V
22	20 21	opeldm	⊢ ( ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ℂfld → ( Base ‘ ndx ) ∈ dom ℂfld )
23	17 19 2 22	structtocusgr	⊢ ( ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∈ ℂfld → 𝐺 ∈ ComplUSGraph )
24	13 23	ax-mp	⊢ 𝐺 ∈ ComplUSGraph