Metamath Proof Explorer

Theorem frgr3v

Description: Any graph with three vertices which are completely connected with each other is a friendship graph. (Contributed by Alexander van der Vekens, 5-Oct-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Hypotheses frgr3v.v 
|- V = ( Vtx ` G )
frgr3v.e 
|- E = ( Edg ` G )
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 frgr3v.v 
 |-  V = ( Vtx ` G )
2 frgr3v.e 
 |-  E = ( Edg ` G )
3 1 2 isfrgr 
 |-  ( G e. FriendGraph <-> ( G e. USGraph /\ A. k e. V A. l e. ( V \ { k } ) E! x e. V { { x , k } , { x , l } } C_ E ) )
4 3 a1i 
 |-  ( ( ( ( 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 <-> ( G e. USGraph /\ A. k e. V A. l e. ( V \ { k } ) E! x e. V { { x , k } , { x , l } } C_ E ) ) )
5 id 
 |-  ( V = { A , B , C } -> V = { A , B , C } )
6 difeq1 
 |-  ( V = { A , B , C } -> ( V \ { k } ) = ( { A , B , C } \ { k } ) )
7 reueq1 
 |-  ( V = { A , B , C } -> ( E! x e. V { { x , k } , { x , l } } C_ E <-> E! x e. { A , B , C } { { x , k } , { x , l } } C_ E ) )
8 6 7 raleqbidv 
 |-  ( V = { A , B , C } -> ( A. l e. ( V \ { k } ) E! x e. V { { x , k } , { x , l } } C_ E <-> A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ E ) )
9 5 8 raleqbidv 
 |-  ( V = { A , B , C } -> ( A. k e. V A. l e. ( V \ { k } ) E! x e. V { { x , k } , { x , l } } C_ E <-> A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ E ) )
10 9 anbi2d 
 |-  ( V = { A , B , C } -> ( ( G e. USGraph /\ A. k e. V A. l e. ( V \ { k } ) E! x e. V { { x , k } , { x , l } } C_ E ) <-> ( G e. USGraph /\ A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ E ) ) )
11 10 baibd 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( ( G e. USGraph /\ A. k e. V A. l e. ( V \ { k } ) E! x e. V { { x , k } , { x , l } } C_ E ) <-> A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ E ) )
12 11 adantl 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( ( G e. USGraph /\ A. k e. V A. l e. ( V \ { k } ) E! x e. V { { x , k } , { x , l } } C_ E ) <-> A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ E ) )
13 4 12 bitrd 
 |-  ( ( ( ( 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. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ E ) )
14 sneq 
 |-  ( k = A -> { k } = { A } )
15 14 difeq2d 
 |-  ( k = A -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { A } ) )
16 preq2 
 |-  ( k = A -> { x , k } = { x , A } )
17 16 preq1d 
 |-  ( k = A -> { { x , k } , { x , l } } = { { x , A } , { x , l } } )
18 17 sseq1d 
 |-  ( k = A -> ( { { x , k } , { x , l } } C_ E <-> { { x , A } , { x , l } } C_ E ) )
19 18 reubidv 
 |-  ( k = A -> ( E! x e. { A , B , C } { { x , k } , { x , l } } C_ E <-> E! x e. { A , B , C } { { x , A } , { x , l } } C_ E ) )
20 15 19 raleqbidv 
 |-  ( k = A -> ( A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ E <-> A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ E ) )
21 sneq 
 |-  ( k = B -> { k } = { B } )
22 21 difeq2d 
 |-  ( k = B -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { B } ) )
23 preq2 
 |-  ( k = B -> { x , k } = { x , B } )
24 23 preq1d 
 |-  ( k = B -> { { x , k } , { x , l } } = { { x , B } , { x , l } } )
25 24 sseq1d 
 |-  ( k = B -> ( { { x , k } , { x , l } } C_ E <-> { { x , B } , { x , l } } C_ E ) )
26 25 reubidv 
 |-  ( k = B -> ( E! x e. { A , B , C } { { x , k } , { x , l } } C_ E <-> E! x e. { A , B , C } { { x , B } , { x , l } } C_ E ) )
27 22 26 raleqbidv 
 |-  ( k = B -> ( A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ E <-> A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ E ) )
28 sneq 
 |-  ( k = C -> { k } = { C } )
29 28 difeq2d 
 |-  ( k = C -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { C } ) )
