Metamath Proof Explorer

Theorem usgr1v

Description: A class with one (or no) vertex is a simple graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017) (Revised by AV, 18-Oct-2020)

Ref Expression
Assertion usgr1v 
|- ( ( G e. W /\ ( Vtx ` G ) = { A } ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) )

Proof

Step Hyp Ref Expression
1 usgr1vr 
 |-  ( ( A e. _V /\ ( Vtx ` G ) = { A } ) -> ( G e. USGraph -> ( iEdg ` G ) = (/) ) )
2 1 adantrl 
 |-  ( ( A e. _V /\ ( G e. W /\ ( Vtx ` G ) = { A } ) ) -> ( G e. USGraph -> ( iEdg ` G ) = (/) ) )
3 simplrl 
 |-  ( ( ( A e. _V /\ ( G e. W /\ ( Vtx ` G ) = { A } ) ) /\ ( iEdg ` G ) = (/) ) -> G e. W )
4 simpr 
 |-  ( ( ( A e. _V /\ ( G e. W /\ ( Vtx ` G ) = { A } ) ) /\ ( iEdg ` G ) = (/) ) -> ( iEdg ` G ) = (/) )
5 3 4 usgr0e 
 |-  ( ( ( A e. _V /\ ( G e. W /\ ( Vtx ` G ) = { A } ) ) /\ ( iEdg ` G ) = (/) ) -> G e. USGraph )
6 5 ex 
 |-  ( ( A e. _V /\ ( G e. W /\ ( Vtx ` G ) = { A } ) ) -> ( ( iEdg ` G ) = (/) -> G e. USGraph ) )
7 2 6 impbid 
 |-  ( ( A e. _V /\ ( G e. W /\ ( Vtx ` G ) = { A } ) ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) )
8 7 ex 
 |-  ( A e. _V -> ( ( G e. W /\ ( Vtx ` G ) = { A } ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) ) )
9 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
10 simpl 
 |-  ( ( G e. W /\ ( Vtx ` G ) = { A } ) -> G e. W )
11 simprr 
 |-  ( ( { A } = (/) /\ ( G e. W /\ ( Vtx ` G ) = { A } ) ) -> ( Vtx ` G ) = { A } )
12 simpl 
 |-  ( ( { A } = (/) /\ ( G e. W /\ ( Vtx ` G ) = { A } ) ) -> { A } = (/) )
13 11 12 eqtrd 
 |-  ( ( { A } = (/) /\ ( G e. W /\ ( Vtx ` G ) = { A } ) ) -> ( Vtx ` G ) = (/) )
14 usgr0vb 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) )
15 10 13 14 syl2an2 
 |-  ( ( { A } = (/) /\ ( G e. W /\ ( Vtx ` G ) = { A } ) ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) )
16 15 ex 
 |-  ( { A } = (/) -> ( ( G e. W /\ ( Vtx ` G ) = { A } ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) ) )
17 9 16 sylbi 
 |-  ( -. A e. _V -> ( ( G e. W /\ ( Vtx ` G ) = { A } ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) ) )
18 8 17 pm2.61i 
 |-  ( ( G e. W /\ ( Vtx ` G ) = { A } ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) )