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