30 preq2 
 |-  ( k = C -> { x , k } = { x , C } )
31 30 preq1d 
 |-  ( k = C -> { { x , k } , { x , l } } = { { x , C } , { x , l } } )
32 31 sseq1d 
 |-  ( k = C -> ( { { x , k } , { x , l } } C_ E <-> { { x , C } , { x , l } } C_ E ) )
33 32 reubidv 
 |-  ( k = C -> ( E! x e. { A , B , C } { { x , k } , { x , l } } C_ E <-> E! x e. { A , B , C } { { x , C } , { x , l } } C_ E ) )
34 29 33 raleqbidv 
 |-  ( k = C -> ( A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ E <-> A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ E ) )
35 20 27 34 raltpg 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ E <-> ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ E ) ) )
36 35 ad2antrr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ E <-> ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ E ) ) )
37 tprot 
 |-  { A , B , C } = { B , C , A }
38 37 a1i 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> { A , B , C } = { B , C , A } )
39 38 difeq1d 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = ( { B , C , A } \ { A } ) )
40 necom 
 |-  ( A =/= B <-> B =/= A )
41 40 biimpi 
 |-  ( A =/= B -> B =/= A )
42 necom 
 |-  ( A =/= C <-> C =/= A )
43 42 biimpi 
 |-  ( A =/= C -> C =/= A )
44 41 43 anim12i 
 |-  ( ( A =/= B /\ A =/= C ) -> ( B =/= A /\ C =/= A ) )
45 44 3adant3 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( B =/= A /\ C =/= A ) )
46 diftpsn3 
 |-  ( ( B =/= A /\ C =/= A ) -> ( { B , C , A } \ { A } ) = { B , C } )
47 45 46 syl 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { B , C , A } \ { A } ) = { B , C } )
48 39 47 eqtrd 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = { B , C } )
49 48 raleqdv 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ E <-> A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ E ) )
50 tprot 
 |-  { C , A , B } = { A , B , C }
51 50 eqcomi 
 |-  { A , B , C } = { C , A , B }
52 51 a1i 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> { A , B , C } = { C , A , B } )
53 52 difeq1d 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = ( { C , A , B } \ { B } ) )
54 id 
 |-  ( A =/= B -> A =/= B )
55 necom 
 |-  ( B =/= C <-> C =/= B )
56 55 biimpi 
 |-  ( B =/= C -> C =/= B )
57 54 56 anim12ci 
 |-  ( ( A =/= B /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
58 57 3adant2 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
59 diftpsn3 
 |-  ( ( C =/= B /\ A =/= B ) -> ( { C , A , B } \ { B } ) = { C , A } )
60 58 59 syl 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { C , A , B } \ { B } ) = { C , A } )
61 53 60 eqtrd 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = { C , A } )
62 61 raleqdv 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ E <-> A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ E ) )
63 diftpsn3 
 |-  ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
64 63 3adant1 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
65 64 raleqdv 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ E <-> A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ E ) )
66 49 62 65 3anbi123d 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ E ) <-> ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ E ) ) )
67 66 ad2antlr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ E ) <-> ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ E ) ) )
68 preq2 
 |-  ( l = B -> { x , l } = { x , B } )
69 68 preq2d 
 |-  ( l = B -> { { x , A } , { x , l } } = { { x , A } , { x , B } } )
70 69 sseq1d 
 |-  ( l = B -> ( { { x , A } , { x , l } } C_ E <-> { { x , A } , { x , B } } C_ E ) )
71 70 reubidv 
 |-  ( l = B -> ( E! x e. { A , B , C } { { x , A } , { x , l } } C_ E <-> E! x e. { A , B , C } { { x , A } , { x , B } } C_ E ) )
72 preq2 
 |-  ( l = C -> { x , l } = { x , C } )
73 72 preq2d 
 |-  ( l = C -> { { x , A } , { x , l } } = { { x , A } , { x , C } } )
