cnfldcjOLD

Description: Obsolete version of cnfldcj as of 27-Apr-2025. (Contributed by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017) (Revised by Thierry Arnoux, 17-Dec-2017) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	cnfldcjOLD	⊢ ∗ = ( *_𝑟 ‘ ℂ_fld )

Proof

Step	Hyp	Ref	Expression
1		cjf	⊢ ∗ : ℂ ⟶ ℂ
2		cnex	⊢ ℂ ∈ V
3		fex2	⊢ ( ( ∗ : ℂ ⟶ ℂ ∧ ℂ ∈ V ∧ ℂ ∈ V ) → ∗ ∈ V )
4	1 2 2 3	mp3an	⊢ ∗ ∈ V
5		cnfldstrOLD	⊢ ℂ_fld Struct ⟨ 1 , ; 1 3 ⟩
6		starvid	⊢ _𝑟 = Slot ( _𝑟 ‘ ndx )
7		ssun2	⊢ { ⟨ ( _𝑟 ‘ ndx ) , ∗ ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( _𝑟 ‘ ndx ) , ∗ ⟩ } )
8		ssun1	⊢ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( _𝑟 ‘ ndx ) , ∗ ⟩ } ) ⊆ ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( _𝑟 ‘ 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	8 9	sseqtrri	⊢ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *_𝑟 ‘ ndx ) , ∗ ⟩ } ) ⊆ ℂ_fld
11	7 10	sstri	⊢ { ⟨ ( *_𝑟 ‘ ndx ) , ∗ ⟩ } ⊆ ℂ_fld
12	5 6 11	strfv	⊢ ( ∗ ∈ V → ∗ = ( *_𝑟 ‘ ℂ_fld ) )
13	4 12	ax-mp	⊢ ∗ = ( *_𝑟 ‘ ℂ_fld )

Metamath Proof Explorer

Theorem cnfldcjOLD

Proof