Metamath Proof Explorer

Theorem frgr3vlem1

Description: Lemma 1 for frgr3v . (Contributed by Alexander van der Vekens, 4-Oct-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Hypotheses frgr3v.v 
|- V = ( Vtx ` G )
frgr3v.e 
|- E = ( Edg ` G )
Assertion frgr3vlem1 
|- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A. x A. y ( ( ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) /\ ( y e. { A , B , C } /\ { { y , A } , { y , B } } C_ E ) ) -> x = y ) )

Proof

Step Hyp Ref Expression
1 frgr3v.v 
 |-  V = ( Vtx ` G )
2 frgr3v.e 
 |-  E = ( Edg ` G )
3 vex 
 |-  x e. _V
4 3 eltp 
 |-  ( x e. { A , B , C } <-> ( x = A \/ x = B \/ x = C ) )
5 vex 
 |-  y e. _V
6 5 eltp 
 |-  ( y e. { A , B , C } <-> ( y = A \/ y = B \/ y = C ) )
7 eqidd 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = A )
8 7 a1i 
 |-  ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = A ) )
9 8 a1i13 
 |-  ( y = A -> ( { { A , A } , { A , B } } C_ E -> ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = A ) ) ) )
10 preq1 
 |-  ( y = A -> { y , A } = { A , A } )
11 preq1 
 |-  ( y = A -> { y , B } = { A , B } )
12 10 11 preq12d 
 |-  ( y = A -> { { y , A } , { y , B } } = { { A , A } , { A , B } } )
13 12 sseq1d 
 |-  ( y = A -> ( { { y , A } , { y , B } } C_ E <-> { { A , A } , { A , B } } C_ E ) )
14 eqeq2 
 |-  ( y = A -> ( A = y <-> A = A ) )
15 14 imbi2d 
 |-  ( y = A -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = y ) <-> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = A ) ) )
16 15 imbi2d 
 |-  ( y = A -> ( ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = y ) ) <-> ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = A ) ) ) )
17 9 13 16 3imtr4d 
 |-  ( y = A -> ( { { y , A } , { y , B } } C_ E -> ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = y ) ) ) )
18 prex 
 |-  { A , A } e. _V
19 prex 
 |-  { A , B } e. _V
20 18 19 prss 
 |-  ( ( { A , A } e. E /\ { A , B } e. E ) <-> { { A , A } , { A , B } } C_ E )
21 2 usgredgne 
 |-  ( ( G e. USGraph /\ { A , A } e. E ) -> A =/= A )
22 21 adantll 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { A , A } e. E ) -> A =/= A )
23 df-ne 
 |-  ( A =/= A <-> -. A = A )
24 eqid 
 |-  A = A
25 24 pm2.24i 
 |-  ( -. A = A -> A = B )
26 23 25 sylbi 
 |-  ( A =/= A -> A = B )
27 22 26 syl 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { A , A } e. E ) -> A = B )
28 27 expcom 
 |-  ( { A , A } e. E -> ( ( V = { A , B , C } /\ G e. USGraph ) -> A = B ) )
29 28 adantr 
 |-  ( ( { A , A } e. E /\ { A , B } e. E ) -> ( ( V = { A , B , C } /\ G e. USGraph ) -> A = B ) )
30 20 29 sylbir 
 |-  ( { { A , A } , { A , B } } C_ E -> ( ( V = { A , B , C } /\ G e. USGraph ) -> A = B ) )
31 30 com12 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( { { A , A } , { A , B } } C_ E -> A = B ) )
32 31 3ad2ant3 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { { A , A } , { A , B } } C_ E -> A = B ) )
33 32 com12 
 |-  ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = B ) )
34 33 2a1i 
 |-  ( y = B -> ( { { B , A } , { B , B } } C_ E -> ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = B ) ) ) )
35 preq1 
 |-  ( y = B -> { y , A } = { B , A } )
36 preq1 
 |-  ( y = B -> { y , B } = { B , B } )
37 35 36 preq12d 
 |-  ( y = B -> { { y , A } , { y , B } } = { { B , A } , { B , B } } )
38 37 sseq1d 
 |-  ( y = B -> ( { { y , A } , { y , B } } C_ E <-> { { B , A } , { B , B } } C_ E ) )
39 eqeq2 
 |-  ( y = B -> ( A = y <-> A = B ) )