74 73 sseq1d 
 |-  ( l = C -> ( { { x , A } , { x , l } } C_ E <-> { { x , A } , { x , C } } C_ E ) )
75 74 reubidv 
 |-  ( l = C -> ( E! x e. { A , B , C } { { x , A } , { x , l } } C_ E <-> E! x e. { A , B , C } { { x , A } , { x , C } } C_ E ) )
76 71 75 ralprg 
 |-  ( ( B e. Y /\ C e. Z ) -> ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ E <-> ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ E ) ) )
77 76 3adant1 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ E <-> ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ E ) ) )
78 72 preq2d 
 |-  ( l = C -> { { x , B } , { x , l } } = { { x , B } , { x , C } } )
79 78 sseq1d 
 |-  ( l = C -> ( { { x , B } , { x , l } } C_ E <-> { { x , B } , { x , C } } C_ E ) )
80 79 reubidv 
 |-  ( l = C -> ( E! x e. { A , B , C } { { x , B } , { x , l } } C_ E <-> E! x e. { A , B , C } { { x , B } , { x , C } } C_ E ) )
81 preq2 
 |-  ( l = A -> { x , l } = { x , A } )
82 81 preq2d 
 |-  ( l = A -> { { x , B } , { x , l } } = { { x , B } , { x , A } } )
83 82 sseq1d 
 |-  ( l = A -> ( { { x , B } , { x , l } } C_ E <-> { { x , B } , { x , A } } C_ E ) )
84 83 reubidv 
 |-  ( l = A -> ( E! x e. { A , B , C } { { x , B } , { x , l } } C_ E <-> E! x e. { A , B , C } { { x , B } , { x , A } } C_ E ) )
85 80 84 ralprg 
 |-  ( ( C e. Z /\ A e. X ) -> ( A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ E <-> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ E ) ) )
86 85 ancoms 
 |-  ( ( A e. X /\ C e. Z ) -> ( A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ E <-> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ E ) ) )
87 86 3adant2 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ E <-> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ E ) ) )
88 81 preq2d 
 |-  ( l = A -> { { x , C } , { x , l } } = { { x , C } , { x , A } } )
89 88 sseq1d 
 |-  ( l = A -> ( { { x , C } , { x , l } } C_ E <-> { { x , C } , { x , A } } C_ E ) )
90 89 reubidv 
 |-  ( l = A -> ( E! x e. { A , B , C } { { x , C } , { x , l } } C_ E <-> E! x e. { A , B , C } { { x , C } , { x , A } } C_ E ) )
91 68 preq2d 
 |-  ( l = B -> { { x , C } , { x , l } } = { { x , C } , { x , B } } )
92 91 sseq1d 
 |-  ( l = B -> ( { { x , C } , { x , l } } C_ E <-> { { x , C } , { x , B } } C_ E ) )
93 92 reubidv 
 |-  ( l = B -> ( E! x e. { A , B , C } { { x , C } , { x , l } } C_ E <-> E! x e. { A , B , C } { { x , C } , { x , B } } C_ E ) )
94 90 93 ralprg 
 |-  ( ( A e. X /\ B e. Y ) -> ( A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ E <-> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ E ) ) )
95 94 3adant3 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ E <-> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ E ) ) )
96 77 87 95 3anbi123d 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ E ) <-> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ E ) ) ) )
97 96 ad2antrr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ E ) <-> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ E ) ) ) )
98 36 67 97 3bitrd 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ E <-> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ E ) ) ) )
99 1 2 frgr3vlem2 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( V = { A , B , C } /\ G e. USGraph ) -> ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E <-> ( { C , A } e. E /\ { C , B } e. E ) ) ) )
100 99 imp 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E <-> ( { C , A } e. E /\ { C , B } e. E ) ) )
101 simpll1 
 |-  ( ( ( ( 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 )
102 simpll3 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C e. Z )
103 simpll2 
 |-  ( ( ( ( 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 )
104 101 102 103 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 /\ C e. Z /\ B e. Y ) )
105 simplr2 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A =/= C )
106 simplr1 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A =/= B )
107 58 simpld 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> C =/= B )
108 107 ad2antlr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C =/= B )
109 105 106 108 3jca 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( A =/= C /\ A =/= B /\ C =/= B ) )
110 tpcomb 
 |-  { A , B , C } = { A , C , B }
