Metamath Proof Explorer

Theorem 3vfriswmgr

Description: Every friendship graph with three (different) vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

Ref Expression
Hypotheses 3vfriswmgr.v 
|- V = ( Vtx ` G )
3vfriswmgr.e 
|- E = ( Edg ` G )
Assertion 3vfriswmgr 
|- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) )

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v 
 |-  V = ( Vtx ` G )
2 3vfriswmgr.e 
 |-  E = ( Edg ` G )
3 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
4 1 2 frgr3v 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( V = { A , B , C } /\ G e. USGraph ) -> ( G e. FriendGraph <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) ) )
5 4 exp4b 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( V = { A , B , C } -> ( G e. USGraph -> ( G e. FriendGraph <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) ) ) ) )
6 5 3imp1 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> ( G e. FriendGraph <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
7 prcom 
 |-  { C , A } = { A , C }
8 7 eleq1i 
 |-  ( { C , A } e. E <-> { A , C } e. E )
9 8 biimpi 
 |-  ( { C , A } e. E -> { A , C } e. E )
10 9 3ad2ant3 
 |-  ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) -> { A , C } e. E )
11 10 adantl 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> { A , C } e. E )
12 simpl11 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> A e. X )
13 simpl12 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> B e. Y )
14 simp1 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> A =/= B )
15 14 3ad2ant2 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> A =/= B )
16 15 adantr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> A =/= B )
17 12 13 16 3jca 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> ( A e. X /\ B e. Y /\ A =/= B ) )
18 simp3 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> V = { A , B , C } )
19 18 anim1i 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> ( V = { A , B , C } /\ G e. USGraph ) )
20 17 19 jca 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) )
21 simp1 
 |-  ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) -> { A , B } e. E )
22 1 2 3vfriswmgrlem 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { A , B } e. E -> E! w e. { A , B } { A , w } e. E ) )
23 22 imp 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> E! w e. { A , B } { A , w } e. E )
24 20 21 23 syl2an 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> E! w e. { A , B } { A , w } e. E )
25 11 24 jca 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> ( { A , C } e. E /\ E! w e. { A , B } { A , w } e. E ) )
26 simpr2 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> { B , C } e. E )
27 necom 
 |-  ( A =/= B <-> B =/= A )
28 27 biimpi 
 |-  ( A =/= B -> B =/= A )
29 28 3ad2ant1 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> B =/= A )
30 29 3ad2ant2 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> B =/= A )
31 30 adantr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> B =/= A )
32 13 12 31 3jca 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> ( B e. Y /\ A e. X /\ B =/= A ) )
33 tpcoma 
 |-  { A , B , C } = { B , A , C }
34 18 33 eqtrdi 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> V = { B , A , C } )
35 34 anim1i 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> ( V = { B , A , C } /\ G e. USGraph ) )
36 32 35 jca 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> ( ( B e. Y /\ A e. X /\ B =/= A ) /\ ( V = { B , A , C } /\ G e. USGraph ) ) )
37 prcom 
 |-  { A , B } = { B , A }
38 37 eleq1i 
 |-  ( { A , B } e. E <-> { B , A } e. E )
39 38 biimpi 
 |-  ( { A , B } e. E -> { B , A } e. E )
40 39 3ad2ant1 
 |-  ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) -> { B , A } e. E )
41 1 2 3vfriswmgrlem 
 |-  ( ( ( B e. Y /\ A e. X /\ B =/= A ) /\ ( V = { B , A , C } /\ G e. USGraph ) ) -> ( { B , A } e. E -> E! w e. { B , A } { B , w } e. E ) )
42 41 imp 
 |-  ( ( ( ( B e. Y /\ A e. X /\ B =/= A ) /\ ( V = { B , A , C } /\ G e. USGraph ) ) /\ { B , A } e. E ) -> E! w e. { B , A } { B , w } e. E )
43 reueq1 
 |-  ( { A , B } = { B , A } -> ( E! w e. { A , B } { B , w } e. E <-> E! w e. { B , A } { B , w } e. E ) )
44 37 43 ax-mp 
 |-  ( E! w e. { A , B } { B , w } e. E <-> E! w e. { B , A } { B , w } e. E )
45 42 44 sylibr 
 |-  ( ( ( ( B e. Y /\ A e. X /\ B =/= A ) /\ ( V = { B , A , C } /\ G e. USGraph ) ) /\ { B , A } e. E ) -> E! w e. { A , B } { B , w } e. E )