40 39 imbi2d 
 |-  ( y = B -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = y ) <-> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = B ) ) )
41 40 imbi2d 
 |-  ( y = B -> ( ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = y ) ) <-> ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = B ) ) ) )
42 34 38 41 3imtr4d 
 |-  ( y = B -> ( { { y , A } , { y , B } } C_ E -> ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = y ) ) ) )
43 24 pm2.24i 
 |-  ( -. A = A -> A = C )
44 23 43 sylbi 
 |-  ( A =/= A -> A = C )
45 22 44 syl 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { A , A } e. E ) -> A = C )
46 45 expcom 
 |-  ( { A , A } e. E -> ( ( V = { A , B , C } /\ G e. USGraph ) -> A = C ) )
47 46 adantr 
 |-  ( ( { A , A } e. E /\ { A , B } e. E ) -> ( ( V = { A , B , C } /\ G e. USGraph ) -> A = C ) )
48 20 47 sylbir 
 |-  ( { { A , A } , { A , B } } C_ E -> ( ( V = { A , B , C } /\ G e. USGraph ) -> A = C ) )
49 48 com12 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( { { A , A } , { A , B } } C_ E -> A = C ) )
50 49 3ad2ant3 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { { A , A } , { A , B } } C_ E -> A = C ) )
51 50 com12 
 |-  ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = C ) )
52 51 2a1i 
 |-  ( y = C -> ( { { C , A } , { C , B } } C_ E -> ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = C ) ) ) )
53 preq1 
 |-  ( y = C -> { y , A } = { C , A } )
54 preq1 
 |-  ( y = C -> { y , B } = { C , B } )
55 53 54 preq12d 
 |-  ( y = C -> { { y , A } , { y , B } } = { { C , A } , { C , B } } )
56 55 sseq1d 
 |-  ( y = C -> ( { { y , A } , { y , B } } C_ E <-> { { C , A } , { C , B } } C_ E ) )
57 eqeq2 
 |-  ( y = C -> ( A = y <-> A = C ) )
58 57 imbi2d 
 |-  ( y = C -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = y ) <-> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = C ) ) )
59 58 imbi2d 
 |-  ( y = C -> ( ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = y ) ) <-> ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = C ) ) ) )
60 52 56 59 3imtr4d 
 |-  ( y = C -> ( { { y , A } , { y , B } } C_ E -> ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = y ) ) ) )
61 17 42 60 3jaoi 
 |-  ( ( y = A \/ y = B \/ y = C ) -> ( { { y , A } , { y , B } } C_ E -> ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = y ) ) ) )
62 preq1 
 |-  ( x = A -> { x , A } = { A , A } )
63 preq1 
 |-  ( x = A -> { x , B } = { A , B } )
64 62 63 preq12d 
 |-  ( x = A -> { { x , A } , { x , B } } = { { A , A } , { A , B } } )
65 64 sseq1d 
 |-  ( x = A -> ( { { x , A } , { x , B } } C_ E <-> { { A , A } , { A , B } } C_ E ) )
66 eqeq1 
 |-  ( x = A -> ( x = y <-> A = y ) )
67 66 imbi2d 
 |-  ( x = A -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) <-> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = y ) ) )
68 65 67 imbi12d 
 |-  ( x = A -> ( ( { { x , A } , { x , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) <-> ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = y ) ) ) )
69 68 imbi2d 
 |-  ( x = A -> ( ( { { y , A } , { y , B } } C_ E -> ( { { x , A } , { x , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) ) <-> ( { { y , A } , { y , B } } C_ E -> ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A = y ) ) ) ) )
70 61 69 imbitrrid 
 |-  ( x = A -> ( ( y = A \/ y = B \/ y = C ) -> ( { { y , A } , { y , B } } C_ E -> ( { { x , A } , { x , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) ) ) )
71 prex 
 |-  { B , A } e. _V
72 prex 
 |-  { B , B } e. _V
73 71 72 prss 
 |-  ( ( { B , A } e. E /\ { B , B } e. E ) <-> { { B , A } , { B , B } } C_ E )
74 2 usgredgne 
 |-  ( ( G e. USGraph /\ { B , B } e. E ) -> B =/= B )
75 74 adantll 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { B , B } e. E ) -> B =/= B )
76 df-ne 
 |-  ( B =/= B <-> -. B = B )
