Metamath Proof Explorer

Theorem nbgr0vtxlem

Description: Lemma for nbgr0vtx and nbgr0edg . (Contributed by AV, 15-Nov-2020)

Ref Expression
Hypothesis nbgr0vtxlem.v 
|- ( ph -> A. n e. ( ( Vtx ` G ) \ { K } ) -. E. e e. ( Edg ` G ) { K , n } C_ e )
Assertion nbgr0vtxlem 
|- ( ph -> ( G NeighbVtx K ) = (/) )

Proof

Step Hyp Ref Expression
1 nbgr0vtxlem.v 
 |-  ( ph -> A. n e. ( ( Vtx ` G ) \ { K } ) -. E. e e. ( Edg ` G ) { K , n } C_ e )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
4 2 3 nbgrval 
 |-  ( K e. ( Vtx ` G ) -> ( G NeighbVtx K ) = { n e. ( ( Vtx ` G ) \ { K } ) | E. e e. ( Edg ` G ) { K , n } C_ e } )
5 4 ad2antrl 
 |-  ( ( ( G e. _V /\ K e. _V ) /\ ( K e. ( Vtx ` G ) /\ ph ) ) -> ( G NeighbVtx K ) = { n e. ( ( Vtx ` G ) \ { K } ) | E. e e. ( Edg ` G ) { K , n } C_ e } )
6 1 ad2antll 
 |-  ( ( ( G e. _V /\ K e. _V ) /\ ( K e. ( Vtx ` G ) /\ ph ) ) -> A. n e. ( ( Vtx ` G ) \ { K } ) -. E. e e. ( Edg ` G ) { K , n } C_ e )
7 rabeq0 
 |-  ( { n e. ( ( Vtx ` G ) \ { K } ) | E. e e. ( Edg ` G ) { K , n } C_ e } = (/) <-> A. n e. ( ( Vtx ` G ) \ { K } ) -. E. e e. ( Edg ` G ) { K , n } C_ e )
8 6 7 sylibr 
 |-  ( ( ( G e. _V /\ K e. _V ) /\ ( K e. ( Vtx ` G ) /\ ph ) ) -> { n e. ( ( Vtx ` G ) \ { K } ) | E. e e. ( Edg ` G ) { K , n } C_ e } = (/) )
9 5 8 eqtrd 
 |-  ( ( ( G e. _V /\ K e. _V ) /\ ( K e. ( Vtx ` G ) /\ ph ) ) -> ( G NeighbVtx K ) = (/) )
10 9 expcom 
 |-  ( ( K e. ( Vtx ` G ) /\ ph ) -> ( ( G e. _V /\ K e. _V ) -> ( G NeighbVtx K ) = (/) ) )
11 10 ex 
 |-  ( K e. ( Vtx ` G ) -> ( ph -> ( ( G e. _V /\ K e. _V ) -> ( G NeighbVtx K ) = (/) ) ) )
12 11 com23 
 |-  ( K e. ( Vtx ` G ) -> ( ( G e. _V /\ K e. _V ) -> ( ph -> ( G NeighbVtx K ) = (/) ) ) )
13 df-nel 
 |-  ( K e/ ( Vtx ` G ) <-> -. K e. ( Vtx ` G ) )
14 2 nbgrnvtx0 
 |-  ( K e/ ( Vtx ` G ) -> ( G NeighbVtx K ) = (/) )
15 13 14 sylbir 
 |-  ( -. K e. ( Vtx ` G ) -> ( G NeighbVtx K ) = (/) )
16 15 a1d 
 |-  ( -. K e. ( Vtx ` G ) -> ( ph -> ( G NeighbVtx K ) = (/) ) )
17 nbgrprc0 
 |-  ( -. ( G e. _V /\ K e. _V ) -> ( G NeighbVtx K ) = (/) )
18 17 a1d 
 |-  ( -. ( G e. _V /\ K e. _V ) -> ( ph -> ( G NeighbVtx K ) = (/) ) )
19 12 16 18 pm2.61nii 
 |-  ( ph -> ( G NeighbVtx K ) = (/) )