111 5 110 eqtrdi 
 |-  ( V = { A , B , C } -> V = { A , C , B } )
112 111 anim1i 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( V = { A , C , B } /\ G e. USGraph ) )
113 112 adantl 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( V = { A , C , B } /\ G e. USGraph ) )
114 reueq1 
 |-  ( { A , B , C } = { A , C , B } -> ( E! x e. { A , B , C } { { x , A } , { x , C } } C_ E <-> E! x e. { A , C , B } { { x , A } , { x , C } } C_ E ) )
115 110 114 mp1i 
 |-  ( ( ( ( A e. X /\ C e. Z /\ B e. Y ) /\ ( A =/= C /\ A =/= B /\ C =/= B ) ) /\ ( V = { A , C , B } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , A } , { x , C } } C_ E <-> E! x e. { A , C , B } { { x , A } , { x , C } } C_ E ) )
116 1 2 frgr3vlem2 
 |-  ( ( ( A e. X /\ C e. Z /\ B e. Y ) /\ ( A =/= C /\ A =/= B /\ C =/= B ) ) -> ( ( V = { A , C , B } /\ G e. USGraph ) -> ( E! x e. { A , C , B } { { x , A } , { x , C } } C_ E <-> ( { B , A } e. E /\ { B , C } e. E ) ) ) )
117 116 imp 
 |-  ( ( ( ( A e. X /\ C e. Z /\ B e. Y ) /\ ( A =/= C /\ A =/= B /\ C =/= B ) ) /\ ( V = { A , C , B } /\ G e. USGraph ) ) -> ( E! x e. { A , C , B } { { x , A } , { x , C } } C_ E <-> ( { B , A } e. E /\ { B , C } e. E ) ) )
118 115 117 bitrd 
 |-  ( ( ( ( A e. X /\ C e. Z /\ B e. Y ) /\ ( A =/= C /\ A =/= B /\ C =/= B ) ) /\ ( V = { A , C , B } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , A } , { x , C } } C_ E <-> ( { B , A } e. E /\ { B , C } e. E ) ) )
119 104 109 113 118 syl21anc 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , A } , { x , C } } C_ E <-> ( { B , A } e. E /\ { B , C } e. E ) ) )
120 100 119 anbi12d 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ E ) <-> ( ( { C , A } e. E /\ { C , B } e. E ) /\ ( { B , A } e. E /\ { B , C } e. E ) ) ) )
121 103 102 101 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 /\ C e. Z /\ A e. X ) )
122 simplr3 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B =/= C )
123 106 necomd 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B =/= A )
124 105 necomd 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C =/= A )
125 122 123 124 3jca 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( B =/= C /\ B =/= A /\ C =/= A ) )
126 37 eqeq2i 
 |-  ( V = { A , B , C } <-> V = { B , C , A } )
127 126 biimpi 
 |-  ( V = { A , B , C } -> V = { B , C , A } )
128 127 anim1i 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( V = { B , C , A } /\ G e. USGraph ) )
129 128 adantl 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( V = { B , C , A } /\ G e. USGraph ) )
130 reueq1 
 |-  ( { A , B , C } = { B , C , A } -> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ E <-> E! x e. { B , C , A } { { x , B } , { x , C } } C_ E ) )