77 eqid 
 |-  B = B
78 77 pm2.24i 
 |-  ( -. B = B -> B = A )
79 76 78 sylbi 
 |-  ( B =/= B -> B = A )
80 75 79 syl 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { B , B } e. E ) -> B = A )
81 80 expcom 
 |-  ( { B , B } e. E -> ( ( V = { A , B , C } /\ G e. USGraph ) -> B = A ) )
82 81 adantl 
 |-  ( ( { B , A } e. E /\ { B , B } e. E ) -> ( ( V = { A , B , C } /\ G e. USGraph ) -> B = A ) )
83 73 82 sylbir 
 |-  ( { { B , A } , { B , B } } C_ E -> ( ( V = { A , B , C } /\ G e. USGraph ) -> B = A ) )
84 83 com12 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( { { B , A } , { B , B } } C_ E -> B = A ) )
85 84 3ad2ant3 
 |-  ( ( ( 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 , B } } C_ E -> B = A ) )
86 85 com12 
 |-  ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = A ) )
87 86 2a1i 
 |-  ( y = A -> ( { { A , A } , { A , B } } C_ E -> ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = A ) ) ) )
88 eqeq2 
 |-  ( y = A -> ( B = y <-> B = A ) )
89 88 imbi2d 
 |-  ( y = A -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = y ) <-> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = A ) ) )
90 89 imbi2d 
 |-  ( y = A -> ( ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = y ) ) <-> ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = A ) ) ) )
91 87 13 90 3imtr4d 
 |-  ( y = A -> ( { { y , A } , { y , B } } C_ E -> ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = y ) ) ) )
92 eqidd 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = B )
93 92 a1i 
 |-  ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = B ) )
94 93 a1i13 
 |-  ( y = B -> ( { { B , A } , { B , B } } C_ E -> ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = B ) ) ) )
95 eqeq2 
 |-  ( y = B -> ( B = y <-> B = B ) )
96 95 imbi2d 
 |-  ( y = B -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = y ) <-> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = B ) ) )
97 96 imbi2d 
 |-  ( y = B -> ( ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = y ) ) <-> ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = B ) ) ) )
98 94 38 97 3imtr4d 
 |-  ( y = B -> ( { { y , A } , { y , B } } C_ E -> ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = y ) ) ) )
99 77 pm2.24i 
 |-  ( -. B = B -> B = C )
100 76 99 sylbi 
 |-  ( B =/= B -> B = C )
101 75 100 syl 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { B , B } e. E ) -> B = C )
102 101 expcom 
 |-  ( { B , B } e. E -> ( ( V = { A , B , C } /\ G e. USGraph ) -> B = C ) )
103 102 adantl 
 |-  ( ( { B , A } e. E /\ { B , B } e. E ) -> ( ( V = { A , B , C } /\ G e. USGraph ) -> B = C ) )
104 73 103 sylbir 
 |-  ( { { B , A } , { B , B } } C_ E -> ( ( V = { A , B , C } /\ G e. USGraph ) -> B = C ) )
105 104 com12 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( { { B , A } , { B , B } } C_ E -> B = C ) )
106 105 3ad2ant3 
 |-  ( ( ( 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 , B } } C_ E -> B = C ) )
107 106 com12 
 |-  ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = C ) )
108 107 2a1i 
 |-  ( y = C -> ( { { C , A } , { C , B } } C_ E -> ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = C ) ) ) )
109 eqeq2 
 |-  ( y = C -> ( B = y <-> B = C ) )
110 109 imbi2d 
 |-  ( y = C -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = y ) <-> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = C ) ) )
111 110 imbi2d 
 |-  ( y = C -> ( ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = y ) ) <-> ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = C ) ) ) )
112 108 56 111 3imtr4d 
 |-  ( y = C -> ( { { y , A } , { y , B } } C_ E -> ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = y ) ) ) )
113 91 98 112 3jaoi 
 |-  ( ( y = A \/ y = B \/ y = C ) -> ( { { y , A } , { y , B } } C_ E -> ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = y ) ) ) )
114 preq1 
 |-  ( x = B -> { x , A } = { B , A } )
115 preq1 
 |-  ( x = B -> { x , B } = { B , B } )
116 114 115 preq12d 
 |-  ( x = B -> { { x , A } , { x , B } } = { { B , A } , { B , B } } )
