MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  constr3trllem2 Structured version   Unicode version

Theorem constr3trllem2 21640
Description: Lemma for constr3trl 21648. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
Hypotheses
Ref Expression
constr3cycl.f  |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. ,  <. 1 ,  ( `' E `  { B ,  C } ) >. ,  <. 2 ,  ( `' E `  { C ,  A } ) >. }
constr3cycl.p  |-  P  =  ( { <. 0 ,  A >. ,  <. 1 ,  B >. }  u.  { <. 2 ,  C >. , 
<. 3 ,  A >. } )
Assertion
Ref Expression
constr3trllem2  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  Fun  `' F
)

Proof of Theorem constr3trllem2
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 constr3cycl.f . . . . . 6  |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. ,  <. 1 ,  ( `' E `  { B ,  C } ) >. ,  <. 2 ,  ( `' E `  { C ,  A } ) >. }
2 constr3cycl.p . . . . . 6  |-  P  =  ( { <. 0 ,  A >. ,  <. 1 ,  B >. }  u.  { <. 2 ,  C >. , 
<. 3 ,  A >. } )
31, 2constr3trllem1 21639 . . . . 5  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  F  e. Word  dom  E )
4 wrdf 11735 . . . . 5  |-  ( F  e. Word  dom  E  ->  F : ( 0..^ (
# `  F )
) --> dom  E )
53, 4syl 16 . . . 4  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  F : ( 0..^ ( # `  F
) ) --> dom  E
)
61, 2constr3lem2 21635 . . . . 5  |-  ( # `  F )  =  3
7 usgraf1o 21384 . . . . . . . . . . . 12  |-  ( V USGrph  E  ->  E : dom  E -1-1-onto-> ran 
E )
8 3cycl3dv 21631 . . . . . . . . . . . . . 14  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
) )
9 usgraedgrnv 21399 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( V USGrph  E  /\  { A ,  B }  e.  ran  E )  ->  ( A  e.  V  /\  B  e.  V ) )
109ex 425 . . . . . . . . . . . . . . . . . . 19  |-  ( V USGrph  E  ->  ( { A ,  B }  e.  ran  E  ->  ( A  e.  V  /\  B  e.  V ) ) )
11 usgraedgrnv 21399 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( V USGrph  E  /\  { C ,  A }  e.  ran  E )  ->  ( C  e.  V  /\  A  e.  V ) )
1211ex 425 . . . . . . . . . . . . . . . . . . 19  |-  ( V USGrph  E  ->  ( { C ,  A }  e.  ran  E  ->  ( C  e.  V  /\  A  e.  V ) ) )
1310, 12anim12d 548 . . . . . . . . . . . . . . . . . 18  |-  ( V USGrph  E  ->  ( ( { A ,  B }  e.  ran  E  /\  { C ,  A }  e.  ran  E )  -> 
( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V )
) ) )
1413com12 30 . . . . . . . . . . . . . . . . 17  |-  ( ( { A ,  B }  e.  ran  E  /\  { C ,  A }  e.  ran  E )  -> 
( V USGrph  E  ->  ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) ) ) )
15143adant2 977 . . . . . . . . . . . . . . . 16  |-  ( ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E )  -> 
( V USGrph  E  ->  ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) ) ) )
1615impcom 421 . . . . . . . . . . . . . . 15  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V )
) )
171, 2constr3lem5 21637 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )
1817jctl 527 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( (
( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) )
1918exp31 589 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V )
)  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  ( E : dom  E -1-1-onto-> ran  E  ->  (
( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) ) ) )
2016, 19mpancom 652 . . . . . . . . . . . . . 14  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A )  ->  ( E : dom  E -1-1-onto-> ran  E  ->  ( ( ( F `
 0 )  =  ( `' E `  { A ,  B }
)  /\  ( F `  1 )  =  ( `' E `  { B ,  C }
)  /\  ( F `  2 )  =  ( `' E `  { C ,  A }
) )  /\  (
( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) ) ) )
218, 20mpd 15 . . . . . . . . . . . . 13  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  ( E : dom  E -1-1-onto-> ran  E  ->  (
( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) ) )
2221ex 425 . . . . . . . . . . . 12  |-  ( V USGrph  E  ->  ( ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E )  -> 
( E : dom  E -1-1-onto-> ran 
E  ->  ( (
( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) ) ) )
237, 22mpid 40 . . . . . . . . . . 11  |-  ( V USGrph  E  ->  ( ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E )  -> 
( ( ( F `
 0 )  =  ( `' E `  { A ,  B }
)  /\  ( F `  1 )  =  ( `' E `  { B ,  C }
)  /\  ( F `  2 )  =  ( `' E `  { C ,  A }
) )  /\  (
( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) ) )
2423imp 420 . . . . . . . . . 10  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  ( ( ( F `  0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) )
2524adantl 454 . . . . . . . . 9  |-  ( ( ( # `  F
)  =  3  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  ->  ( (
( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) )
26 c0ex 9087 . . . . . . . . . . 11  |-  0  e.  _V
27 1ex 9088 . . . . . . . . . . 11  |-  1  e.  _V
28 2z 10314 . . . . . . . . . . 11  |-  2  e.  ZZ
2926, 27, 283pm3.2i 1133 . . . . . . . . . 10  |-  ( 0  e.  _V  /\  1  e.  _V  /\  2  e.  ZZ )
30 eqidd 2439 . . . . . . . . . . . . . . 15  |-  ( ( F `  0 )  =  ( F ` 
0 )  ->  0  =  0 )
3130a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( F `  0
)  =  ( F `
 0 )  -> 
0  =  0 ) )
32 f1of1 5675 . . . . . . . . . . . . . . . . . . 19  |-  ( E : dom  E -1-1-onto-> ran  E  ->  E : dom  E -1-1-> ran 
E )
3332adantl 454 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  E : dom  E -1-1-> ran  E )
34 3simpa 955 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E )  -> 
( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E ) )
3534adantl 454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E ) )
3635ad3antlr 713 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E ) )
37 f1ocnvfvrneq 6021 . . . . . . . . . . . . . . . . . 18  |-  ( ( E : dom  E -1-1-> ran 
E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E ) )  ->  ( ( `' E `  { A ,  B } )  =  ( `' E `  { B ,  C }
)  ->  { A ,  B }  =  { B ,  C }
) )
3833, 36, 37syl2anc 644 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( ( `' E `  { A ,  B } )  =  ( `' E `  { B ,  C }
)  ->  { A ,  B }  =  { B ,  C }
) )
39 simpl 445 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( A  e.  V  /\  B  e.  V
) )
40 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  V  /\  B  e.  V )  ->  B  e.  V )
41 simpl 445 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( C  e.  V  /\  A  e.  V )  ->  C  e.  V )
4240, 41anim12i 551 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( B  e.  V  /\  C  e.  V
) )
43 preq12bg 3979 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( B  e.  V  /\  C  e.  V ) )  -> 
( { A ,  B }  =  { B ,  C }  <->  ( ( A  =  B  /\  B  =  C )  \/  ( A  =  C  /\  B  =  B ) ) ) )
4439, 42, 43syl2anc 644 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( { A ,  B }  =  { B ,  C }  <->  ( ( A  =  B  /\  B  =  C )  \/  ( A  =  C  /\  B  =  B ) ) ) )
45 df-ne 2603 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  =/=  B  <->  -.  A  =  B )
46 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  A  =  B  -> 
( A  =  B  ->  0  =  1 ) )
4745, 46sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( A  =/=  B  ->  ( A  =  B  ->  0  =  1 ) )
48473ad2ant1 979 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A )  ->  ( A  =  B  ->  0  =  1 ) )
4948com12 30 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A  =  B  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
1 ) )
5049adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  =  B  /\  B  =  C )  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
1 ) )
51 df-ne 2603 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( C  =/=  A  <->  -.  C  =  A )
52 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( -.  C  =  A  -> 
( C  =  A  ->  0  =  1 ) )
5351, 52sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( C  =/=  A  ->  ( C  =  A  ->  0  =  1 ) )
54533ad2ant3 981 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A )  ->  ( C  =  A  ->  0  =  1 ) )
5554com12 30 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( C  =  A  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
1 ) )
5655eqcoms 2441 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A  =  C  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
1 ) )
5756adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  =  C  /\  B  =  B )  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
1 ) )
5850, 57jaoi 370 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  =  B  /\  B  =  C )  \/  ( A  =  C  /\  B  =  B ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
1 ) )
5944, 58syl6bi 221 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( { A ,  B }  =  { B ,  C }  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
1 ) ) )
6059com23 75 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  ( { A ,  B }  =  { B ,  C }  ->  0  =  1 ) ) )
6160adantr 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V )
)  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  ( { A ,  B }  =  { B ,  C }  ->  0  =  1 ) ) )
6261imp 420 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V )
)  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
) )  ->  ( { A ,  B }  =  { B ,  C }  ->  0  =  1 ) )
6362adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( { A ,  B }  =  { B ,  C }  ->  0  =  1 ) )
6438, 63syld 43 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( ( `' E `  { A ,  B } )  =  ( `' E `  { B ,  C }
)  ->  0  = 
1 ) )
6564adantl 454 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( `' E `  { A ,  B }
)  =  ( `' E `  { B ,  C } )  -> 
0  =  1 ) )
66 eqeq12 2450 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } ) )  -> 
( ( F ` 
0 )  =  ( F `  1 )  <-> 
( `' E `  { A ,  B }
)  =  ( `' E `  { B ,  C } ) ) )
67663adant3 978 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  -> 
( ( F ` 
0 )  =  ( F `  1 )  <-> 
( `' E `  { A ,  B }
)  =  ( `' E `  { B ,  C } ) ) )
6867imbi1d 310 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  -> 
( ( ( F `
 0 )  =  ( F `  1
)  ->  0  = 
1 )  <->  ( ( `' E `  { A ,  B } )  =  ( `' E `  { B ,  C }
)  ->  0  = 
1 ) ) )
6968adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( ( F ` 
0 )  =  ( F `  1 )  ->  0  =  1 )  <->  ( ( `' E `  { A ,  B } )  =  ( `' E `  { B ,  C }
)  ->  0  = 
1 ) ) )
7065, 69mpbird 225 . . . . . . . . . . . . . 14  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( F `  0
)  =  ( F `
 1 )  -> 