46 36 40 45 syl2an 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> E! w e. { A , B } { B , w } e. E )
47 26 46 jca 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> ( { B , C } e. E /\ E! w e. { A , B } { B , w } e. E ) )
48 25 47 jca 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> ( ( { A , C } e. E /\ E! w e. { A , B } { A , w } e. E ) /\ ( { B , C } e. E /\ E! w e. { A , B } { B , w } e. E ) ) )
49 preq1 
 |-  ( v = A -> { v , C } = { A , C } )
50 49 eleq1d 
 |-  ( v = A -> ( { v , C } e. E <-> { A , C } e. E ) )
51 preq1 
 |-  ( v = A -> { v , w } = { A , w } )
52 51 eleq1d 
 |-  ( v = A -> ( { v , w } e. E <-> { A , w } e. E ) )
53 52 reubidv 
 |-  ( v = A -> ( E! w e. { A , B } { v , w } e. E <-> E! w e. { A , B } { A , w } e. E ) )
54 50 53 anbi12d 
 |-  ( v = A -> ( ( { v , C } e. E /\ E! w e. { A , B } { v , w } e. E ) <-> ( { A , C } e. E /\ E! w e. { A , B } { A , w } e. E ) ) )
55 preq1 
 |-  ( v = B -> { v , C } = { B , C } )
56 55 eleq1d 
 |-  ( v = B -> ( { v , C } e. E <-> { B , C } e. E ) )
57 preq1 
 |-  ( v = B -> { v , w } = { B , w } )
58 57 eleq1d 
 |-  ( v = B -> ( { v , w } e. E <-> { B , w } e. E ) )
59 58 reubidv 
 |-  ( v = B -> ( E! w e. { A , B } { v , w } e. E <-> E! w e. { A , B } { B , w } e. E ) )
60 56 59 anbi12d 
 |-  ( v = B -> ( ( { v , C } e. E /\ E! w e. { A , B } { v , w } e. E ) <-> ( { B , C } e. E /\ E! w e. { A , B } { B , w } e. E ) ) )
61 54 60 ralprg 
 |-  ( ( A e. X /\ B e. Y ) -> ( A. v e. { A , B } ( { v , C } e. E /\ E! w e. { A , B } { v , w } e. E ) <-> ( ( { A , C } e. E /\ E! w e. { A , B } { A , w } e. E ) /\ ( { B , C } e. E /\ E! w e. { A , B } { B , w } e. E ) ) ) )
62 61 3adant3 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. v e. { A , B } ( { v , C } e. E /\ E! w e. { A , B } { v , w } e. E ) <-> ( ( { A , C } e. E /\ E! w e. { A , B } { A , w } e. E ) /\ ( { B , C } e. E /\ E! w e. { A , B } { B , w } e. E ) ) ) )
63 62 3ad2ant1 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> ( A. v e. { A , B } ( { v , C } e. E /\ E! w e. { A , B } { v , w } e. E ) <-> ( ( { A , C } e. E /\ E! w e. { A , B } { A , w } e. E ) /\ ( { B , C } e. E /\ E! w e. { A , B } { B , w } e. E ) ) ) )
64 63 adantr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> ( A. v e. { A , B } ( { v , C } e. E /\ E! w e. { A , B } { v , w } e. E ) <-> ( ( { A , C } e. E /\ E! w e. { A , B } { A , w } e. E ) /\ ( { B , C } e. E /\ E! w e. { A , B } { B , w } e. E ) ) ) )
65 64 adantr 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> ( A. v e. { A , B } ( { v , C } e. E /\ E! w e. { A , B } { v , w } e. E ) <-> ( ( { A , C } e. E /\ E! w e. { A , B } { A , w } e. E ) /\ ( { B , C } e. E /\ E! w e. { A , B } { B , w } e. E ) ) ) )
66 48 65 mpbird 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> A. v e. { A , B } ( { v , C } e. E /\ E! w e. { A , B } { v , w } e. E ) )
67 diftpsn3 
 |-  ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
68 67 3adant1 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
69 reueq1 
 |-  ( ( { A , B , C } \ { C } ) = { A , B } -> ( E! w e. ( { A , B , C } \ { C } ) { v , w } e. E <-> E! w e. { A , B } { v , w } e. E ) )