131 37 130 mp1i 
 |-  ( ( ( ( B e. Y /\ C e. Z /\ A e. X ) /\ ( B =/= C /\ B =/= A /\ C =/= A ) ) /\ ( V = { B , C , A } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ E <-> E! x e. { B , C , A } { { x , B } , { x , C } } C_ E ) )
132 1 2 frgr3vlem2 
 |-  ( ( ( B e. Y /\ C e. Z /\ A e. X ) /\ ( B =/= C /\ B =/= A /\ C =/= A ) ) -> ( ( V = { B , C , A } /\ G e. USGraph ) -> ( E! x e. { B , C , A } { { x , B } , { x , C } } C_ E <-> ( { A , B } e. E /\ { A , C } e. E ) ) ) )
133 132 imp 
 |-  ( ( ( ( B e. Y /\ C e. Z /\ A e. X ) /\ ( B =/= C /\ B =/= A /\ C =/= A ) ) /\ ( V = { B , C , A } /\ G e. USGraph ) ) -> ( E! x e. { B , C , A } { { x , B } , { x , C } } C_ E <-> ( { A , B } e. E /\ { A , C } e. E ) ) )
134 131 133 bitrd 
 |-  ( ( ( ( B e. Y /\ C e. Z /\ A e. X ) /\ ( B =/= C /\ B =/= A /\ C =/= A ) ) /\ ( V = { B , C , A } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ E <-> ( { A , B } e. E /\ { A , C } e. E ) ) )
135 121 125 129 134 syl21anc 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ E <-> ( { A , B } e. E /\ { A , C } e. E ) ) )
136 103 101 102 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 /\ C e. Z ) )
137 123 122 105 3jca 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( B =/= A /\ B =/= C /\ A =/= C ) )
138 tpcoma 
 |-  { A , B , C } = { B , A , C }
139 138 eqeq2i 
 |-  ( V = { A , B , C } <-> V = { B , A , C } )
140 139 biimpi 
 |-  ( V = { A , B , C } -> V = { B , A , C } )
141 140 anim1i 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( V = { B , A , C } /\ G e. USGraph ) )
142 141 adantl 
 |-  ( ( ( ( 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 ) )
143 reueq1 
 |-  ( { A , B , C } = { B , A , C } -> ( E! x e. { A , B , C } { { x , B } , { x , A } } C_ E <-> E! x e. { B , A , C } { { x , B } , { x , A } } C_ E ) )
144 138 143 mp1i 
 |-  ( ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( B =/= A /\ B =/= C /\ A =/= C ) ) /\ ( V = { B , A , C } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , B } , { x , A } } C_ E <-> E! x e. { B , A , C } { { x , B } , { x , A } } C_ E ) )
145 1 2 frgr3vlem2 
 |-  ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( B =/= A /\ B =/= C /\ A =/= C ) ) -> ( ( V = { B , A , C } /\ G e. USGraph ) -> ( E! x e. { B , A , C } { { x , B } , { x , A } } C_ E <-> ( { C , B } e. E /\ { C , A } e. E ) ) ) )
146 145 imp 
 |-  ( ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( B =/= A /\ B =/= C /\ A =/= C ) ) /\ ( V = { B , A , C } /\ G e. USGraph ) ) -> ( E! x e. { B , A , C } { { x , B } , { x , A } } C_ E <-> ( { C , B } e. E /\ { C , A } e. E ) ) )
147 144 146 bitrd 
 |-  ( ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( B =/= A /\ B =/= C /\ A =/= C ) ) /\ ( V = { B , A , C } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , B } , { x , A } } C_ E <-> ( { C , B } e. E /\ { C , A } e. E ) ) )
148 136 137 142 147 syl21anc 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , B } , { x , A } } C_ E <-> ( { C , B } e. E /\ { C , A } e. E ) ) )
149 135 148 anbi12d 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ E ) <-> ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { C , B } e. E /\ { C , A } e. E ) ) ) )
150 102 101 103 3jca 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( C e. Z /\ A e. X /\ B e. Y ) )
151 124 108 106 3jca 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( C =/= A /\ C =/= B /\ A =/= B ) )
152 51 eqeq2i 
 |-  ( V = { A , B , C } <-> V = { C , A , B } )
153 152 biimpi 
 |-  ( V = { A , B , C } -> V = { C , A , B } )
154 153 anim1i 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( V = { C , A , B } /\ G e. USGraph ) )
155 154 adantl 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( V = { C , A , B } /\ G e. USGraph ) )
156 reueq1 
 |-  ( { A , B , C } = { C , A , B } -> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ E <-> E! x e. { C , A , B } { { x , C } , { x , A } } C_ E ) )
157 51 156 mp1i 
 |-  ( ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( C =/= A /\ C =/= B /\ A =/= B ) ) /\ ( V = { C , A , B } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ E <-> E! x e. { C , A , B } { { x , C } , { x , A } } C_ E ) )