0  =  1 ) )
71 3simpb 956 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E )  -> 
( { A ,  B }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )
7271adantl 454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  ( { A ,  B }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )
7372ad3antlr 713 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( { A ,  B }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )
74 f1ocnvfvrneq 6021 . . . . . . . . . . . . . . . . . 18  |-  ( ( E : dom  E -1-1-> ran 
E  /\  ( { A ,  B }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  ( ( `' E `  { A ,  B } )  =  ( `' E `  { C ,  A }
)  ->  { A ,  B }  =  { C ,  A }
) )
7533, 73, 74syl2anc 644 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( ( `' E `  { A ,  B } )  =  ( `' E `  { C ,  A }
)  ->  { A ,  B }  =  { C ,  A }
) )
76 preq12bg 3979 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( { A ,  B }  =  { C ,  A }  <->  ( ( A  =  C  /\  B  =  A )  \/  ( A  =  A  /\  B  =  C ) ) ) )
77 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( -.  A  =  B  -> 
( A  =  B  ->  0  =  2 ) )
7845, 77sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  =/=  B  ->  ( A  =  B  ->  0  =  2 ) )
79783ad2ant1 979 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A )  ->  ( A  =  B  ->  0  =  2 ) )
8079com12 30 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  =  B  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
2 ) )
8180eqcoms 2441 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( B  =  A  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
2 ) )
8281adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  =  C  /\  B  =  A )  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
2 ) )
83 df-ne 2603 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( B  =/=  C  <->  -.  B  =  C )
84 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  B  =  C  -> 
( B  =  C  ->  0  =  2 ) )
8583, 84sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( B  =/=  C  ->  ( B  =  C  ->  0  =  2 ) )
86853ad2ant2 980 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A )  ->  ( B  =  C  ->  0  =  2 ) )
8786com12 30 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( B  =  C  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
2 ) )
8887adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  =  A  /\  B  =  C )  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
2 ) )
8982, 88jaoi 370 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  =  C  /\  B  =  A )  \/  ( A  =  A  /\  B  =  C ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
2 ) )
9076, 89syl6bi 221 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( { A ,  B }  =  { C ,  A }  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  0  = 
2 ) ) )
9190com23 75 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  ( { A ,  B }  =  { C ,  A }  ->  0  =  2 ) ) )
9291adantr 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V )
)  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  ( { A ,  B }  =  { C ,  A }  ->  0  =  2 ) ) )
9392imp 420 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V )
)  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
) )  ->  ( { A ,  B }  =  { C ,  A }  ->  0  =  2 ) )
9493adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( { A ,  B }  =  { C ,  A }  ->  0  =  2 ) )
9575, 94syld 43 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( ( `' E `  { A ,  B } )  =  ( `' E `  { C ,  A }
)  ->  0  = 
2 ) )
9695adantl 454 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( `' E `  { A ,  B }
)  =  ( `' E `  { C ,  A } )  -> 
0  =  2 ) )
97 eqeq12 2450 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  -> 
( ( F ` 
0 )  =  ( F `  2 )  <-> 
( `' E `  { A ,  B }
)  =  ( `' E `  { C ,  A } ) ) )
98973adant2 977 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  -> 
( ( F ` 
0 )  =  ( F `  2 )  <-> 
( `' E `  { A ,  B }
)  =  ( `' E `  { C ,  A } ) ) )
9998imbi1d 310 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  -> 
( ( ( F `
 0 )  =  ( F `  2
)  ->  0  = 
2 )  <->  ( ( `' E `  { A ,  B } )  =  ( `' E `  { C ,  A }
)  ->  0  = 
2 ) ) )
10099adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( ( F ` 
0 )  =  ( F `  2 )  ->  0  =  2 )  <->  ( ( `' E `  { A ,  B } )  =  ( `' E `  { C ,  A }
)  ->  0  = 
2 ) ) )
10196, 100mpbird 225 . . . . . . . . . . . . . 14  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( F `  0
)  =  ( F `
 2 )  -> 
