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 
|- P = { x e. ~P CC | ( # ` x ) = 2 }
cffldtocusgrOLD.g 
|- G = ( CCfld sSet <. ( .ef ` ndx ) , ( _I |` P ) >. )
Assertion cffldtocusgrOLD 
|- G e. ComplUSGraph

Proof

Step Hyp Ref Expression
1 cffldtocusgrOLD.p 
 |-  P = { x e. ~P CC | ( # ` x ) = 2 }
2 cffldtocusgrOLD.g 
 |-  G = ( CCfld sSet <. ( .ef ` ndx ) , ( _I |` P ) >. )
3 opex 
 |-  <. ( Base ` ndx ) , CC >. e. _V
4 3 tpid1 
 |-  <. ( Base ` ndx ) , CC >. e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. }
5 4 orci 
 |-  ( <. ( Base ` ndx ) , CC >. e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } \/ <. ( Base ` ndx ) , CC >. e. { <. ( *r ` ndx ) , * >. } )
6 elun 
 |-  ( <. ( Base ` ndx ) , CC >. e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) <-> ( <. ( Base ` ndx ) , CC >. e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } \/ <. ( Base ` ndx ) , CC >. e. { <. ( *r ` ndx ) , * >. } ) )
7 5 6 mpbir 
 |-  <. ( Base ` ndx ) , CC >. e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } )
8 7 orci 
 |-  ( <. ( Base ` ndx ) , CC >. e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) \/ <. ( Base ` ndx ) , CC >. e. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
9 dfcnfldOLD 
 |-  CCfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
10 9 eleq2i 
 |-  ( <. ( Base ` ndx ) , CC >. e. CCfld <-> <. ( Base ` ndx ) , CC >. e. ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
11 elun 
 |-  ( <. ( Base ` ndx ) , CC >. e. ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) <-> ( <. ( Base ` ndx ) , CC >. e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) \/ <. ( Base ` ndx ) , CC >. e. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
12 10 11 bitri 
 |-  ( <. ( Base ` ndx ) , CC >. e. CCfld <-> ( <. ( Base ` ndx ) , CC >. e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) \/ <. ( Base ` ndx ) , CC >. e. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
13 8 12 mpbir 
 |-  <. ( Base ` ndx ) , CC >. e. CCfld
14 cnfldbas 
 |-  CC = ( Base ` CCfld )
15 14 pweqi 
 |-  ~P CC = ~P ( Base ` CCfld )
16 15 rabeqi 
 |-  { x e. ~P CC | ( # ` x ) = 2 } = { x e. ~P ( Base ` CCfld ) | ( # ` x ) = 2 }
17 1 16 eqtri 
 |-  P = { x e. ~P ( Base ` CCfld ) | ( # ` x ) = 2 }
18 cnfldstr 
 |-  CCfld Struct <. 1 , ; 1 3 >.
19 18 a1i 
 |-  ( <. ( Base ` ndx ) , CC >. e. CCfld -> CCfld Struct <. 1 , ; 1 3 >. )
20 fvex 
 |-  ( Base ` ndx ) e. _V
21 cnex 
 |-  CC e. _V
22 20 21 opeldm 
 |-  ( <. ( Base ` ndx ) , CC >. e. CCfld -> ( Base ` ndx ) e. dom CCfld )
23 17 19 2 22 structtocusgr 
 |-  ( <. ( Base ` ndx ) , CC >. e. CCfld -> G e. ComplUSGraph )
24 13 23 ax-mp 
 |-  G e. ComplUSGraph