158 1 2 frgr3vlem2 
 |-  ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( C =/= A /\ C =/= B /\ A =/= B ) ) -> ( ( V = { C , A , B } /\ G e. USGraph ) -> ( E! x e. { C , A , B } { { x , C } , { x , A } } C_ E <-> ( { B , C } e. E /\ { B , A } e. E ) ) ) )
159 158 imp 
 |-  ( ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( C =/= A /\ C =/= B /\ A =/= B ) ) /\ ( V = { C , A , B } /\ G e. USGraph ) ) -> ( E! x e. { C , A , B } { { x , C } , { x , A } } C_ E <-> ( { B , C } e. E /\ { B , A } e. E ) ) )
160 157 159 bitrd 
 |-  ( ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( C =/= A /\ C =/= B /\ A =/= B ) ) /\ ( V = { C , A , B } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ E <-> ( { B , C } e. E /\ { B , A } e. E ) ) )
161 150 151 155 160 syl21anc 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ E <-> ( { B , C } e. E /\ { B , A } e. E ) ) )
162 3anrev 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( C e. Z /\ B e. Y /\ A e. X ) )
163 162 biimpi 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( C e. Z /\ B e. Y /\ A e. X ) )
164 55 42 40 3anbi123i 
 |-  ( ( B =/= C /\ A =/= C /\ A =/= B ) <-> ( C =/= B /\ C =/= A /\ B =/= A ) )
165 164 biimpi 
 |-  ( ( B =/= C /\ A =/= C /\ A =/= B ) -> ( C =/= B /\ C =/= A /\ B =/= A ) )
166 165 3com13 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= B /\ C =/= A /\ B =/= A ) )
167 163 166 anim12i 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) )
168 tpcoma 
 |-  { B , C , A } = { C , B , A }
169 37 168 eqtri 
 |-  { A , B , C } = { C , B , A }
170 169 eqeq2i 
 |-  ( V = { A , B , C } <-> V = { C , B , A } )
171 170 biimpi 
 |-  ( V = { A , B , C } -> V = { C , B , A } )
172 171 anim1i 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( V = { C , B , A } /\ G e. USGraph ) )
173 reueq1 
 |-  ( { A , B , C } = { C , B , A } -> ( E! x e. { A , B , C } { { x , C } , { x , B } } C_ E <-> E! x e. { C , B , A } { { x , C } , { x , B } } C_ E ) )
174 169 173 mp1i 
 |-  ( ( ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) /\ ( V = { C , B , A } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , C } , { x , B } } C_ E <-> E! x e. { C , B , A } { { x , C } , { x , B } } C_ E ) )
175 1 2 frgr3vlem2 
 |-  ( ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) -> ( ( V = { C , B , A } /\ G e. USGraph ) -> ( E! x e. { C , B , A } { { x , C } , { x , B } } C_ E <-> ( { A , C } e. E /\ { A , B } e. E ) ) ) )
176 175 imp 
 |-  ( ( ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) /\ ( V = { C , B , A } /\ G e. USGraph ) ) -> ( E! x e. { C , B , A } { { x , C } , { x , B } } C_ E <-> ( { A , C } e. E /\ { A , B } e. E ) ) )
177 174 176 bitrd 
 |-  ( ( ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) /\ ( V = { C , B , A } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , C } , { x , B } } C_ E <-> ( { A , C } e. E /\ { A , B } e. E ) ) )
178 167 172 177 syl2an 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , C } , { x , B } } C_ E <-> ( { A , C } e. E /\ { A , B } e. E ) ) )
179 161 178 anbi12d 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ E ) <-> ( ( { B , C } e. E /\ { B , A } e. E ) /\ ( { A , C } e. E /\ { A , B } e. E ) ) ) )
180 120 149 179 3anbi123d 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ E ) ) <-> ( ( ( { C , A } e. E /\ { C , B } e. E ) /\ ( { B , A } e. E /\ { B , C } e. E ) ) /\ ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { C , B } e. E /\ { C , A } e. E ) ) /\ ( ( { B , C } e. E /\ { B , A } e. E ) /\ ( { A , C } e. E /\ { A , B } e. E ) ) ) ) )
181 prcom 
 |-  { B , C } = { C , B }
182 181 eleq1i 
 |-  ( { B , C } e. E <-> { C , B } e. E )