0  =  2 ) )
10231, 70, 1013jca 1135 . . . . . . . . . . . . 13  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( ( F ` 
0 )  =  ( F `  0 )  ->  0  =  0 )  /\  ( ( F `  0 )  =  ( F ` 
1 )  ->  0  =  1 )  /\  ( ( F ` 
0 )  =  ( F `  2 )  ->  0  =  2 ) ) )
103102adantl 454 . . . . . . . . . . . 12  |-  ( ( ( 0  e.  _V  /\  1  e.  _V  /\  2  e.  ZZ )  /\  ( ( ( F `
 0 )  =  ( `' E `  { A ,  B }
)  /\  ( F `  1 )  =  ( `' E `  { B ,  C }
)  /\  ( F `  2 )  =  ( `' E `  { C ,  A }
) )  /\  (
( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) )  -> 
( ( ( F `
 0 )  =  ( F `  0
)  ->  0  = 
0 )  /\  (
( F `  0
)  =  ( F `
 1 )  -> 
0  =  1 )  /\  ( ( F `
 0 )  =  ( F `  2
)  ->  0  = 
2 ) ) )
104 fveq2 5730 . . . . . . . . . . . . . . . 16  |-  ( y  =  0  ->  ( F `  y )  =  ( F ` 
0 ) )
105104eqeq2d 2449 . . . . . . . . . . . . . . 15  |-  ( y  =  0  ->  (
( F `  0
)  =  ( F `
 y )  <->  ( F `  0 )  =  ( F `  0
) ) )
106 eqeq2 2447 . . . . . . . . . . . . . . 15  |-  ( y  =  0  ->  (
0  =  y  <->  0  = 
0 ) )
107105, 106imbi12d 313 . . . . . . . . . . . . . 14  |-  ( y  =  0  ->  (
( ( F ` 
0 )  =  ( F `  y )  ->  0  =  y )  <->  ( ( F `
 0 )  =  ( F `  0
)  ->  0  = 
0 ) ) )
108 fveq2 5730 . . . . . . . . . . . . . . . 16  |-  ( y  =  1  ->  ( F `  y )  =  ( F ` 
1 ) )
109108eqeq2d 2449 . . . . . . . . . . . . . . 15  |-  ( y  =  1  ->  (
( F `  0
)  =  ( F `
 y )  <->  ( F `  0 )  =  ( F `  1
) ) )
110 eqeq2 2447 . . . . . . . . . . . . . . 15  |-  ( y  =  1  ->  (
0  =  y  <->  0  = 
1 ) )
111109, 110imbi12d 313 . . . . . . . . . . . . . 14  |-  ( y  =  1  ->  (
( ( F ` 
0 )  =  ( F `  y )  ->  0  =  y )  <->  ( ( F `
 0 )  =  ( F `  1
)  ->  0  = 
1 ) ) )
112 fveq2 5730 . . . . . . . . . . . . . . . 16  |-  ( y  =  2  ->  ( F `  y )  =  ( F ` 
2 ) )
113112eqeq2d 2449 . . . . . . . . . . . . . . 15  |-  ( y  =  2  ->  (
( F `  0
)  =  ( F `
 y )  <->  ( F `  0 )  =  ( F `  2
) ) )
114 eqeq2 2447 . . . . . . . . . . . . . . 15  |-  ( y  =  2  ->  (
0  =  y  <->  0  = 
2 ) )
115113, 114imbi12d 313 . . . . . . . . . . . . . 14  |-  ( y  =  2  ->  (
( ( F ` 
0 )  =  ( F `  y )  ->  0  =  y )  <->  ( ( F `
 0 )  =  ( F `  2
)  ->  0  = 
2 ) ) )
116107, 111, 115raltpg 3861 . . . . . . . . . . . . 13  |-  ( ( 0  e.  _V  /\  1  e.  _V  /\  2  e.  ZZ )  ->  ( A. y  e.  { 0 ,  1 ,  2 }  ( ( F `
 0 )  =  ( F `  y
)  ->  0  =  y )  <->  ( (
( F `  0
)  =  ( F `
 0 )  -> 
0  =  0 )  /\  ( ( F `
 0 )  =  ( F `  1
)  ->  0  = 
1 )  /\  (
( F `  0
)  =  ( F `
 2 )  -> 
0  =  2 ) ) ) )
117116adantr 453 . . . . . . . . . . . 12  |-  ( ( ( 0  e.  _V  /\  1  e.  _V  /\  2  e.  ZZ )  /\  ( ( ( F `
 0 )  =  ( `' E `  { A ,  B }
)  /\  ( F `  1 )  =  ( `' E `  { B ,  C }
)  /\  ( F `  2 )  =  ( `' E `  { C ,  A }
) )  /\  (
( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) )  -> 
( A. y  e. 
{ 0 ,  1 ,  2 }  (
( F `  0
)  =  ( F `
 y )  -> 
0  =  y )  <-> 
( ( ( F `
 0 )  =  ( F `  0
)  ->  0  = 
0 )  /\  (
( F `  0
)  =  ( F `
 1 )  -> 
0  =  1 )  /\  ( ( F `
 0 )  =  ( F `  2
)  ->  0  = 
2 ) ) ) )
118103, 117mpbird 225 . . . . . . . . . . 11  |-  ( ( ( 0  e.  _V  /\  1  e.  _V  /\  2  e.  ZZ )  /\  ( ( ( F `
 0 )  =  ( `' E `  { A ,  B }
)  /\  ( F `  1 )  =  ( `' E `  { B ,  C }
)  /\  ( F `  2 )  =  ( `' E `  { C ,  A }
) )  /\  (
( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) )  ->  A. y  e.  { 0 ,  1 ,  2 }  ( ( F `
 0 )  =  ( F `  y
)  ->  0  =  y ) )
119 pm3.22 438 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E )  -> 
( { B ,  C }  e.  ran  E  /\  { A ,  B }  e.  ran  E ) )
1201193adant3 978 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E )  -> 
( { B ,  C }  e.  ran  E  /\  { A ,  B }  e.  ran  E ) )
121120adantl 454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  ( { B ,  C }  e.  ran  E  /\  { A ,  B }  e.  ran  E ) )
122121ad3antlr 713 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( { B ,  C }  e.  ran  E  /\  { A ,  B }  e.  ran  E ) )
123 f1ocnvfvrneq 6021 . . . . . . . . . . . . . . . . . 18  |-  ( ( E : dom  E -1-1-> ran 
E  /\  ( { B ,  C }  e.  ran  E  /\  { A ,  B }  e.  ran  E ) )  ->  ( ( `' E `  { B ,  C } )  =  ( `' E `  { A ,  B }
)  ->  { B ,  C }  =  { A ,  B }
) )
12433, 122, 123syl2anc 644 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( ( `' E `  { B ,  C } )  =  ( `' E `  { A ,  B }
)  ->  { B ,  C }  =  { A ,  B }
) )
125 preq12bg 3979 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( B  e.  V  /\  C  e.  V
)  /\  ( A  e.  V  /\  B  e.  V ) )  -> 
( { B ,  C }  =  { A ,  B }  <->  ( ( B  =  A  /\  C  =  B )  \/  ( B  =  B  /\  C  =  A ) ) ) )
12642, 39, 125syl2anc 644 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( { B ,  C }  =  { A ,  B }  <->  ( ( B  =  A  /\  C  =  B )  \/  ( B  =  B  /\  C  =  A ) ) ) )
127 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( -.  A  =  B  -> 
( A  =  B  ->  1  =  0 ) )
12845, 127sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  =/=  B  ->  ( A  =  B  ->  1  =  0 ) )
1291283ad2ant1 979 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A )  ->  ( A  =  B  ->  1  =  0 ) )
130129com12 30 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  =  B  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
0 ) )
131130eqcoms 2441 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( B  =  A  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
0 ) )
132131adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( B  =  A  /\  C  =  B )  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
0 ) )
133 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  C  =  A  -> 
( C  =  A  ->  1  =  0 ) )
13451, 133sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( C  =/=  A  ->  ( C  =  A  ->  1  =  0 ) )
1351343ad2ant3 981 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A )  ->  ( C  =  A  ->  1  =  0 ) )
136135com12 30 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( C  =  A  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
0 ) )
137136adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( B  =  B  /\  C  =  A )  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
0 ) )
138132, 137jaoi 370 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( B  =  A  /\  C  =  B )  \/  ( B  =  B  /\  C  =  A ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
0 ) )
139126, 138syl6bi 221 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( { B ,  C }  =  { A ,  B }  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
0 ) ) )
140139com23 75 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  ( { B ,  C }  =  { A ,  B }  ->  1  =  0 ) ) )
141140adantr 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V )
)  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  ( { B ,  C }  =  { A ,  B }  ->  1  =  0 ) ) )
142141imp 420 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V )
)  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
) )  ->  ( { B ,  C }  =  { A ,  B }  ->  1  =  0 ) )
143142adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( { B ,  C }  =  { A ,  B }  ->  1  =  0 ) )
144124, 143syld 43 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( ( `' E `  { B ,  C } )  =  ( `' E `  { A ,  B }
)  ->  1  = 
0 ) )
145144adantl 454 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( `' E `  { B ,  C }
)  =  ( `' E `  { A ,  B } )  -> 
1  =  0 ) )
146 eqeq12 2450 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( F `  1
)  =  ( `' E `  { B ,  C } )  /\  ( F `  0 )  =  ( `' E `  { A ,  B } ) )  -> 
( ( F ` 
1 )  =  ( F `  0 )  <-> 
( `' E `  { B ,  C }
)  =  ( `' E `  { A ,  B } ) ) )
147146ancoms 441 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } ) )  -> 
( ( F ` 
1 )  =  ( F `  0 )  <-> 
( `' E `  { B ,  C }
)  =  ( `' E `  { A ,  B } ) ) )
1481473adant3 978 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  -> 
( ( F ` 
1 )  =  ( F `  0 )  <-> 
( `' E `  { B ,  C }
)  =  ( `' E `  { A ,  B } ) ) )
149148imbi1d 310 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  -> 
( ( ( F `
 1 )  =  ( F `  0
)  ->  1  = 
0 )  <->  ( ( `' E `  { B ,  C } )  =  ( `' E `  { A ,  B }
)  ->  1  = 
0 ) ) )
150149adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( ( F ` 
1 )  =  ( F `  0 )  ->  1  =  0 )  <->  ( ( `' E `  { B ,  C } )  =  ( `' E `  { A ,  B }
)  ->  1  = 
0 ) ) )
151145, 150mpbird 225 . . . . . . . . . . . . . 14  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( F `  1
)  =  ( F `
 0 )  -> 