70 68 69 syl 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( E! w e. ( { A , B , C } \ { C } ) { v , w } e. E <-> E! w e. { A , B } { v , w } e. E ) )
71 70 anbi2d 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( ( { v , C } e. E /\ E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) <-> ( { v , C } e. E /\ E! w e. { A , B } { v , w } e. E ) ) )
72 68 71 raleqbidv 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( A. v e. ( { A , B , C } \ { C } ) ( { v , C } e. E /\ E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) <-> A. v e. { A , B } ( { v , C } e. E /\ E! w e. { A , B } { v , w } e. E ) ) )
73 72 3ad2ant2 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> ( A. v e. ( { A , B , C } \ { C } ) ( { v , C } e. E /\ E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) <-> A. v e. { A , B } ( { v , C } e. E /\ E! w e. { A , B } { v , w } e. E ) ) )
74 73 adantr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> ( A. v e. ( { A , B , C } \ { C } ) ( { v , C } e. E /\ E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) <-> A. v e. { A , B } ( { v , C } e. E /\ E! w e. { A , B } { v , w } e. E ) ) )
75 74 adantr 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> ( A. v e. ( { A , B , C } \ { C } ) ( { v , C } e. E /\ E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) <-> A. v e. { A , B } ( { v , C } e. E /\ E! w e. { A , B } { v , w } e. E ) ) )
76 66 75 mpbird 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> A. v e. ( { A , B , C } \ { C } ) ( { v , C } e. E /\ E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) )
77 76 3mix3d 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> ( A. v e. ( { A , B , C } \ { A } ) ( { v , A } e. E /\ E! w e. ( { A , B , C } \ { A } ) { v , w } e. E ) \/ A. v e. ( { A , B , C } \ { B } ) ( { v , B } e. E /\ E! w e. ( { A , B , C } \ { B } ) { v , w } e. E ) \/ A. v e. ( { A , B , C } \ { C } ) ( { v , C } e. E /\ E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) ) )
78 sneq 
 |-  ( h = A -> { h } = { A } )
79 78 difeq2d 
 |-  ( h = A -> ( { A , B , C } \ { h } ) = ( { A , B , C } \ { A } ) )
80 preq2 
 |-  ( h = A -> { v , h } = { v , A } )
81 80 eleq1d 
 |-  ( h = A -> ( { v , h } e. E <-> { v , A } e. E ) )
82 reueq1 
 |-  ( ( { A , B , C } \ { h } ) = ( { A , B , C } \ { A } ) -> ( E! w e. ( { A , B , C } \ { h } ) { v , w } e. E <-> E! w e. ( { A , B , C } \ { A } ) { v , w } e. E ) )
83 79 82 syl 
 |-  ( h = A -> ( E! w e. ( { A , B , C } \ { h } ) { v , w } e. E <-> E! w e. ( { A , B , C } \ { A } ) { v , w } e. E ) )
84 81 83 anbi12d 
 |-  ( h = A -> ( ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) <-> ( { v , A } e. E /\ E! w e. ( { A , B , C } \ { A } ) { v , w } e. E ) ) )
85 79 84 raleqbidv 
 |-  ( h = A -> ( A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) <-> A. v e. ( { A , B , C } \ { A } ) ( { v , A } e. E /\ E! w e. ( { A , B , C } \ { A } ) { v , w } e. E ) ) )
86 sneq 
 |-  ( h = B -> { h } = { B } )
87 86 difeq2d 
 |-  ( h = B -> ( { A , B , C } \ { h } ) = ( { A , B , C } \ { B } ) )
88 preq2 
 |-  ( h = B -> { v , h } = { v , B } )
89 88 eleq1d 
 |-  ( h = B -> ( { v , h } e. E <-> { v , B } e. E ) )
90 reueq1 
 |-  ( ( { A , B , C } \ { h } ) = ( { A , B , C } \ { B } ) -> ( E! w e. ( { A , B , C } \ { h } ) { v , w } e. E <-> E! w e. ( { A , B , C } \ { B } ) { v , w } e. E ) )
91 87 90 syl 
 |-  ( h = B -> ( E! w e. ( { A , B , C } \ { h } ) { v , w } e. E <-> E! w e. ( { A , B , C } \ { B } ) { v , w } e. E ) )
92 89 91 anbi12d 
 |-  ( h = B -> ( ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) <-> ( { v , B } e. E /\ E! w e. ( { A , B , C } \ { B } ) { v , w } e. E ) ) )
93 87 92 raleqbidv 
 |-  ( h = B -> ( A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) <-> A. v e. ( { A , B , C } \ { B } ) ( { v , B } e. E /\ E! w e. ( { A , B , C } \ { B } ) { v , w } e. E ) ) )
94 sneq 
 |-  ( h = C -> { h } = { C } )
95 94 difeq2d 
 |-  ( h = C -> ( { A , B , C } \ { h } ) = ( { A , B , C } \ { C } ) )
96 preq2 
 |-  ( h = C -> { v , h } = { v , C } )
97 96 eleq1d 
 |-  ( h = C -> ( { v , h } e. E <-> { v , C } e. E ) )