183 182 anbi2i 
 |-  ( ( { B , A } e. E /\ { B , C } e. E ) <-> ( { B , A } e. E /\ { C , B } e. E ) )
184 183 anbi2i 
 |-  ( ( ( { C , A } e. E /\ { C , B } e. E ) /\ ( { B , A } e. E /\ { B , C } e. E ) ) <-> ( ( { C , A } e. E /\ { C , B } e. E ) /\ ( { B , A } e. E /\ { C , B } e. E ) ) )
185 anandir 
 |-  ( ( ( { C , A } e. E /\ { B , A } e. E ) /\ { C , B } e. E ) <-> ( ( { C , A } e. E /\ { C , B } e. E ) /\ ( { B , A } e. E /\ { C , B } e. E ) ) )
186 184 185 bitr4i 
 |-  ( ( ( { C , A } e. E /\ { C , B } e. E ) /\ ( { B , A } e. E /\ { B , C } e. E ) ) <-> ( ( { C , A } e. E /\ { B , A } e. E ) /\ { C , B } e. E ) )
187 prcom 
 |-  { C , A } = { A , C }
188 187 eleq1i 
 |-  ( { C , A } e. E <-> { A , C } e. E )
189 188 anbi2i 
 |-  ( ( { C , B } e. E /\ { C , A } e. E ) <-> ( { C , B } e. E /\ { A , C } e. E ) )
190 189 anbi2i 
 |-  ( ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { C , B } e. E /\ { C , A } e. E ) ) <-> ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { C , B } e. E /\ { A , C } e. E ) ) )
191 anandir 
 |-  ( ( ( { A , B } e. E /\ { C , B } e. E ) /\ { A , C } e. E ) <-> ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { C , B } e. E /\ { A , C } e. E ) ) )
192 190 191 bitr4i 
 |-  ( ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { C , B } e. E /\ { C , A } e. E ) ) <-> ( ( { A , B } e. E /\ { C , B } e. E ) /\ { A , C } e. E ) )
193 prcom 
 |-  { A , B } = { B , A }
194 193 eleq1i 
 |-  ( { A , B } e. E <-> { B , A } e. E )
195 194 anbi2i 
 |-  ( ( { A , C } e. E /\ { A , B } e. E ) <-> ( { A , C } e. E /\ { B , A } e. E ) )
196 195 anbi2i 
 |-  ( ( ( { B , C } e. E /\ { B , A } e. E ) /\ ( { A , C } e. E /\ { A , B } e. E ) ) <-> ( ( { B , C } e. E /\ { B , A } e. E ) /\ ( { A , C } e. E /\ { B , A } e. E ) ) )
197 anandir 
 |-  ( ( ( { B , C } e. E /\ { A , C } e. E ) /\ { B , A } e. E ) <-> ( ( { B , C } e. E /\ { B , A } e. E ) /\ ( { A , C } e. E /\ { B , A } e. E ) ) )
198 196 197 bitr4i 
 |-  ( ( ( { B , C } e. E /\ { B , A } e. E ) /\ ( { A , C } e. E /\ { A , B } e. E ) ) <-> ( ( { B , C } e. E /\ { A , C } e. E ) /\ { B , A } e. E ) )
199 186 192 198 3anbi123i 
 |-  ( ( ( ( { C , A } e. E /\ { C , B } e. E ) /\ ( { B , A } e. E /\ { B , C } e. E ) ) /\ ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { C , B } e. E /\ { C , A } e. E ) ) /\ ( ( { B , C } e. E /\ { B , A } e. E ) /\ ( { A , C } e. E /\ { A , B } e. E ) ) ) <-> ( ( ( { C , A } e. E /\ { B , A } e. E ) /\ { C , B } e. E ) /\ ( ( { A , B } e. E /\ { C , B } e. E ) /\ { A , C } e. E ) /\ ( ( { B , C } e. E /\ { A , C } e. E ) /\ { B , A } e. E ) ) )
200 3anrot 
 |-  ( ( { C , A } e. E /\ { B , A } e. E /\ { C , B } e. E ) <-> ( { B , A } e. E /\ { C , B } e. E /\ { C , A } e. E ) )
