Theorem isfusgrf1

Description: The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020) (Revised by AV, 21-Oct-2020)

	Ref	Expression
Hypotheses	isfusgr.v	|- V = ( Vtx ` G )
	isfusgrf1.i	|- I = ( iEdg ` G )
Assertion	isfusgrf1	|- ( G e. W -> ( G e. FinUSGraph <-> ( I : dom I -1-1-> { x e. ~P V | ( # ` x ) = 2 } /\ V e. Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfusgr.v	|- V = ( Vtx ` G )
2		isfusgrf1.i	|- I = ( iEdg ` G )
3	1	isfusgr	|- ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
4	1 2	isusgrs	|- ( G e. W -> ( G e. USGraph <-> I : dom I -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) )
5	4	anbi1d	|- ( G e. W -> ( ( G e. USGraph /\ V e. Fin ) <-> ( I : dom I -1-1-> { x e. ~P V | ( # ` x ) = 2 } /\ V e. Fin ) ) )
6	3 5	bitrid	|- ( G e. W -> ( G e. FinUSGraph <-> ( I : dom I -1-1-> { x e. ~P V | ( # ` x ) = 2 } /\ V e. Fin ) ) )