Theorem constr3trllem2 24853

Description: Lemma for constr3trl 24861. (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.

Step	Hyp	Ref	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 >. } )
3	1, 2	constr3trllem1 24852	. . . . 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 12538	. . . . 5 |- ( F e. Word dom E -> F : ( 0..^ ( # ` F ) ) --> dom E )
5	3, 4	syl 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 )
6	1, 2	constr3lem2 24848	. . . . 5 |- ( # ` F ) = 3
7		usgraf1o 24560	. . . . . . . . . . . 12 |- ( V USGrph E -> E : dom E -1-1-onto-> ran E )
8		3cycl3dv 24844	. . . . . . . . . . . . . 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 24579	. . . . . . . . . . . . . . . . . . . 20 |- ( ( V USGrph E /\ { A , B } e. ran E ) -> ( A e. V /\ B e. V ) )
10	9	ex 432	. . . . . . . . . . . . . . . . . . 19 |- ( V USGrph E -> ( { A , B } e. ran E -> ( A e. V /\ B e. V ) ) )
11		usgraedgrnv 24579	. . . . . . . . . . . . . . . . . . . 20 |- ( ( V USGrph E /\ { C , A } e. ran E ) -> ( C e. V /\ A e. V ) )
12	11	ex 432	. . . . . . . . . . . . . . . . . . 19 |- ( V USGrph E -> ( { C , A } e. ran E -> ( C e. V /\ A e. V ) ) )
13	10, 12	anim12d 561	. . . . . . . . . . . . . . . . . 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 ) ) ) )
14	13	com12 31	. . . . . . . . . . . . . . . . 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 ) ) ) )
15	14	3adant2 1013	. . . . . . . . . . . . . . . 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 ) ) ) )
16	15	impcom 428	. . . . . . . . . . . . . . 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 ) ) )
17	1, 2	constr3lem5 24850	. . . . . . . . . . . . . . . . 17 |- ( ( F ` 0 ) = ( `' E ` { A , B } ) /\ ( F ` 1 ) = ( `' E ` { B , C } ) /\ ( F ` 2 ) = ( `' E ` { C , A } ) )
18	17	jctl 539	. . . . . . . . . . . . . . . 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 ) ) )
19	18	exp31 602	. . . . . . . . . . . . . . 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 ) ) ) ) )
20	16, 19	mpancom 667	. . . . . . . . . . . . . 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 ) ) ) ) )
21	8, 20	mpd 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 ) ) ) )
22	21	ex 432	. . . . . . . . . . . 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 ) ) ) ) )
23	7, 22	mpid 41	. . . . . . . . . . 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 ) ) ) )
24	23	imp 427	. . . . . . . . . 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 ) ) )
25	24	adantl 464	. . . . . . . . 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 9579	. . . . . . . . . . 11 |- 0 e. _V
27		1ex 9580	. . . . . . . . . . 11 |- 1 e. _V
28		2z 10892	. . . . . . . . . . 11 |- 2 e. ZZ
29	26, 27, 28	3pm3.2i 1172	. . . . . . . . . 10 |- ( 0 e. _V /\ 1 e. _V /\ 2 e. ZZ )
30		eqidd 2455	. . . . . . . . . . . . . . 15 |- ( ( F ` 0 ) = ( F ` 0 ) -> 0 = 0 )
31	30	a1i 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 5797	. . . . . . . . . . . . . . . . . . 19 |- ( E : dom E -1-1-onto-> ran E -> E : dom E -1-1-> ran E )
33	32	adantl 464	. . . . . . . . . . . . . . . . . 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 991	. . . . . . . . . . . . . . . . . . . 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 ) )
35	34	adantl 464	. . . . . . . . . . . . . . . . . . 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 ) )
36	35	ad3antlr 728	. . . . . . . . . . . . . . . . . 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 6164	. . . . . . . . . . . . . . . . . 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 } ) )
38	33, 36, 37	syl2anc 659	. . . . . . . . . . . . . . . . 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 455	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ A e. V ) ) -> ( A e. V /\ B e. V ) )
40		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A e. V /\ B e. V ) -> B e. V )
41		simpl 455	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( C e. V /\ A e. V ) -> C e. V )
42	40, 41	anim12i 564	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ A e. V ) ) -> ( B e. V /\ C e. V ) )
43		preq12bg 4195	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
44	39, 42, 43	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . 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 2651	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A =/= B <-> -. A = B )
46		pm2.21 108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -. A = B -> ( A = B -> 0 = 1 ) )
47	45, 46	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( A =/= B -> ( A = B -> 0 = 1 ) )
48	47	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A =/= B /\ B =/= C /\ C =/= A ) -> ( A = B -> 0 = 1 ) )
49	48	com12 31	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A = B -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 0 = 1 ) )
50	49	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A = B /\ B = C ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 0 = 1 ) )
51		df-ne 2651	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( C =/= A <-> -. C = A )
52		pm2.21 108	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. C = A -> ( C = A -> 0 = 1 ) )
53	51, 52	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( C =/= A -> ( C = A -> 0 = 1 ) )
54	53	3ad2ant3 1017	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( A =/= B /\ B =/= C /\ C =/= A ) -> ( C = A -> 0 = 1 ) )
55	54	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( C = A -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 0 = 1 ) )
56	55	eqcoms 2466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A = C -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 0 = 1 ) )
57	56	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A = C /\ B = B ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 0 = 1 ) )
58	50, 57	jaoi 377	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( A = B /\ B = C ) \/ ( A = C /\ B = B ) ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 0 = 1 ) )
59	44, 58	syl6bi 228	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
60	59	com23 78	. . . . . . . . . . . . . . . . . . . 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 ) ) )
61	60	adantr 463	. . . . . . . . . . . . . . . . . . 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 ) ) )
62	61	imp 427	. . . . . . . . . . . . . . . . . 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 ) )
63	62	adantr 463	. . . . . . . . . . . . . . . . 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 ) )
64	38, 63	syld 44	. . . . . . . . . . . . . . . 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 ) )
65	64	adantl 464	. . . . . . . . . . . . . . 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 2473	. . . . . . . . . . . . . . . . . 18 |- ( ( ( F ` 0 ) = ( `' E ` { A , B } ) /\ ( F ` 1 ) = ( `' E ` { B , C } ) ) -> ( ( F ` 0 ) = ( F ` 1 ) <-> ( `' E ` { A , B } ) = ( `' E ` { B , C } ) ) )
67	66	3adant3 1014	. . . . . . . . . . . . . . . . 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 } ) ) )
68	67	imbi1d 315	. . . . . . . . . . . . . . . 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 ) ) )
69	68	adantr 463	. . . . . . . . . . . . . . 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 ) ) )
70	65, 69	mpbird 232	. . . . . . . . . . . . . 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 992	. . . . . . . . . . . . . . . . . . . 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 ) )
72	71	adantl 464	. . . . . . . . . . . . . . . . . . 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 ) )
73	72	ad3antlr 728	. . . . . . . . . . . . . . . . . 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 6164	. . . . . . . . . . . . . . . . . 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 } ) )
75	33, 73, 74	syl2anc 659	. . . . . . . . . . . . . . . . 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 4195	. . . . . . . . . . . . . . . . . . . . . 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 108	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. A = B -> ( A = B -> 0 = 2 ) )
78	45, 77	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A =/= B -> ( A = B -> 0 = 2 ) )
79	78	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( A =/= B /\ B =/= C /\ C =/= A ) -> ( A = B -> 0 = 2 ) )
80	79	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A = B -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 0 = 2 ) )
81	80	eqcoms 2466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( B = A -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 0 = 2 ) )
82	81	adantl 464	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A = C /\ B = A ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 0 = 2 ) )
83		df-ne 2651	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( B =/= C <-> -. B = C )
84		pm2.21 108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -. B = C -> ( B = C -> 0 = 2 ) )
85	83, 84	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( B =/= C -> ( B = C -> 0 = 2 ) )
86	85	3ad2ant2 1016	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A =/= B /\ B =/= C /\ C =/= A ) -> ( B = C -> 0 = 2 ) )
87	86	com12 31	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( B = C -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 0 = 2 ) )
88	87	adantl 464	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A = A /\ B = C ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 0 = 2 ) )
89	82, 88	jaoi 377	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( A = C /\ B = A ) \/ ( A = A /\ B = C ) ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 0 = 2 ) )
90	76, 89	syl6bi 228	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
91	90	com23 78	. . . . . . . . . . . . . . . . . . . 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 ) ) )
92	91	adantr 463	. . . . . . . . . . . . . . . . . . 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 ) ) )
93	92	imp 427	. . . . . . . . . . . . . . . . . 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 ) )
94	93	adantr 463	. . . . . . . . . . . . . . . . 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 ) )
95	75, 94	syld 44	. . . . . . . . . . . . . . . 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 ) )
96	95	adantl 464	. . . . . . . . . . . . . . 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 2473	. . . . . . . . . . . . . . . . . 18 |- ( ( ( F ` 0 ) = ( `' E ` { A , B } ) /\ ( F ` 2 ) = ( `' E ` { C , A } ) ) -> ( ( F ` 0 ) = ( F ` 2 ) <-> ( `' E ` { A , B } ) = ( `' E ` { C , A } ) ) )
98	97	3adant2 1013	. . . . . . . . . . . . . . . . 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 } ) ) )
99	98	imbi1d 315	. . . . . . . . . . . . . . . 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 ) ) )
100	99	adantr 463	. . . . . . . . . . . . . . 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 ) ) )
101	96, 100	mpbird 232	. . . . . . . . . . . . . 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 ) )
102	31, 70, 101	3jca 1174	. . . . . . . . . . . . 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 ) ) )
103	102	adantl 464	. . . . . . . . . . . 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 5848	. . . . . . . . . . . . . . . 16 |- ( y = 0 -> ( F ` y ) = ( F ` 0 ) )
105	104	eqeq2d 2468	. . . . . . . . . . . . . . 15 |- ( y = 0 -> ( ( F ` 0 ) = ( F ` y ) <-> ( F ` 0 ) = ( F ` 0 ) ) )
106		eqeq2 2469	. . . . . . . . . . . . . . 15 |- ( y = 0 -> ( 0 = y <-> 0 = 0 ) )
107	105, 106	imbi12d 318	. . . . . . . . . . . . . 14 |- ( y = 0 -> ( ( ( F ` 0 ) = ( F ` y ) -> 0 = y ) <-> ( ( F ` 0 ) = ( F ` 0 ) -> 0 = 0 ) ) )
108		fveq2 5848	. . . . . . . . . . . . . . . 16 |- ( y = 1 -> ( F ` y ) = ( F ` 1 ) )
109	108	eqeq2d 2468	. . . . . . . . . . . . . . 15 |- ( y = 1 -> ( ( F ` 0 ) = ( F ` y ) <-> ( F ` 0 ) = ( F ` 1 ) ) )
110		eqeq2 2469	. . . . . . . . . . . . . . 15 |- ( y = 1 -> ( 0 = y <-> 0 = 1 ) )
111	109, 110	imbi12d 318	. . . . . . . . . . . . . 14 |- ( y = 1 -> ( ( ( F ` 0 ) = ( F ` y ) -> 0 = y ) <-> ( ( F ` 0 ) = ( F ` 1 ) -> 0 = 1 ) ) )
112		fveq2 5848	. . . . . . . . . . . . . . . 16 |- ( y = 2 -> ( F ` y ) = ( F ` 2 ) )
113	112	eqeq2d 2468	. . . . . . . . . . . . . . 15 |- ( y = 2 -> ( ( F ` 0 ) = ( F ` y ) <-> ( F ` 0 ) = ( F ` 2 ) ) )
114		eqeq2 2469	. . . . . . . . . . . . . . 15 |- ( y = 2 -> ( 0 = y <-> 0 = 2 ) )
115	113, 114	imbi12d 318	. . . . . . . . . . . . . 14 |- ( y = 2 -> ( ( ( F ` 0 ) = ( F ` y ) -> 0 = y ) <-> ( ( F ` 0 ) = ( F ` 2 ) -> 0 = 2 ) ) )
116	107, 111, 115	raltpg 4067	. . . . . . . . . . . . 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 ) ) ) )
117	116	adantr 463	. . . . . . . . . . . 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 ) ) ) )
118	103, 117	mpbird 232	. . . . . . . . . . 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 447	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( { A , B } e. ran E /\ { B , C } e. ran E ) -> ( { B , C } e. ran E /\ { A , B } e. ran E ) )
120	119	3adant3 1014	. . . . . . . . . . . . . . . . . . . 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 ) )
121	120	adantl 464	. . . . . . . . . . . . . . . . . . 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 ) )
122	121	ad3antlr 728	. . . . . . . . . . . . . . . . . 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 6164	. . . . . . . . . . . . . . . . . 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 } ) )
124	33, 122, 123	syl2anc 659	. . . . . . . . . . . . . . . . 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 4195	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
126	42, 39, 125	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . 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 108	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. A = B -> ( A = B -> 1 = 0 ) )
128	45, 127	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A =/= B -> ( A = B -> 1 = 0 ) )
129	128	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( A =/= B /\ B =/= C /\ C =/= A ) -> ( A = B -> 1 = 0 ) )
130	129	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A = B -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 1 = 0 ) )
131	130	eqcoms 2466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( B = A -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 1 = 0 ) )
132	131	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( B = A /\ C = B ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 1 = 0 ) )
133		pm2.21 108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -. C = A -> ( C = A -> 1 = 0 ) )
134	51, 133	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( C =/= A -> ( C = A -> 1 = 0 ) )
135	134	3ad2ant3 1017	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A =/= B /\ B =/= C /\ C =/= A ) -> ( C = A -> 1 = 0 ) )
136	135	com12 31	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( C = A -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 1 = 0 ) )
137	136	adantl 464	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( B = B /\ C = A ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 1 = 0 ) )
138	132, 137	jaoi 377	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( B = A /\ C = B ) \/ ( B = B /\ C = A ) ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 1 = 0 ) )
139	126, 138	syl6bi 228	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
140	139	com23 78	. . . . . . . . . . . . . . . . . . . 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 ) ) )
141	140	adantr 463	. . . . . . . . . . . . . . . . . . 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 ) ) )
142	141	imp 427	. . . . . . . . . . . . . . . . . 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 ) )
143	142	adantr 463	. . . . . . . . . . . . . . . . 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 ) )
144	124, 143	syld 44	. . . . . . . . . . . . . . . 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 ) )
145	144	adantl 464	. . . . . . . . . . . . . . 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 2473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( F ` 1 ) = ( `' E ` { B , C } ) /\ ( F ` 0 ) = ( `' E ` { A , B } ) ) -> ( ( F ` 1 ) = ( F ` 0 ) <-> ( `' E ` { B , C } ) = ( `' E ` { A , B } ) ) )
147	146	ancoms 451	. . . . . . . . . . . . . . . . . 18 |- ( ( ( F ` 0 ) = ( `' E ` { A , B } ) /\ ( F ` 1 ) = ( `' E ` { B , C } ) ) -> ( ( F ` 1 ) = ( F ` 0 ) <-> ( `' E ` { B , C } ) = ( `' E ` { A , B } ) ) )
148	147	3adant3 1014	. . . . . . . . . . . . . . . . 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 } ) ) )
149	148	imbi1d 315	. . . . . . . . . . . . . . . 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 ) ) )
150	149	adantr 463	. . . . . . . . . . . . . . 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 ) ) )
151	145, 150	mpbird 232	. . . . . . . . . . . . . 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 2455	. . . . . . . . . . . . . . 15 |- ( ( F ` 1 ) = ( F ` 1 ) -> 1 = 1 )
153	152	a1i 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 993	. . . . . . . . . . . . . . . . . . . 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 ) )
155	154	adantl 464	. . . . . . . . . . . . . . . . . . 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 ) )
156	155	ad3antlr 728	. . . . . . . . . . . . . . . . . 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 6164	. . . . . . . . . . . . . . . . . 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 } ) )
158	33, 156, 157	syl2anc 659	. . . . . . . . . . . . . . . . 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 4195	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
160	42, 159	sylancom 665	. . . . . . . . . . . . . . . . . . . . . 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 108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -. B = C -> ( B = C -> 1 = 2 ) )
162	83, 161	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( B =/= C -> ( B = C -> 1 = 2 ) )
163	162	3ad2ant2 1016	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A =/= B /\ B =/= C /\ C =/= A ) -> ( B = C -> 1 = 2 ) )
164	163	com12 31	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( B = C -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 1 = 2 ) )
165	164	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( B = C /\ C = A ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 1 = 2 ) )
166		pm2.21 108	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. A = B -> ( A = B -> 1 = 2 ) )
167	45, 166	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A =/= B -> ( A = B -> 1 = 2 ) )
168	167	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( A =/= B /\ B =/= C /\ C =/= A ) -> ( A = B -> 1 = 2 ) )
169	168	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A = B -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 1 = 2 ) )
170	169	eqcoms 2466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( B = A -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 1 = 2 ) )
171	170	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( B = A /\ C = C ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 1 = 2 ) )
172	165, 171	jaoi 377	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( B = C /\ C = A ) \/ ( B = A /\ C = C ) ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 1 = 2 ) )
173	160, 172	syl6bi 228	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
174	173	com23 78	. . . . . . . . . . . . . . . . . . . 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 ) ) )
175	174	adantr 463	. . . . . . . . . . . . . . . . . . 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 ) ) )
176	175	imp 427	. . . . . . . . . . . . . . . . . 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 ) )
177	176	adantr 463	. . . . . . . . . . . . . . . . 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 ) )
178	158, 177	syld 44	. . . . . . . . . . . . . . . 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 ) )
179	178	adantl 464	. . . . . . . . . . . . . . 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 2473	. . . . . . . . . . . . . . . . . 18 |- ( ( ( F ` 1 ) = ( `' E ` { B , C } ) /\ ( F ` 2 ) = ( `' E ` { C , A } ) ) -> ( ( F ` 1 ) = ( F ` 2 ) <-> ( `' E ` { B , C } ) = ( `' E ` { C , A } ) ) )
181	180	3adant1 1012	. . . . . . . . . . . . . . . . 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 } ) ) )
182	181	imbi1d 315	. . . . . . . . . . . . . . . 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 ) ) )
183	182	adantr 463	. . . . . . . . . . . . . . 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 ) ) )
184	179, 183	mpbird 232	. . . . . . . . . . . . . 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 ) )
185	151, 153, 184	3jca 1174	. . . . . . . . . . . . 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 ) ) )
186	185	adantl 464	. . . . . . . . . . . 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 ) ) )
187	104	eqeq2d 2468	. . . . . . . . . . . . . . 15 |- ( y = 0 -> ( ( F ` 1 ) = ( F ` y ) <-> ( F ` 1 ) = ( F ` 0 ) ) )
188		eqeq2 2469	. . . . . . . . . . . . . . 15 |- ( y = 0 -> ( 1 = y <-> 1 = 0 ) )
189	187, 188	imbi12d 318	. . . . . . . . . . . . . 14 |- ( y = 0 -> ( ( ( F ` 1 ) = ( F ` y ) -> 1 = y ) <-> ( ( F ` 1 ) = ( F ` 0 ) -> 1 = 0 ) ) )
190	108	eqeq2d 2468	. . . . . . . . . . . . . . 15 |- ( y = 1 -> ( ( F ` 1 ) = ( F ` y ) <-> ( F ` 1 ) = ( F ` 1 ) ) )
191		eqeq2 2469	. . . . . . . . . . . . . . 15 |- ( y = 1 -> ( 1 = y <-> 1 = 1 ) )
192	190, 191	imbi12d 318	. . . . . . . . . . . . . 14 |- ( y = 1 -> ( ( ( F ` 1 ) = ( F ` y ) -> 1 = y ) <-> ( ( F ` 1 ) = ( F ` 1 ) -> 1 = 1 ) ) )
193	112	eqeq2d 2468	. . . . . . . . . . . . . . 15 |- ( y = 2 -> ( ( F ` 1 ) = ( F ` y ) <-> ( F ` 1 ) = ( F ` 2 ) ) )
194		eqeq2 2469	. . . . . . . . . . . . . . 15 |- ( y = 2 -> ( 1 = y <-> 1 = 2 ) )
195	193, 194	imbi12d 318	. . . . . . . . . . . . . 14 |- ( y = 2 -> ( ( ( F ` 1 ) = ( F ` y ) -> 1 = y ) <-> ( ( F ` 1 ) = ( F ` 2 ) -> 1 = 2 ) ) )
196	189, 192, 195	raltpg 4067	. . . . . . . . . . . . 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 ) ) ) )
197	196	adantr 463	. . . . . . . . . . . 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 ) ) ) )
198	186, 197	mpbird 232	. . . . . . . . . . 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 447	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( { A , B } e. ran E /\ { C , A } e. ran E ) -> ( { C , A } e. ran E /\ { A , B } e. ran E ) )
200	199	3adant2 1013	. . . . . . . . . . . . . . . . . . . 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 ) )
201	200	adantl 464	. . . . . . . . . . . . . . . . . . 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 ) )
202	201	ad3antlr 728	. . . . . . . . . . . . . . . . . 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 6164	. . . . . . . . . . . . . . . . . 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 } ) )
204	33, 202, 203	syl2anc 659	. . . . . . . . . . . . . . . . 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 4195	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
206	205	ancoms 451	. . . . . . . . . . . . . . . . . . . . . 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 108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -. A = B -> ( A = B -> 2 = 0 ) )
208	45, 207	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( A =/= B -> ( A = B -> 2 = 0 ) )
209	208	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A =/= B /\ B =/= C /\ C =/= A ) -> ( A = B -> 2 = 0 ) )
210	209	com12 31	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A = B -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 2 = 0 ) )
211	210	adantl 464	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( C = A /\ A = B ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 2 = 0 ) )
212		pm2.21 108	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. B = C -> ( B = C -> 2 = 0 ) )
213	83, 212	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( B =/= C -> ( B = C -> 2 = 0 ) )
214	213	3ad2ant2 1016	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( A =/= B /\ B =/= C /\ C =/= A ) -> ( B = C -> 2 = 0 ) )
215	214	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( B = C -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 2 = 0 ) )
216	215	eqcoms 2466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( C = B -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 2 = 0 ) )
217	216	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( C = B /\ A = A ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 2 = 0 ) )
218	211, 217	jaoi 377	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( C = A /\ A = B ) \/ ( C = B /\ A = A ) ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> 2 = 0 ) )
219	206, 218	syl6bi 228	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
220	219	com23 78	. . . . . . . . . . . . . . . . . . . 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 ) ) )
221	220	adantr 463	. . . . . . . . . . . . . . . . . . 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 ) ) )
222	221	imp 427	. . . . . . . . . . . . . . . . . 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 ) )
223	222	adantr 463	. . . . . . . . . . . . . . . . 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 ) )
224	204, 223	syld 44	. . . . . . . . . . . . . . . 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 ) )
225	224	adantl 464	. . . . . . . . . . . . . . 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 2473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( F ` 2 ) = ( `' E ` { C , A } ) /\ ( F ` 0 ) = ( `' E ` { A , B } ) ) -> ( ( F ` 2 ) = ( F ` 0 ) <-> ( `' E ` { C , A } ) = ( `' E ` { A , B } ) ) )
227	226	ancoms 451	. . . . . . . . . . . . . . . . . 18 |- ( ( ( F ` 0 ) = ( `' E ` { A , B } ) /\ ( F ` 2 ) = ( `' E ` { C , A } ) ) -> ( ( F ` 2 ) = ( F ` 0 ) <-> ( `' E ` { C , A } ) = ( `' E ` { A , B } ) ) )
228	227	3adant2 1013	. . . . . . . . . . . . . . . . 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 } ) ) )
229	228	imbi1d 315	. . . . . . . . . . . . . . . 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 ) ) )
230	229	adantr 463	. . . . . . . . . . . . . . 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 ) ) )
231	225, 230	mpbird 232	. . . . . . . . . . . . . 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 447	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( { B , C } e. ran E /\ { C , A } e. ran E ) -> ( { C , A } e. ran E /\ { B , C } e. ran E ) )
233	232	3adant1 1012	. . . . . . . . . . . . . . . . . . . 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 ) )
234	233	adantl 464	. . . . . . . . . . . . . . . . . . 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 ) )
235	234	ad3antlr 728	. . . . . . . . . . . . . . . . . 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 6164	. . . . . . . . . . . . . . . . . 18 |- ( ( E : dom E -1-1-> ran E /\ ( { C , A