201 df-3an 
 |-  ( ( { C , A } e. E /\ { B , A } e. E /\ { C , B } e. E ) <-> ( ( { C , A } e. E /\ { B , A } e. E ) /\ { C , B } e. E ) )
202 prcom 
 |-  { B , A } = { A , B }
203 202 eleq1i 
 |-  ( { B , A } e. E <-> { A , B } e. E )
204 prcom 
 |-  { C , B } = { B , C }
205 204 eleq1i 
 |-  ( { C , B } e. E <-> { B , C } e. E )
206 biid 
 |-  ( { C , A } e. E <-> { C , A } e. E )
207 203 205 206 3anbi123i 
 |-  ( ( { B , A } e. E /\ { C , B } e. E /\ { C , A } e. E ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) )
208 200 201 207 3bitr3i 
 |-  ( ( ( { C , A } e. E /\ { B , A } e. E ) /\ { C , B } e. E ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) )
209 df-3an 
 |-  ( ( { A , B } e. E /\ { C , B } e. E /\ { A , C } e. E ) <-> ( ( { A , B } e. E /\ { C , B } e. E ) /\ { A , C } e. E ) )
210 biid 
 |-  ( { A , B } e. E <-> { A , B } e. E )
211 prcom 
 |-  { A , C } = { C , A }
212 211 eleq1i 
 |-  ( { A , C } e. E <-> { C , A } e. E )
213 210 205 212 3anbi123i 
 |-  ( ( { A , B } e. E /\ { C , B } e. E /\ { A , C } e. E ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) )
214 209 213 bitr3i 
 |-  ( ( ( { A , B } e. E /\ { C , B } e. E ) /\ { A , C } e. E ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) )
215 df-3an 
 |-  ( ( { B , C } e. E /\ { A , C } e. E /\ { B , A } e. E ) <-> ( ( { B , C } e. E /\ { A , C } e. E ) /\ { B , A } e. E ) )
216 3anrot 
 |-  ( ( { B , C } e. E /\ { A , C } e. E /\ { B , A } e. E ) <-> ( { A , C } e. E /\ { B , A } e. E /\ { B , C } e. E ) )
217 3anrot 
 |-  ( ( { A , C } e. E /\ { B , A } e. E /\ { B , C } e. E ) <-> ( { B , A } e. E /\ { B , C } e. E /\ { A , C } e. E ) )
218 biid 
 |-  ( { B , C } e. E <-> { B , C } e. E )
219 203 218 212 3anbi123i 
 |-  ( ( { B , A } e. E /\ { B , C } e. E /\ { A , C } e. E ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) )
220 216 217 219 3bitri 
 |-  ( ( { B , C } e. E /\ { A , C } e. E /\ { B , A } e. E ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) )
221 215 220 bitr3i 
 |-  ( ( ( { B , C } e. E /\ { A , C } e. E ) /\ { B , A } e. E ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) )
222 208 214 221 3anbi123i 
 |-  ( ( ( ( { C , A } e. E /\ { B , A } e. E ) /\ { C , B } e. E ) /\ ( ( { A , B } e. E /\ { C , B } e. E ) /\ { A , C } e. E ) /\ ( ( { B , C } e. E /\ { A , C } e. E ) /\ { B , A } e. E ) ) <-> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
223 df-3an 
 |-  ( ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) <-> ( ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
224 anabs1 
 |-  ( ( ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) <-> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
225 anidm 
 |-  ( ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) )
226 223 224 225 3bitri 
 |-  ( ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) )
227 199 222 226 3bitri 
 |-  ( ( ( ( { C , A } e. E /\ { C , B } e. E ) /\ ( { B , A } e. E /\ { B , C } e. E ) ) /\ ( ( { A , B } e. E /\ { A , C } e. E ) /\ ( { C , B } e. E /\ { C , A } e. E ) ) /\ ( ( { B , C } e. E /\ { B , A } e. E ) /\ ( { A , C } e. E /\ { A , B } e. E ) ) ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) )
228 180 227 syl6bb 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ E ) ) <-> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) )
229 13 98 228 3bitrd 
 |-  ( ( ( ( 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 ) ) )
230 229 ex 
 |-  ( ( ( 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 ) ) ) )