This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cffldtocusgrOLD

Description: Obsolete version of cffldtocusgr as of 27-Apr-2025. (Contributed by AV, 14-Nov-2021) (Proof shortened by AV, 17-Nov-2021) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cffldtocusgrOLD.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 ℂ ∣ ( ♯ ‘ 𝑥 ) = 2 }
2 cffldtocusgrOLD.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 dfcnfldOLD ⊢ ℂ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