Metamath Proof Explorer

Theorem frgrncvvdeqlem2

Description: Lemma 2 for frgrncvvdeq . In a friendship graph, for each neighbor of a vertex there is exactly one neighbor of another vertex so that there is an edge between these two neighbors. (Contributed by Alexander van der Vekens, 22-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 frgrncvvdeqlem2 
|- ( ( ph /\ x e. D ) -> E! y e. N { x , y } e. E )

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 9 adantr 
 |-  ( ( ph /\ x e. D ) -> G e. FriendGraph )
12 3 eleq2i 
 |-  ( x e. D <-> x e. ( G NeighbVtx X ) )
13 1 nbgrisvtx 
 |-  ( x e. ( G NeighbVtx X ) -> x e. V )
14 13 a1i 
 |-  ( ph -> ( x e. ( G NeighbVtx X ) -> x e. V ) )
15 12 14 syl5bi 
 |-  ( ph -> ( x e. D -> x e. V ) )
16 15 imp 
 |-  ( ( ph /\ x e. D ) -> x e. V )
17 6 adantr 
 |-  ( ( ph /\ x e. D ) -> Y e. V )
18 elnelne2 
 |-  ( ( x e. D /\ Y e/ D ) -> x =/= Y )
19 18 expcom 
 |-  ( Y e/ D -> ( x e. D -> x =/= Y ) )
20 8 19 syl 
 |-  ( ph -> ( x e. D -> x =/= Y ) )
21 20 imp 
 |-  ( ( ph /\ x e. D ) -> x =/= Y )
22 16 17 21 3jca 
 |-  ( ( ph /\ x e. D ) -> ( x e. V /\ Y e. V /\ x =/= Y ) )
23 1 2 frcond1 
 |-  ( G e. FriendGraph -> ( ( x e. V /\ Y e. V /\ x =/= Y ) -> E! y e. V { { x , y } , { y , Y } } C_ E ) )
24 11 22 23 sylc 
 |-  ( ( ph /\ x e. D ) -> E! y e. V { { x , y } , { y , Y } } C_ E )
25 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
26 prex 
 |-  { x , y } e. _V
27 prex 
 |-  { y , Y } e. _V
28 26 27 prss 
 |-  ( ( { x , y } e. E /\ { y , Y } e. E ) <-> { { x , y } , { y , Y } } C_ E )
29 ancom 
 |-  ( ( { x , y } e. E /\ { y , Y } e. E ) <-> ( { y , Y } e. E /\ { x , y } e. E ) )
30 28 29 bitr3i 
 |-  ( { { x , y } , { y , Y } } C_ E <-> ( { y , Y } e. E /\ { x , y } e. E ) )
31 30 anbi2i 
 |-  ( ( y e. V /\ { { x , y } , { y , Y } } C_ E ) <-> ( y e. V /\ ( { y , Y } e. E /\ { x , y } e. E ) ) )
32 usgrumgr 
 |-  ( G e. USGraph -> G e. UMGraph )
33 1 2 umgrpredgv 
 |-  ( ( G e. UMGraph /\ { x , y } e. E ) -> ( x e. V /\ y e. V ) )
34 33 simprd 
 |-  ( ( G e. UMGraph /\ { x , y } e. E ) -> y e. V )
35 34 ex 
 |-  ( G e. UMGraph -> ( { x , y } e. E -> y e. V ) )
36 32 35 syl 
 |-  ( G e. USGraph -> ( { x , y } e. E -> y e. V ) )
37 36 adantld 
 |-  ( G e. USGraph -> ( ( { y , Y } e. E /\ { x , y } e. E ) -> y e. V ) )
38 37 pm4.71rd 
 |-  ( G e. USGraph -> ( ( { y , Y } e. E /\ { x , y } e. E ) <-> ( y e. V /\ ( { y , Y } e. E /\ { x , y } e. E ) ) ) )
39 31 38 bitr4id 
 |-  ( G e. USGraph -> ( ( y e. V /\ { { x , y } , { y , Y } } C_ E ) <-> ( { y , Y } e. E /\ { x , y } e. E ) ) )
40 4 eleq2i 
 |-  ( y e. N <-> y e. ( G NeighbVtx Y ) )
41 2 nbusgreledg 
 |-  ( G e. USGraph -> ( y e. ( G NeighbVtx Y ) <-> { y , Y } e. E ) )
42 40 41 bitr2id 
 |-  ( G e. USGraph -> ( { y , Y } e. E <-> y e. N ) )
43 42 anbi1d 
 |-  ( G e. USGraph -> ( ( { y , Y } e. E /\ { x , y } e. E ) <-> ( y e. N /\ { x , y } e. E ) ) )
44 39 43 bitrd 
 |-  ( G e. USGraph -> ( ( y e. V /\ { { x , y } , { y , Y } } C_ E ) <-> ( y e. N /\ { x , y } e. E ) ) )
45 44 eubidv 
 |-  ( G e. USGraph -> ( E! y ( y e. V /\ { { x , y } , { y , Y } } C_ E ) <-> E! y ( y e. N /\ { x , y } e. E ) ) )
46 45 biimpd 
 |-  ( G e. USGraph -> ( E! y ( y e. V /\ { { x , y } , { y , Y } } C_ E ) -> E! y ( y e. N /\ { x , y } e. E ) ) )
47 df-reu 
 |-  ( E! y e. V { { x , y } , { y , Y } } C_ E <-> E! y ( y e. V /\ { { x , y } , { y , Y } } C_ E ) )
48 df-reu 
 |-  ( E! y e. N { x , y } e. E <-> E! y ( y e. N /\ { x , y } e. E ) )
49 46 47 48 3imtr4g 
 |-  ( G e. USGraph -> ( E! y e. V { { x , y } , { y , Y } } C_ E -> E! y e. N { x , y } e. E ) )
50 9 25 49 3syl 
 |-  ( ph -> ( E! y e. V { { x , y } , { y , Y } } C_ E -> E! y e. N { x , y } e. E ) )
51 50 adantr 
 |-  ( ( ph /\ x e. D ) -> ( E! y e. V { { x , y } , { y , Y } } C_ E -> E! y e. N { x , y } e. E ) )
52 24 51 mpd 
 |-  ( ( ph /\ x e. D ) -> E! y e. N { x , y } e. E )