117 116 sseq1d 
 |-  ( x = B -> ( { { x , A } , { x , B } } C_ E <-> { { B , A } , { B , B } } C_ E ) )
118 eqeq1 
 |-  ( x = B -> ( x = y <-> B = y ) )
119 118 imbi2d 
 |-  ( x = B -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) <-> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = y ) ) )
120 117 119 imbi12d 
 |-  ( x = B -> ( ( { { x , A } , { x , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) <-> ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = y ) ) ) )
121 120 imbi2d 
 |-  ( x = B -> ( ( { { y , A } , { y , B } } C_ E -> ( { { x , A } , { x , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) ) <-> ( { { y , A } , { y , B } } C_ E -> ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> B = y ) ) ) ) )
122 113 121 imbitrrid 
 |-  ( x = B -> ( ( y = A \/ y = B \/ y = C ) -> ( { { y , A } , { y , B } } C_ E -> ( { { x , A } , { x , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) ) ) )
123 24 pm2.24i 
 |-  ( -. A = A -> C = A )
124 23 123 sylbi 
 |-  ( A =/= A -> C = A )
125 22 124 syl 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { A , A } e. E ) -> C = A )
126 125 expcom 
 |-  ( { A , A } e. E -> ( ( V = { A , B , C } /\ G e. USGraph ) -> C = A ) )
127 126 adantr 
 |-  ( ( { A , A } e. E /\ { A , B } e. E ) -> ( ( V = { A , B , C } /\ G e. USGraph ) -> C = A ) )
128 20 127 sylbir 
 |-  ( { { A , A } , { A , B } } C_ E -> ( ( V = { A , B , C } /\ G e. USGraph ) -> C = A ) )
129 128 com12 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( { { A , A } , { A , B } } C_ E -> C = A ) )
130 129 3ad2ant3 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { { A , A } , { A , B } } C_ E -> C = A ) )
131 130 com12 
 |-  ( { { A , A } , { A , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = A ) )
132 131 a1i13 
 |-  ( y = A -> ( { { A , A } , { A , B } } C_ E -> ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = A ) ) ) )
133 eqeq2 
 |-  ( y = A -> ( C = y <-> C = A ) )
134 133 imbi2d 
 |-  ( y = A -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = y ) <-> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = A ) ) )
135 134 imbi2d 
 |-  ( y = A -> ( ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = y ) ) <-> ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = A ) ) ) )
136 132 13 135 3imtr4d 
 |-  ( y = A -> ( { { y , A } , { y , B } } C_ E -> ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = y ) ) ) )
137 pm2.21 
 |-  ( -. B = B -> ( B = B -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> C = B ) ) )
138 76 137 sylbi 
 |-  ( B =/= B -> ( B = B -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> C = B ) ) )
139 75 77 138 mpisyl 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { B , B } e. E ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> C = B ) )
140 139 expcom 
 |-  ( { B , B } e. E -> ( ( V = { A , B , C } /\ G e. USGraph ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> C = B ) ) )
141 140 adantl 
 |-  ( ( { B , A } e. E /\ { B , B } e. E ) -> ( ( V = { A , B , C } /\ G e. USGraph ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> C = B ) ) )
142 73 141 sylbir 
 |-  ( { { B , A } , { B , B } } C_ E -> ( ( V = { A , B , C } /\ G e. USGraph ) -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> C = B ) ) )
143 142 com13 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( V = { A , B , C } /\ G e. USGraph ) -> ( { { B , A } , { B , B } } C_ E -> C = B ) ) )
144 143 a1d 
 |-  ( ( 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 , B } } C_ E -> C = B ) ) ) )
145 144 3imp 
 |-  ( ( ( 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 , B } } C_ E -> C = B ) )
146 145 com12 
 |-  ( { { B , A } , { B , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = B ) )
147 146 a1i13 
 |-  ( y = B -> ( { { B , A } , { B , B } } C_ E -> ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = B ) ) ) )
148 eqeq2 
 |-  ( y = B -> ( C = y <-> C = B ) )
149 148 imbi2d 
 |-  ( y = B -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = y ) <-> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = B ) ) )
150 149 imbi2d 
 |-  ( y = B -> ( ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = y ) ) <-> ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = B ) ) ) )