1  =  0 ) )
152 eqidd 2439 . . . . . . . . . . . . . . 15  |-  ( ( F `  1 )  =  ( F ` 
1 )  ->  1  =  1 )
153152a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( F `  1
)  =  ( F `
 1 )  -> 
1  =  1 ) )
154 3simpc 957 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E )  -> 
( { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )
155154adantl 454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  ( { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )
156155ad3antlr 713 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )
157 f1ocnvfvrneq 6021 . . . . . . . . . . . . . . . . . 18  |-  ( ( E : dom  E -1-1-> ran 
E  /\  ( { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  ( ( `' E `  { B ,  C } )  =  ( `' E `  { C ,  A }
)  ->  { B ,  C }  =  { C ,  A }
) )
15833, 156, 157syl2anc 644 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( ( `' E `  { B ,  C } )  =  ( `' E `  { C ,  A }
)  ->  { B ,  C }  =  { C ,  A }
) )
159 preq12bg 3979 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( B  e.  V  /\  C  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( { B ,  C }  =  { C ,  A }  <->  ( ( B  =  C  /\  C  =  A )  \/  ( B  =  A  /\  C  =  C ) ) ) )
16042, 159sylancom 650 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( { B ,  C }  =  { C ,  A }  <->  ( ( B  =  C  /\  C  =  A )  \/  ( B  =  A  /\  C  =  C ) ) ) )
161 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  B  =  C  -> 
( B  =  C  ->  1  =  2 ) )
16283, 161sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( B  =/=  C  ->  ( B  =  C  ->  1  =  2 ) )
1631623ad2ant2 980 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A )  ->  ( B  =  C  ->  1  =  2 ) )
164163com12 30 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( B  =  C  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
2 ) )
165164adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( B  =  C  /\  C  =  A )  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
2 ) )
166 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( -.  A  =  B  -> 
( A  =  B  ->  1  =  2 ) )
16745, 166sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  =/=  B  ->  ( A  =  B  ->  1  =  2 ) )
1681673ad2ant1 979 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A )  ->  ( A  =  B  ->  1  =  2 ) )
169168com12 30 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  =  B  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
2 ) )
170169eqcoms 2441 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( B  =  A  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
2 ) )
171170adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( B  =  A  /\  C  =  C )  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
2 ) )
172165, 171jaoi 370 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( B  =  C  /\  C  =  A )  \/  ( B  =  A  /\  C  =  C ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
2 ) )
173160, 172syl6bi 221 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( { B ,  C }  =  { C ,  A }  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  1  = 
2 ) ) )
174173com23 75 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  ( { B ,  C }  =  { C ,  A }  ->  1  =  2 ) ) )
175174adantr 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V )
)  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  ( { B ,  C }  =  { C ,  A }  ->  1  =  2 ) ) )
176175imp 420 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V )
)  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
) )  ->  ( { B ,  C }  =  { C ,  A }  ->  1  =  2 ) )
177176adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( { B ,  C }  =  { C ,  A }  ->  1  =  2 ) )
178158, 177syld 43 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( ( `' E `  { B ,  C } )  =  ( `' E `  { C ,  A }
)  ->  1  = 
2 ) )
179178adantl 454 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( `' E `  { B ,  C }
)  =  ( `' E `  { C ,  A } )  -> 
1  =  2 ) )
180 eqeq12 2450 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  1
)  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  -> 
( ( F ` 
1 )  =  ( F `  2 )  <-> 
( `' E `  { B ,  C }
)  =  ( `' E `  { C ,  A } ) ) )
1811803adant1 976 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  -> 
( ( F ` 
1 )  =  ( F `  2 )  <-> 
( `' E `  { B ,  C }
)  =  ( `' E `  { C ,  A } ) ) )
182181imbi1d 310 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  -> 
( ( ( F `
 1 )  =  ( F `  2
)  ->  1  = 
2 )  <->  ( ( `' E `  { B ,  C } )  =  ( `' E `  { C ,  A }
)  ->  1  = 
2 ) ) )
183182adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( ( F ` 
1 )  =  ( F `  2 )  ->  1  =  2 )  <->  ( ( `' E `  { B ,  C } )  =  ( `' E `  { C ,  A }
)  ->  1  = 
2 ) ) )
184179, 183mpbird 225 . . . . . . . . . . . . . 14  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( F `  1
)  =  ( F `
 2 )  -> 
