Metamath Proof Explorer

Theorem frgrncvvdeqlem3

Description: Lemma 3 for frgrncvvdeq . The unique neighbor of a vertex (expressed by a restricted iota) is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 18-Dec-2017) (Revised by AV, 10-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 frgrncvvdeqlem3 
|- ( ( ph /\ x e. D ) -> { ( iota_ y e. N { x , y } e. E ) } = ( ( G NeighbVtx x ) i^i 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 4 ineq2i 
 |-  ( ( G NeighbVtx x ) i^i N ) = ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) )
12 9 adantr 
 |-  ( ( ph /\ x e. D ) -> G e. FriendGraph )
13 3 eleq2i 
 |-  ( x e. D <-> x e. ( G NeighbVtx X ) )
14 1 nbgrisvtx 
 |-  ( x e. ( G NeighbVtx X ) -> x e. V )
15 14 a1i 
 |-  ( ph -> ( x e. ( G NeighbVtx X ) -> x e. V ) )
16 13 15 syl5bi 
 |-  ( ph -> ( x e. D -> x e. V ) )
17 16 imp 
 |-  ( ( ph /\ x e. D ) -> x e. V )
18 6 adantr 
 |-  ( ( ph /\ x e. D ) -> Y e. V )
19 elnelne2 
 |-  ( ( x e. D /\ Y e/ D ) -> x =/= Y )
20 8 19 sylan2 
 |-  ( ( x e. D /\ ph ) -> x =/= Y )
21 20 ancoms 
 |-  ( ( ph /\ x e. D ) -> x =/= Y )
22 17 18 21 3jca 
 |-  ( ( ph /\ x e. D ) -> ( x e. V /\ Y e. V /\ x =/= Y ) )
23 1 2 frcond3 
 |-  ( G e. FriendGraph -> ( ( x e. V /\ Y e. V /\ x =/= Y ) -> E. n e. V ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { n } ) )
24 12 22 23 sylc 
 |-  ( ( ph /\ x e. D ) -> E. n e. V ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { n } )
25 vex 
 |-  n e. _V
26 elinsn 
 |-  ( ( n e. _V /\ ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { n } ) -> ( n e. ( G NeighbVtx x ) /\ n e. ( G NeighbVtx Y ) ) )
27 25 26 mpan 
 |-  ( ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { n } -> ( n e. ( G NeighbVtx x ) /\ n e. ( G NeighbVtx Y ) ) )
28 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
29 2 nbusgreledg 
 |-  ( G e. USGraph -> ( n e. ( G NeighbVtx x ) <-> { n , x } e. E ) )
30 prcom 
 |-  { n , x } = { x , n }
31 30 eleq1i 
 |-  ( { n , x } e. E <-> { x , n } e. E )
32 29 31 bitrdi 
 |-  ( G e. USGraph -> ( n e. ( G NeighbVtx x ) <-> { x , n } e. E ) )
33 32 biimpd 
 |-  ( G e. USGraph -> ( n e. ( G NeighbVtx x ) -> { x , n } e. E ) )
34 9 28 33 3syl 
 |-  ( ph -> ( n e. ( G NeighbVtx x ) -> { x , n } e. E ) )
35 34 adantr 
 |-  ( ( ph /\ x e. D ) -> ( n e. ( G NeighbVtx x ) -> { x , n } e. E ) )
36 35 com12 
 |-  ( n e. ( G NeighbVtx x ) -> ( ( ph /\ x e. D ) -> { x , n } e. E ) )
37 36 adantr 
 |-  ( ( n e. ( G NeighbVtx x ) /\ n e. ( G NeighbVtx Y ) ) -> ( ( ph /\ x e. D ) -> { x , n } e. E ) )
38 37 imp 
 |-  ( ( ( n e. ( G NeighbVtx x ) /\ n e. ( G NeighbVtx Y ) ) /\ ( ph /\ x e. D ) ) -> { x , n } e. E )
39 4 eqcomi 
 |-  ( G NeighbVtx Y ) = N
40 39 eleq2i 
 |-  ( n e. ( G NeighbVtx Y ) <-> n e. N )
41 40 biimpi 
 |-  ( n e. ( G NeighbVtx Y ) -> n e. N )
42 41 adantl 
 |-  ( ( n e. ( G NeighbVtx x ) /\ n e. ( G NeighbVtx Y ) ) -> n e. N )
43 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem2 
 |-  ( ( ph /\ x e. D ) -> E! y e. N { x , y } e. E )
44 preq2 
 |-  ( y = n -> { x , y } = { x , n } )
45 44 eleq1d 
 |-  ( y = n -> ( { x , y } e. E <-> { x , n } e. E ) )
46 45 riota2 
 |-  ( ( n e. N /\ E! y e. N { x , y } e. E ) -> ( { x , n } e. E <-> ( iota_ y e. N { x , y } e. E ) = n ) )
47 42 43 46 syl2an 
 |-  ( ( ( n e. ( G NeighbVtx x ) /\ n e. ( G NeighbVtx Y ) ) /\ ( ph /\ x e. D ) ) -> ( { x , n } e. E <-> ( iota_ y e. N { x , y } e. E ) = n ) )
48 38 47 mpbid 
 |-  ( ( ( n e. ( G NeighbVtx x ) /\ n e. ( G NeighbVtx Y ) ) /\ ( ph /\ x e. D ) ) -> ( iota_ y e. N { x , y } e. E ) = n )
49 27 48 sylan 
 |-  ( ( ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { n } /\ ( ph /\ x e. D ) ) -> ( iota_ y e. N { x , y } e. E ) = n )
50 49 eqcomd 
 |-  ( ( ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { n } /\ ( ph /\ x e. D ) ) -> n = ( iota_ y e. N { x , y } e. E ) )
51 50 sneqd 
 |-  ( ( ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { n } /\ ( ph /\ x e. D ) ) -> { n } = { ( iota_ y e. N { x , y } e. E ) } )
52 eqeq1 
 |-  ( ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { n } -> ( ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { ( iota_ y e. N { x , y } e. E ) } <-> { n } = { ( iota_ y e. N { x , y } e. E ) } ) )
53 52 adantr 
 |-  ( ( ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { n } /\ ( ph /\ x e. D ) ) -> ( ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { ( iota_ y e. N { x , y } e. E ) } <-> { n } = { ( iota_ y e. N { x , y } e. E ) } ) )
54 51 53 mpbird 
 |-  ( ( ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { n } /\ ( ph /\ x e. D ) ) -> ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { ( iota_ y e. N { x , y } e. E ) } )
55 54 ex 
 |-  ( ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { n } -> ( ( ph /\ x e. D ) -> ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { ( iota_ y e. N { x , y } e. E ) } ) )
56 55 rexlimivw 
 |-  ( E. n e. V ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { n } -> ( ( ph /\ x e. D ) -> ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { ( iota_ y e. N { x , y } e. E ) } ) )
57 24 56 mpcom 
 |-  ( ( ph /\ x e. D ) -> ( ( G NeighbVtx x ) i^i ( G NeighbVtx Y ) ) = { ( iota_ y e. N { x , y } e. E ) } )
58 11 57 eqtr2id 
 |-  ( ( ph /\ x e. D ) -> { ( iota_ y e. N { x , y } e. E ) } = ( ( G NeighbVtx x ) i^i N ) )