98 reueq1 
 |-  ( ( { A , B , C } \ { h } ) = ( { A , B , C } \ { C } ) -> ( E! w e. ( { A , B , C } \ { h } ) { v , w } e. E <-> E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) )
99 95 98 syl 
 |-  ( h = C -> ( E! w e. ( { A , B , C } \ { h } ) { v , w } e. E <-> E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) )
100 97 99 anbi12d 
 |-  ( h = C -> ( ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) <-> ( { v , C } e. E /\ E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) ) )
101 95 100 raleqbidv 
 |-  ( h = C -> ( A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) <-> A. v e. ( { A , B , C } \ { C } ) ( { v , C } e. E /\ E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) ) )
102 85 93 101 rextpg 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) <-> ( A. v e. ( { A , B , C } \ { A } ) ( { v , A } e. E /\ E! w e. ( { A , B , C } \ { A } ) { v , w } e. E ) \/ A. v e. ( { A , B , C } \ { B } ) ( { v , B } e. E /\ E! w e. ( { A , B , C } \ { B } ) { v , w } e. E ) \/ A. v e. ( { A , B , C } \ { C } ) ( { v , C } e. E /\ E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) ) ) )
103 102 3ad2ant1 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> ( E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) <-> ( A. v e. ( { A , B , C } \ { A } ) ( { v , A } e. E /\ E! w e. ( { A , B , C } \ { A } ) { v , w } e. E ) \/ A. v e. ( { A , B , C } \ { B } ) ( { v , B } e. E /\ E! w e. ( { A , B , C } \ { B } ) { v , w } e. E ) \/ A. v e. ( { A , B , C } \ { C } ) ( { v , C } e. E /\ E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) ) ) )
104 103 adantr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> ( E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) <-> ( A. v e. ( { A , B , C } \ { A } ) ( { v , A } e. E /\ E! w e. ( { A , B , C } \ { A } ) { v , w } e. E ) \/ A. v e. ( { A , B , C } \ { B } ) ( { v , B } e. E /\ E! w e. ( { A , B , C } \ { B } ) { v , w } e. E ) \/ A. v e. ( { A , B , C } \ { C } ) ( { v , C } e. E /\ E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) ) ) )
105 104 adantr 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> ( E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) <-> ( A. v e. ( { A , B , C } \ { A } ) ( { v , A } e. E /\ E! w e. ( { A , B , C } \ { A } ) { v , w } e. E ) \/ A. v e. ( { A , B , C } \ { B } ) ( { v , B } e. E /\ E! w e. ( { A , B , C } \ { B } ) { v , w } e. E ) \/ A. v e. ( { A , B , C } \ { C } ) ( { v , C } e. E /\ E! w e. ( { A , B , C } \ { C } ) { v , w } e. E ) ) ) )
106 77 105 mpbird 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) )
107 106 ex 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) -> E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) ) )
108 6 107 sylbid 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) /\ G e. USGraph ) -> ( G e. FriendGraph -> E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) ) )
109 108 expcom 
 |-  ( G e. USGraph -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> ( G e. FriendGraph -> E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) ) ) )
110 109 com23 
 |-  ( G e. USGraph -> ( G e. FriendGraph -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) ) ) )
111 3 110 mpcom 
 |-  ( G e. FriendGraph -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) ) )
112 111 com12 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> ( G e. FriendGraph -> E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) ) )
113 difeq1 
 |-  ( V = { A , B , C } -> ( V \ { h } ) = ( { A , B , C } \ { h } ) )
114 reueq1 
 |-  ( ( V \ { h } ) = ( { A , B , C } \ { h } ) -> ( E! w e. ( V \ { h } ) { v , w } e. E <-> E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) )
115 113 114 syl 
 |-  ( V = { A , B , C } -> ( E! w e. ( V \ { h } ) { v , w } e. E <-> E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) )
116 115 anbi2d 
 |-  ( V = { A , B , C } -> ( ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) <-> ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) ) )
117 113 116 raleqbidv 
 |-  ( V = { A , B , C } -> ( A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) <-> A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) ) )
118 117 rexeqbi1dv 
 |-  ( V = { A , B , C } -> ( E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) <-> E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) ) )
119 118 imbi2d 
 |-  ( V = { A , B , C } -> ( ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) <-> ( G e. FriendGraph -> E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) ) ) )
120 119 3ad2ant3 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> ( ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) <-> ( G e. FriendGraph -> E. h e. { A , B , C } A. v e. ( { A , B , C } \ { h } ) ( { v , h } e. E /\ E! w e. ( { A , B , C } \ { h } ) { v , w } e. E ) ) ) )
121 112 120 mpbird 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ V = { A , B , C } ) -> ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) )