# Metamath Proof Explorer

## 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)

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