Metamath Proof Explorer

Theorem frgrncvvdeqlem1

Description: Lemma 1 for frgrncvvdeq . (Contributed by Alexander van der Vekens, 23-Dec-2017) (Revised by AV, 8-May-2021) (Proof shortened by AV, 12-Feb-2022)

Ref Expression
Hypotheses frgrncvvdeq.v1 
|- V = ( Vtx ` G )
frgrncvvdeq.e 
|- E = ( Edg ` G )
frgrncvvdeq.nx 
|- D = ( G NeighbVtx X )
frgrncvvdeq.ny 
|- N = ( G NeighbVtx Y )
frgrncvvdeq.x 
|- ( ph -> X e. V )
frgrncvvdeq.y 
|- ( ph -> Y e. V )
frgrncvvdeq.ne 
|- ( ph -> X =/= Y )
frgrncvvdeq.xy 
|- ( ph -> Y e/ D )
frgrncvvdeq.f 
|- ( ph -> G e. FriendGraph )
frgrncvvdeq.a 
|- A = ( x e. D |-> ( iota_ y e. N { x , y } e. E ) )
Assertion frgrncvvdeqlem1 
|- ( ph -> X e/ N )

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v1 
 |-  V = ( Vtx ` G )
2 frgrncvvdeq.e 
 |-  E = ( Edg ` G )
3 frgrncvvdeq.nx 
 |-  D = ( G NeighbVtx X )
4 frgrncvvdeq.ny 
 |-  N = ( G NeighbVtx Y )
5 frgrncvvdeq.x 
 |-  ( ph -> X e. V )
6 frgrncvvdeq.y 
 |-  ( ph -> Y e. V )
7 frgrncvvdeq.ne 
 |-  ( ph -> X =/= Y )
8 frgrncvvdeq.xy 
 |-  ( ph -> Y e/ D )
9 frgrncvvdeq.f 
 |-  ( ph -> G e. FriendGraph )
10 frgrncvvdeq.a 
 |-  A = ( x e. D |-> ( iota_ y e. N { x , y } e. E ) )
11 df-nel 
 |-  ( Y e/ D <-> -. Y e. D )
12 3 eleq2i 
 |-  ( Y e. D <-> Y e. ( G NeighbVtx X ) )
13 11 12 xchbinx 
 |-  ( Y e/ D <-> -. Y e. ( G NeighbVtx X ) )
14 8 13 sylib 
 |-  ( ph -> -. Y e. ( G NeighbVtx X ) )
15 nbgrsym 
 |-  ( X e. ( G NeighbVtx Y ) <-> Y e. ( G NeighbVtx X ) )
16 14 15 sylnibr 
 |-  ( ph -> -. X e. ( G NeighbVtx Y ) )
17 neleq2 
 |-  ( N = ( G NeighbVtx Y ) -> ( X e/ N <-> X e/ ( G NeighbVtx Y ) ) )
18 4 17 ax-mp 
 |-  ( X e/ N <-> X e/ ( G NeighbVtx Y ) )
19 df-nel 
 |-  ( X e/ ( G NeighbVtx Y ) <-> -. X e. ( G NeighbVtx Y ) )
20 18 19 bitri 
 |-  ( X e/ N <-> -. X e. ( G NeighbVtx Y ) )
21 16 20 sylibr 
 |-  ( ph -> X e/ N )