151 147 38 150 3imtr4d 
 |-  ( y = B -> ( { { y , A } , { y , B } } C_ E -> ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = y ) ) ) )
152 eqidd 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = C )
153 152 a1i 
 |-  ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = C ) )
154 153 a1i13 
 |-  ( y = C -> ( { { C , A } , { C , B } } C_ E -> ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = C ) ) ) )
155 eqeq2 
 |-  ( y = C -> ( C = y <-> C = C ) )
156 155 imbi2d 
 |-  ( y = C -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = y ) <-> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = C ) ) )
157 156 imbi2d 
 |-  ( y = C -> ( ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = y ) ) <-> ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = C ) ) ) )
158 154 56 157 3imtr4d 
 |-  ( y = C -> ( { { y , A } , { y , B } } C_ E -> ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = y ) ) ) )
159 136 151 158 3jaoi 
 |-  ( ( y = A \/ y = B \/ y = C ) -> ( { { y , A } , { y , B } } C_ E -> ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = y ) ) ) )
160 preq1 
 |-  ( x = C -> { x , A } = { C , A } )
161 preq1 
 |-  ( x = C -> { x , B } = { C , B } )
162 160 161 preq12d 
 |-  ( x = C -> { { x , A } , { x , B } } = { { C , A } , { C , B } } )
163 162 sseq1d 
 |-  ( x = C -> ( { { x , A } , { x , B } } C_ E <-> { { C , A } , { C , B } } C_ E ) )
164 eqeq1 
 |-  ( x = C -> ( x = y <-> C = y ) )
165 164 imbi2d 
 |-  ( x = C -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) <-> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = y ) ) )
166 163 165 imbi12d 
 |-  ( x = C -> ( ( { { x , A } , { x , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) <-> ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = y ) ) ) )
167 166 imbi2d 
 |-  ( x = C -> ( ( { { y , A } , { y , B } } C_ E -> ( { { x , A } , { x , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) ) <-> ( { { y , A } , { y , B } } C_ E -> ( { { C , A } , { C , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> C = y ) ) ) ) )
168 159 167 imbitrrid 
 |-  ( x = C -> ( ( y = A \/ y = B \/ y = C ) -> ( { { y , A } , { y , B } } C_ E -> ( { { x , A } , { x , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) ) ) )
169 70 122 168 3jaoi 
 |-  ( ( x = A \/ x = B \/ x = C ) -> ( ( y = A \/ y = B \/ y = C ) -> ( { { y , A } , { y , B } } C_ E -> ( { { x , A } , { x , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) ) ) )
170 169 com3l 
 |-  ( ( y = A \/ y = B \/ y = C ) -> ( { { y , A } , { y , B } } C_ E -> ( ( x = A \/ x = B \/ x = C ) -> ( { { x , A } , { x , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) ) ) )
171 6 170 sylbi 
 |-  ( y e. { A , B , C } -> ( { { y , A } , { y , B } } C_ E -> ( ( x = A \/ x = B \/ x = C ) -> ( { { x , A } , { x , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) ) ) )
172 171 imp 
 |-  ( ( y e. { A , B , C } /\ { { y , A } , { y , B } } C_ E ) -> ( ( x = A \/ x = B \/ x = C ) -> ( { { x , A } , { x , B } } C_ E -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) ) )
173 172 com3l 
 |-  ( ( x = A \/ x = B \/ x = C ) -> ( { { x , A } , { x , B } } C_ E -> ( ( y e. { A , B , C } /\ { { y , A } , { y , B } } C_ E ) -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) ) )
174 4 173 sylbi 
 |-  ( x e. { A , B , C } -> ( { { x , A } , { x , B } } C_ E -> ( ( y e. { A , B , C } /\ { { y , A } , { y , B } } C_ E ) -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) ) ) )
175 174 imp31 
 |-  ( ( ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) /\ ( y e. { A , B , C } /\ { { y , A } , { y , B } } C_ E ) ) -> ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> x = y ) )
176 175 com12 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( ( ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) /\ ( y e. { A , B , C } /\ { { y , A } , { y , B } } C_ E ) ) -> x = y ) )
177 176 alrimivv 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A. x A. y ( ( ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) /\ ( y e. { A , B , C } /\ { { y , A } , { y , B } } C_ E ) ) -> x = y ) )