1  =  2 ) )
185151, 153, 1843jca 1135 . . . . . . . . . . . . 13  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( ( F ` 
1 )  =  ( F `  0 )  ->  1  =  0 )  /\  ( ( F `  1 )  =  ( F ` 
1 )  ->  1  =  1 )  /\  ( ( F ` 
1 )  =  ( F `  2 )  ->  1  =  2 ) ) )
186185adantl 454 . . . . . . . . . . . 12  |-  ( ( ( 0  e.  _V  /\  1  e.  _V  /\  2  e.  ZZ )  /\  ( ( ( F `
 0 )  =  ( `' E `  { A ,  B }
)  /\  ( F `  1 )  =  ( `' E `  { B ,  C }
)  /\  ( F `  2 )  =  ( `' E `  { C ,  A }
) )  /\  (
( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) )  -> 
( ( ( F `
 1 )  =  ( F `  0
)  ->  1  = 
0 )  /\  (
( F `  1
)  =  ( F `
 1 )  -> 
1  =  1 )  /\  ( ( F `
 1 )  =  ( F `  2
)  ->  1  = 
2 ) ) )
187104eqeq2d 2449 . . . . . . . . . . . . . . 15  |-  ( y  =  0  ->  (
( F `  1
)  =  ( F `
 y )  <->  ( F `  1 )  =  ( F `  0
) ) )
188 eqeq2 2447 . . . . . . . . . . . . . . 15  |-  ( y  =  0  ->  (
1  =  y  <->  1  = 
0 ) )
189187, 188imbi12d 313 . . . . . . . . . . . . . 14  |-  ( y  =  0  ->  (
( ( F ` 
1 )  =  ( F `  y )  ->  1  =  y )  <->  ( ( F `
 1 )  =  ( F `  0
)  ->  1  = 
0 ) ) )
190108eqeq2d 2449 . . . . . . . . . . . . . . 15  |-  ( y  =  1  ->  (
( F `  1
)  =  ( F `
 y )  <->  ( F `  1 )  =  ( F `  1
) ) )
191 eqeq2 2447 . . . . . . . . . . . . . . 15  |-  ( y  =  1  ->  (
1  =  y  <->  1  = 
1 ) )
192190, 191imbi12d 313 . . . . . . . . . . . . . 14  |-  ( y  =  1  ->  (
( ( F ` 
1 )  =  ( F `  y )  ->  1  =  y )  <->  ( ( F `
 1 )  =  ( F `  1
)  ->  1  = 
1 ) ) )
193112eqeq2d 2449 . . . . . . . . . . . . . . 15  |-  ( y  =  2  ->  (
( F `  1
)  =  ( F `
 y )  <->  ( F `  1 )  =  ( F `  2
) ) )
194 eqeq2 2447 . . . . . . . . . . . . . . 15  |-  ( y  =  2  ->  (
1  =  y  <->  1  = 
2 ) )
195193, 194imbi12d 313 . . . . . . . . . . . . . 14  |-  ( y  =  2  ->  (
( ( F ` 
1 )  =  ( F `  y )  ->  1  =  y )  <->  ( ( F `
 1 )  =  ( F `  2
)  ->  1  = 
2 ) ) )
196189, 192, 195raltpg 3861 . . . . . . . . . . . . 13  |-  ( ( 0  e.  _V  /\  1  e.  _V  /\  2  e.  ZZ )  ->  ( A. y  e.  { 0 ,  1 ,  2 }  ( ( F `
 1 )  =  ( F `  y
)  ->  1  =  y )  <->  ( (
( F `  1
)  =  ( F `
 0 )  -> 
1  =  0 )  /\  ( ( F `
 1 )  =  ( F `  1
)  ->  1  = 
1 )  /\  (
( F `  1
)  =  ( F `
 2 )  -> 
1  =  2 ) ) ) )
197196adantr 453 . . . . . . . . . . . 12  |-  ( ( ( 0  e.  _V  /\  1  e.  _V  /\  2  e.  ZZ )  /\  ( ( ( F `
 0 )  =  ( `' E `  { A ,  B }
)  /\  ( F `  1 )  =  ( `' E `  { B ,  C }
)  /\  ( F `  2 )  =  ( `' E `  { C ,  A }
) )  /\  (
( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) )  -> 
( A. y  e. 
{ 0 ,  1 ,  2 }  (
( F `  1
)  =  ( F `
 y )  -> 
1  =  y )  <-> 
( ( ( F `
 1 )  =  ( F `  0
)  ->  1  = 
0 )  /\  (
( F `  1
)  =  ( F `
 1 )  -> 
1  =  1 )  /\  ( ( F `
 1 )  =  ( F `  2
)  ->  1  = 
2 ) ) ) )
198186, 197mpbird 225 . . . . . . . . . . 11  |-  ( ( ( 0  e.  _V  /\  1  e.  _V  /\  2  e.  ZZ )  /\  ( ( ( F `
 0 )  =  ( `' E `  { A ,  B }
)  /\  ( F `  1 )  =  ( `' E `  { B ,  C }
)  /\  ( F `  2 )  =  ( `' E `  { C ,  A }
) )  /\  (
( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) ) )  ->  A. y  e.  { 0 ,  1 ,  2 }  ( ( F `
 1 )  =  ( F `  y
)  ->  1  =  y ) )
199 pm3.22 438 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( { A ,  B }  e.  ran  E  /\  { C ,  A }  e.  ran  E )  -> 
( { C ,  A }  e.  ran  E  /\  { A ,  B }  e.  ran  E ) )
2001993adant2 977 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E )  -> 
( { C ,  A }  e.  ran  E  /\  { A ,  B }  e.  ran  E ) )
201200adantl 454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  ( { C ,  A }  e.  ran  E  /\  { A ,  B }  e.  ran  E ) )
202201ad3antlr 713 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( { C ,  A }  e.  ran  E  /\  { A ,  B }  e.  ran  E ) )
203 f1ocnvfvrneq 6021 . . . . . . . . . . . . . . . . . 18  |-  ( ( E : dom  E -1-1-> ran 
E  /\  ( { C ,  A }  e.  ran  E  /\  { A ,  B }  e.  ran  E ) )  ->  ( ( `' E `  { C ,  A } )  =  ( `' E `  { A ,  B }
)  ->  { C ,  A }  =  { A ,  B }
) )
20433, 202, 203syl2anc 644 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( ( `' E `  { C ,  A } )  =  ( `' E `  { A ,  B }
)  ->  { C ,  A }  =  { A ,  B }
) )
205 preq12bg 3979 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( C  e.  V  /\  A  e.  V
)  /\  ( A  e.  V  /\  B  e.  V ) )  -> 
( { C ,  A }  =  { A ,  B }  <->  ( ( C  =  A  /\  A  =  B )  \/  ( C  =  B  /\  A  =  A ) ) ) )
206205ancoms 441 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( { C ,  A }  =  { A ,  B }  <->  ( ( C  =  A  /\  A  =  B )  \/  ( C  =  B  /\  A  =  A ) ) ) )
207 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  A  =  B  -> 
( A  =  B  ->  2  =  0 ) )
20845, 207sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( A  =/=  B  ->  ( A  =  B  ->  2  =  0 ) )
2092083ad2ant1 979 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A )  ->  ( A  =  B  ->  2  =  0 ) )
210209com12 30 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A  =  B  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  2  = 
0 ) )
211210adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( C  =  A  /\  A  =  B )  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  2  = 
0 ) )
212 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( -.  B  =  C  -> 
( B  =  C  ->  2  =  0 ) )
21383, 212sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( B  =/=  C  ->  ( B  =  C  ->  2  =  0 ) )
2142133ad2ant2 980 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A )  ->  ( B  =  C  ->  2  =  0 ) )
215214com12 30 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( B  =  C  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  2  = 
0 ) )
216215eqcoms 2441 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( C  =  B  ->  (
( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
)  ->  2  = 
0 ) )
217216adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( C  =  B  /\  A  =  A )  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  2  = 
0 ) )
218211, 217jaoi 370 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( C  =  A  /\  A  =  B )  \/  ( C  =  B  /\  A  =  A ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  2  = 
0 ) )
219206, 218syl6bi 221 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( { C ,  A }  =  { A ,  B }  ->  ( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  2  = 
0 ) ) )
220219com23 75 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  ( { C ,  A }  =  { A ,  B }  ->  2  =  0 ) ) )
221220adantr 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V )
)  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  -> 
( ( A  =/= 
B  /\  B  =/=  C  /\  C  =/=  A
)  ->  ( { C ,  A }  =  { A ,  B }  ->  2  =  0 ) ) )
222221imp 420 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V )
)  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A
) )  ->  ( { C ,  A }  =  { A ,  B }  ->  2  =  0 ) )
223222adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( { C ,  A }  =  { A ,  B }  ->  2  =  0 ) )
224204, 223syld 43 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( ( `' E `  { C ,  A } )  =  ( `' E `  { A ,  B }
)  ->  2  = 
0 ) )
225224adantl 454 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( `' E `  { C ,  A }
)  =  ( `' E `  { A ,  B } )  -> 
2  =  0 ) )
226 eqeq12 2450 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( F `  2
)  =  ( `' E `  { C ,  A } )  /\  ( F `  0 )  =  ( `' E `  { A ,  B } ) )  -> 
( ( F ` 
2 )  =  ( F `  0 )  <-> 
( `' E `  { C ,  A }
)  =  ( `' E `  { A ,  B } ) ) )
227226ancoms 441 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  -> 
( ( F ` 
2 )  =  ( F `  0 )  <-> 
( `' E `  { C ,  A }
)  =  ( `' E `  { A ,  B } ) ) )
2282273adant2 977 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  -> 
( ( F ` 
2 )  =  ( F `  0 )  <-> 
( `' E `  { C ,  A }
)  =  ( `' E `  { A ,  B } ) ) )
229228imbi1d 310 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  0
)  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  -> 
( ( ( F `
 2 )  =  ( F `  0
)  ->  2  = 
0 )  <->  ( ( `' E `  { C ,  A } )  =  ( `' E `  { A ,  B }
)  ->  2  = 
0 ) ) )
230229adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( ( F ` 
2 )  =  ( F `  0 )  ->  2  =  0 )  <->  ( ( `' E `  { C ,  A } )  =  ( `' E `  { A ,  B }
)  ->  2  = 
0 ) ) )
231225, 230mpbird 225 . . . . . . . . . . . . . 14  |-  ( ( ( ( F ` 
0 )  =  ( `' E `  { A ,  B } )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E `  { C ,  A } ) )  /\  ( ( ( ( ( A  e.  V  /\  B  e.  V
)  /\  ( C  e.  V  /\  A  e.  V ) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
) )  ->  (
( F `  2
)  =  ( F `
 0 )  -> 
2  =  0 ) )
232 pm3.22 438 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E )  -> 
( { C ,  A }  e.  ran  E  /\  { B ,  C }  e.  ran  E ) )
2332323adant1 976 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E )  -> 
( { C ,  A }  e.  ran  E  /\  { B ,  C }  e.  ran  E ) )
234233adantl 454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) )  ->  ( { C ,  A }  e.  ran  E  /\  { B ,  C }  e.  ran  E ) )
235234ad3antlr 713 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  e.  V  /\  B  e.  V )  /\  ( C  e.  V  /\  A  e.  V
) )  /\  ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/= 
A ) )  /\  E : dom  E -1-1-onto-> ran  E
)  ->  ( { C ,  A }  e.  ran  E  /\  { B ,  C }  e.  ran  E ) )
236 f1ocnvfvrneq 6021 . . . . . . . . . . . . . . . . . 18  |-  ( ( E : dom  E -1-1-> ran 
E  /\  ( { C ,  A }