Theorem frgra3v 25572

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

Assertion

Ref	Expression
frgra3v	|- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( { A , B , C } USGrph E -> ( { A , B , C } FriendGrph E <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) ) )

Proof of Theorem frgra3v

Dummy variables k l x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		usgrav 24908	. . . . . 6 |- ( { A , B , C } USGrph E -> ( { A , B , C } e. _V /\ E e. _V ) )
2		isfrgra 25560	. . . . . 6 |- ( ( { A , B , C } e. _V /\ E e. _V ) -> ( { A , B , C } FriendGrph E <-> ( { A , B , C } USGrph E /\ A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E ) ) )
3	1, 2	syl 17	. . . . 5 |- ( { A , B , C } USGrph E -> ( { A , B , C } FriendGrph E <-> ( { A , B , C } USGrph E /\ A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E ) ) )
4	3	adantl 467	. . . 4 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( { A , B , C } FriendGrph E <-> ( { A , B , C } USGrph E /\ A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E ) ) )
5		ibar 506	. . . . 5 |- ( { A , B , C } USGrph E -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> ( { A , B , C } USGrph E /\ A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E ) ) )
6	5	adantl 467	. . . 4 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> ( { A , B , C } USGrph E /\ A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E ) ) )
7	4, 6	bitr4d 259	. . 3 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( { A , B , C } FriendGrph E <-> A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E ) )
8		sneq 4003	. . . . . . . . 9 |- ( k = A -> { k } = { A } )
9	8	difeq2d 3580	. . . . . . . 8 |- ( k = A -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { A } ) )
10		preq2 4074	. . . . . . . . . . 11 |- ( k = A -> { x , k } = { x , A } )
11	10	preq1d 4079	. . . . . . . . . 10 |- ( k = A -> { { x , k } , { x , l } } = { { x , A } , { x , l } } )
12	11	sseq1d 3488	. . . . . . . . 9 |- ( k = A -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , A } , { x , l } } C_ ran E ) )
13	12	reubidv 3011	. . . . . . . 8 |- ( k = A -> ( E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E ) )
14	9, 13	raleqbidv 3037	. . . . . . 7 |- ( k = A -> ( A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E ) )
15		sneq 4003	. . . . . . . . 9 |- ( k = B -> { k } = { B } )
16	15	difeq2d 3580	. . . . . . . 8 |- ( k = B -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { B } ) )
17		preq2 4074	. . . . . . . . . . 11 |- ( k = B -> { x , k } = { x , B } )
18	17	preq1d 4079	. . . . . . . . . 10 |- ( k = B -> { { x , k } , { x , l } } = { { x , B } , { x , l } } )
19	18	sseq1d 3488	. . . . . . . . 9 |- ( k = B -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , B } , { x , l } } C_ ran E ) )
20	19	reubidv 3011	. . . . . . . 8 |- ( k = B -> ( E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E ) )
21	16, 20	raleqbidv 3037	. . . . . . 7 |- ( k = B -> ( A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E ) )
22		sneq 4003	. . . . . . . . 9 |- ( k = C -> { k } = { C } )
23	22	difeq2d 3580	. . . . . . . 8 |- ( k = C -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { C } ) )
24		preq2 4074	. . . . . . . . . . 11 |- ( k = C -> { x , k } = { x , C } )
25	24	preq1d 4079	. . . . . . . . . 10 |- ( k = C -> { { x , k } , { x , l } } = { { x , C } , { x , l } } )
26	25	sseq1d 3488	. . . . . . . . 9 |- ( k = C -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , C } , { x , l } } C_ ran E ) )
27	26	reubidv 3011	. . . . . . . 8 |- ( k = C -> ( E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) )
28	23, 27	raleqbidv 3037	. . . . . . 7 |- ( k = C -> ( A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) )
29	14, 21, 28	raltpg 4045	. . . . . 6 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) ) )
30	29	adantr 466	. . . . 5 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) ) )
31	30	adantr 466	. . . 4 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) ) )
32		tprot 4089	. . . . . . . . . . 11 |- { A , B , C } = { B , C , A }
33	32	a1i 11	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> { A , B , C } = { B , C , A } )
34	33	difeq1d 3579	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = ( { B , C , A } \ { A } ) )
35		necom 2691	. . . . . . . . . . . . 13 |- ( A =/= B <-> B =/= A )
36	35	biimpi 197	. . . . . . . . . . . 12 |- ( A =/= B -> B =/= A )
37		necom 2691	. . . . . . . . . . . . 13 |- ( A =/= C <-> C =/= A )
38	37	biimpi 197	. . . . . . . . . . . 12 |- ( A =/= C -> C =/= A )
39	36, 38	anim12i 568	. . . . . . . . . . 11 |- ( ( A =/= B /\ A =/= C ) -> ( B =/= A /\ C =/= A ) )
40	39	3adant3 1025	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( B =/= A /\ C =/= A ) )
41		diftpsn3 4132	. . . . . . . . . 10 |- ( ( B =/= A /\ C =/= A ) -> ( { B , C , A } \ { A } ) = { B , C } )
42	40, 41	syl 17	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { B , C , A } \ { A } ) = { B , C } )
43	34, 42	eqtrd 2461	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = { B , C } )
44	43	raleqdv 3029	. . . . . . 7 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E <-> A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E ) )
45		tprot 4089	. . . . . . . . . . . 12 |- { C , A , B } = { A , B , C }
46	45	eqcomi 2433	. . . . . . . . . . 11 |- { A , B , C } = { C , A , B }
47	46	a1i 11	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> { A , B , C } = { C , A , B } )
48	47	difeq1d 3579	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = ( { C , A , B } \ { B } ) )
49		id 23	. . . . . . . . . . . 12 |- ( A =/= B -> A =/= B )
50		necom 2691	. . . . . . . . . . . . 13 |- ( B =/= C <-> C =/= B )
51	50	biimpi 197	. . . . . . . . . . . 12 |- ( B =/= C -> C =/= B )
52	49, 51	anim12ci 569	. . . . . . . . . . 11 |- ( ( A =/= B /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
53	52	3adant2 1024	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
54		diftpsn3 4132	. . . . . . . . . 10 |- ( ( C =/= B /\ A =/= B ) -> ( { C , A , B } \ { B } ) = { C , A } )
55	53, 54	syl 17	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { C , A , B } \ { B } ) = { C , A } )
56	48, 55	eqtrd 2461	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = { C , A } )
57	56	raleqdv 3029	. . . . . . 7 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E <-> A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E ) )
58		diftpsn3 4132	. . . . . . . . 9 |- ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
59	58	3adant1 1023	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
60	59	raleqdv 3029	. . . . . . 7 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E <-> A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) )
61	44, 57, 60	3anbi123d 1335	. . . . . 6 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) <-> ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) ) )
62	61	adantl 467	. . . . 5 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) <-> ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) ) )
63	62	adantr 466	. . . 4 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) <-> ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) ) )
64		preq2 4074	. . . . . . . . . . . 12 |- ( l = B -> { x , l } = { x , B } )
65	64	preq2d 4080	. . . . . . . . . . 11 |- ( l = B -> { { x , A } , { x , l } } = { { x , A } , { x , B } } )
66	65	sseq1d 3488	. . . . . . . . . 10 |- ( l = B -> ( { { x , A } , { x , l } } C_ ran E <-> { { x , A } , { x , B } } C_ ran E ) )
67	66	reubidv 3011	. . . . . . . . 9 |- ( l = B -> ( E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E <-> E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E ) )
68		preq2 4074	. . . . . . . . . . . 12 |- ( l = C -> { x , l } = { x , C } )
69	68	preq2d 4080	. . . . . . . . . . 11 |- ( l = C -> { { x , A } , { x , l } } = { { x , A } , { x , C } } )
70	69	sseq1d 3488	. . . . . . . . . 10 |- ( l = C -> ( { { x , A } , { x , l } } C_ ran E <-> { { x , A } , { x , C } } C_ ran E ) )
71	70	reubidv 3011	. . . . . . . . 9 |- ( l = C -> ( E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E <-> E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) )
72	67, 71	ralprg 4043	. . . . . . . 8 |- ( ( B e. Y /\ C e. Z ) -> ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E <-> ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) ) )
73	72	3adant1 1023	. . . . . . 7 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E <-> ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) ) )
74	68	preq2d 4080	. . . . . . . . . . . 12 |- ( l = C -> { { x , B } , { x , l } } = { { x , B } , { x , C } } )
75	74	sseq1d 3488	. . . . . . . . . . 11 |- ( l = C -> ( { { x , B } , { x , l } } C_ ran E <-> { { x , B } , { x , C } } C_ ran E ) )
76	75	reubidv 3011	. . . . . . . . . 10 |- ( l = C -> ( E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E <-> E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E ) )
77		preq2 4074	. . . . . . . . . . . . 13 |- ( l = A -> { x , l } = { x , A } )
78	77	preq2d 4080	. . . . . . . . . . . 12 |- ( l = A -> { { x , B } , { x , l } } = { { x , B } , { x , A } } )
79	78	sseq1d 3488	. . . . . . . . . . 11 |- ( l = A -> ( { { x , B } , { x , l } } C_ ran E <-> { { x , B } , { x , A } } C_ ran E ) )
80	79	reubidv 3011	. . . . . . . . . 10 |- ( l = A -> ( E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E <-> E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) )
81	76, 80	ralprg 4043	. . . . . . . . 9 |- ( ( C e. Z /\ A e. X ) -> ( A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E <-> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) ) )
82	81	ancoms 454	. . . . . . . 8 |- ( ( A e. X /\ C e. Z ) -> ( A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E <-> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) ) )
83	82	3adant2 1024	. . . . . . 7 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E <-> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) ) )
84	77	preq2d 4080	. . . . . . . . . . 11 |- ( l = A -> { { x , C } , { x , l } } = { { x , C } , { x , A } } )
85	84	sseq1d 3488	. . . . . . . . . 10 |- ( l = A -> ( { { x , C } , { x , l } } C_ ran E <-> { { x , C } , { x , A } } C_ ran E ) )
86	85	reubidv 3011	. . . . . . . . 9 |- ( l = A -> ( E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E <-> E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E ) )
87	64	preq2d 4080	. . . . . . . . . . 11 |- ( l = B -> { { x , C } , { x , l } } = { { x , C } , { x , B } } )
88	87	sseq1d 3488	. . . . . . . . . 10 |- ( l = B -> ( { { x , C } , { x , l } } C_ ran E <-> { { x , C } , { x , B } } C_ ran E ) )
89	88	reubidv 3011	. . . . . . . . 9 |- ( l = B -> ( E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E <-> E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) )
90	86, 89	ralprg 4043	. . . . . . . 8 |- ( ( A e. X /\ B e. Y ) -> ( A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E <-> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) ) )
91	90	3adant3 1025	. . . . . . 7 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E <-> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) ) )
92	73, 83, 91	3anbi123d 1335	. . . . . 6 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) <-> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) ) ) )
93	92	adantr 466	. . . . 5 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) <-> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) ) ) )
94	93	adantr 466	. . . 4 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) <-> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) ) ) )
95	31, 63, 94	3bitrd 282	. . 3 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) ) ) )
96		frgra3vlem2 25571	. . . . . . 7 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( { A , B , C } USGrph E -> ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E <-> ( { C , A } e. ran E /\ { C , B } e. ran E ) ) ) )
97	96	imp 430	. . . . . 6 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E <-> ( { C , A } e. ran E /\ { C , B } e. ran E ) ) )
98		3ancomb 991	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( A e. X /\ C e. Z /\ B e. Y ) )
99		3ancoma 989	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ B =/= C ) )
100		biid 239	. . . . . . . . . 10 |- ( A =/= C <-> A =/= C )
101		biid 239	. . . . . . . . . 10 |- ( A =/= B <-> A =/= B )
102	100, 101, 50	3anbi123i 1194	. . . . . . . . 9 |- ( ( A =/= C /\ A =/= B /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ C =/= B ) )
103	99, 102	bitri 252	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ C =/= B ) )
104	98, 103	anbi12i 701	. . . . . . 7 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) <-> ( ( A e. X /\ C e. Z /\ B e. Y ) /\ ( A =/= C /\ A =/= B /\ C =/= B ) ) )
105		tpcomb 4091	. . . . . . . 8 |- { A , B , C } = { A , C , B }
106	105	breq1i 4424	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { A , C , B } USGrph E )
107		reueq1 3025	. . . . . . . . 9 |- ( { A , B , C } = { A , C , B } -> ( E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E <-> E! x e. { A , C , B } { { x , A } , { x , C } } C_ ran E ) )
108	105, 107	mp1i 13	. . . . . . . 8 |- ( ( ( ( A e. X /\ C e. Z /\ B e. Y ) /\ ( A =/= C /\ A =/= B /\ C =/= B ) ) /\ { A , C , B } USGrph E ) -> ( E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E <-> E! x e. { A , C , B } { { x , A } , { x , C } } C_ ran E ) )
109		frgra3vlem2 25571	. . . . . . . . 9 |- ( ( ( A e. X /\ C e. Z /\ B e. Y ) /\ ( A =/= C /\ A =/= B /\ C =/= B ) ) -> ( { A , C , B } USGrph E -> ( E! x e. { A , C , B } { { x , A } , { x , C } } C_ ran E <-> ( { B , A } e. ran E /\ { B , C } e. ran E ) ) ) )
110	109	imp 430	. . . . . . . 8 |- ( ( ( ( A e. X /\ C e. Z /\ B e. Y ) /\ ( A =/= C /\ A =/= B /\ C =/= B ) ) /\ { A , C , B } USGrph E ) -> ( E! x e. { A , C , B } { { x , A } , { x , C } } C_ ran E <-> ( { B , A } e. ran E /\ { B , C } e. ran E ) ) )
111	108, 110	bitrd 256	. . . . . . 7 |- ( ( ( ( A e. X /\ C e. Z /\ B e. Y ) /\ ( A =/= C /\ A =/= B /\ C =/= B ) ) /\ { A , C , B } USGrph E ) -> ( E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E <-> ( { B , A } e. ran E /\ { B , C } e. ran E ) ) )
112	104, 106, 111	syl2anb 481	. . . . . 6 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E <-> ( { B , A } e. ran E /\ { B , C } e. ran E ) ) )
113	97, 112	anbi12d 715	. . . . 5 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) <-> ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { B , C } e. ran E ) ) ) )
114		3anrot 987	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ C e. Z /\ A e. X ) )
115		3anrot 987	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= B /\ A =/= C ) <-> ( A =/= B /\ A =/= C /\ B =/= C ) )
116		biid 239	. . . . . . . . . 10 |- ( B =/= C <-> B =/= C )
117	116, 35, 37	3anbi123i 1194	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= B /\ A =/= C ) <-> ( B =/= C /\ B =/= A /\ C =/= A ) )
118	115, 117	bitr3i 254	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( B =/= C /\ B =/= A /\ C =/= A ) )
119	114, 118	anbi12i 701	. . . . . . 7 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) <-> ( ( B e. Y /\ C e. Z /\ A e. X ) /\ ( B =/= C /\ B =/= A /\ C =/= A ) ) )
120	32	breq1i 4424	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { B , C , A } USGrph E )
121		reueq1 3025	. . . . . . . . 9 |- ( { A , B , C } = { B , C , A } -> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E <-> E! x e. { B , C , A } { { x , B } , { x , C } } C_ ran E ) )
122	32, 121	mp1i 13	. . . . . . . 8 |- ( ( ( ( B e. Y /\ C e. Z /\ A e. X ) /\ ( B =/= C /\ B =/= A /\ C =/= A ) ) /\ { B , C , A } USGrph E ) -> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E <-> E! x e. { B , C , A } { { x , B } , { x , C } } C_ ran E ) )
123		frgra3vlem2 25571	. . . . . . . . 9 |- ( ( ( B e. Y /\ C e. Z /\ A e. X ) /\ ( B =/= C /\ B =/= A /\ C =/= A ) ) -> ( { B , C , A } USGrph E -> ( E! x e. { B , C , A } { { x , B } , { x , C } } C_ ran E <-> ( { A , B } e. ran E /\ { A , C } e. ran E ) ) ) )
124	123	imp 430	. . . . . . . 8 |- ( ( ( ( B e. Y /\ C e. Z /\ A e. X ) /\ ( B =/= C /\ B =/= A /\ C =/= A ) ) /\ { B , C , A } USGrph E ) -> ( E! x e. { B , C , A } { { x , B } , { x , C } } C_ ran E <-> ( { A , B } e. ran E /\ { A , C } e. ran E ) ) )
125	122, 124	bitrd 256	. . . . . . 7 |- ( ( ( ( B e. Y /\ C e. Z /\ A e. X ) /\ ( B =/= C /\ B =/= A /\ C =/= A ) ) /\ { B , C , A } USGrph E ) -> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E <-> ( { A , B } e. ran E /\ { A , C } e. ran E ) ) )
126	119, 120, 125	syl2anb 481	. . . . . 6 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E <-> ( { A , B } e. ran E /\ { A , C } e. ran E ) ) )
127		3ancoma 989	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ A e. X /\ C e. Z ) )
128		3ancomb 991	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= B /\ B =/= C /\ A =/= C ) )
129	35, 116, 100	3anbi123i 1194	. . . . . . . . 9 |- ( ( A =/= B /\ B =/= C /\ A =/= C ) <-> ( B =/= A /\ B =/= C /\ A =/= C ) )
130	128, 129	bitri 252	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( B =/= A /\ B =/= C /\ A =/= C ) )
131	127, 130	anbi12i 701	. . . . . . 7 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) <-> ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( B =/= A /\ B =/= C /\ A =/= C ) ) )
132		tpcoma 4090	. . . . . . . 8 |- { A , B , C } = { B , A , C }
133	132	breq1i 4424	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { B , A , C } USGrph E )
134		reueq1 3025	. . . . . . . . 9 |- ( { A , B , C } = { B , A , C } -> ( E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E <-> E! x e. { B , A , C } { { x , B } , { x , A } } C_ ran E ) )
135	132, 134	mp1i 13	. . . . . . . 8 |- ( ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( B =/= A /\ B =/= C /\ A =/= C ) ) /\ { B , A , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E <-> E! x e. { B , A , C } { { x , B } , { x , A } } C_ ran E ) )
136		frgra3vlem2 25571	. . . . . . . . 9 |- ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( B =/= A /\ B =/= C /\ A =/= C ) ) -> ( { B , A , C } USGrph E -> ( E! x e. { B , A , C } { { x , B } , { x , A } } C_ ran E <-> ( { C , B } e. ran E /\ { C , A } e. ran E ) ) ) )
137	136	imp 430	. . . . . . . 8 |- ( ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( B =/= A /\ B =/= C /\ A =/= C ) ) /\ { B , A , C } USGrph E ) -> ( E! x e. { B , A , C } { { x , B } , { x , A } } C_ ran E <-> ( { C , B } e. ran E /\ { C , A } e. ran E ) ) )
138	135, 137	bitrd 256	. . . . . . 7 |- ( ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( B =/= A /\ B =/= C /\ A =/= C ) ) /\ { B , A , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E <-> ( { C , B } e. ran E /\ { C , A } e. ran E ) ) )
139	131, 133, 138	syl2anb 481	. . . . . 6 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E <-> ( { C , B } e. ran E /\ { C , A } e. ran E ) ) )
140	126, 139	anbi12d 715	. . . . 5 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) <-> ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { C , A } e. ran E ) ) ) )
141		3anrot 987	. . . . . . . . 9 |- ( ( C e. Z /\ A e. X /\ B e. Y ) <-> ( A e. X /\ B e. Y /\ C e. Z ) )
142	141	biimpri 209	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( C e. Z /\ A e. X /\ B e. Y ) )
143		3anrot 987	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ B =/= C /\ A =/= B ) )
144	37, 50, 101	3anbi123i 1194	. . . . . . . . . 10 |- ( ( A =/= C /\ B =/= C /\ A =/= B ) <-> ( C =/= A /\ C =/= B /\ A =/= B ) )
145	143, 144	bitri 252	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( C =/= A /\ C =/= B /\ A =/= B ) )
146	145	biimpi 197	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= A /\ C =/= B /\ A =/= B ) )
147	142, 146	anim12i 568	. . . . . . 7 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( C =/= A /\ C =/= B /\ A =/= B ) ) )
148	46	breq1i 4424	. . . . . . . 8 |- ( { A , B , C } USGrph E <-> { C , A , B } USGrph E )
149	148	biimpi 197	. . . . . . 7 |- ( { A , B , C } USGrph E -> { C , A , B } USGrph E )
150		reueq1 3025	. . . . . . . . 9 |- ( { A , B , C } = { C , A , B } -> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E <-> E! x e. { C , A , B } { { x , C } , { x , A } } C_ ran E ) )
151	46, 150	mp1i 13	. . . . . . . 8 |- ( ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( C =/= A /\ C =/= B /\ A =/= B ) ) /\ { C , A , B } USGrph E ) -> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E <-> E! x e. { C , A , B } { { x , C } , { x , A } } C_ ran E ) )
152		frgra3vlem2 25571	. . . . . . . . 9 |- ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( C =/= A /\ C =/= B /\ A =/= B ) ) -> ( { C , A , B } USGrph E -> ( E! x e. { C , A , B } { { x , C } , { x , A } } C_ ran E <-> ( { B , C } e. ran E /\ { B , A } e. ran E ) ) ) )
153	152	imp 430	. . . . . . . 8 |- ( ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( C =/= A /\ C =/= B /\ A =/= B ) ) /\ { C , A , B } USGrph E ) -> ( E! x e. { C , A , B } { { x , C } , { x , A } } C_ ran E <-> ( { B , C } e. ran E /\ { B , A } e. ran E ) ) )
154	151, 153	bitrd 256	. . . . . . 7 |- ( ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( C =/= A /\ C =/= B /\ A =/= B ) ) /\ { C , A , B } USGrph E ) -> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E <-> ( { B , C } e. ran E /\ { B , A } e. ran E ) ) )
155	147, 149, 154	syl2an 479	. . . . . 6 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E <-> ( { B , C } e. ran E /\ { B , A } e. ran E ) ) )
156		3anrev 993	. . . . . . . . 9 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( C e. Z /\ B e. Y /\ A e. X ) )
157	156	biimpi 197	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( C e. Z /\ B e. Y /\ A e. X ) )
158	50, 37, 35	3anbi123i 1194	. . . . . . . . . 10 |- ( ( B =/= C /\ A =/= C /\ A =/= B ) <-> ( C =/= B /\ C =/= A /\ B =/= A ) )
159	158	biimpi 197	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= C /\ A =/= B ) -> ( C =/= B /\ C =/= A /\ B =/= A ) )
160	159	3com13 1210	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= B /\ C =/= A /\ B =/= A ) )
161	157, 160	anim12i 568	. . . . . . 7 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) )
162		tpcoma 4090	. . . . . . . . . 10 |- { B , C , A } = { C , B , A }
163	32, 162	eqtri 2449	. . . . . . . . 9 |- { A , B , C } = { C , B , A }
164	163	breq1i 4424	. . . . . . . 8 |- ( { A , B , C } USGrph E <-> { C , B , A } USGrph E )
165	164	biimpi 197	. . . . . . 7 |- ( { A , B , C } USGrph E -> { C , B , A } USGrph E )
166		reueq1 3025	. . . . . . . . 9 |- ( { A , B , C } = { C , B , A } -> ( E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E <-> E! x e. { C , B , A } { { x , C } , { x , B } } C_ ran E ) )
167	163, 166	mp1i 13	. . . . . . . 8 |- ( ( ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) /\ { C , B , A } USGrph E ) -> ( E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E <-> E! x e. { C , B , A } { { x , C } , { x , B } } C_ ran E ) )
168		frgra3vlem2 25571	. . . . . . . . 9 |- ( ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) -> ( { C , B , A } USGrph E -> ( E! x e. { C , B , A } { { x , C } , { x , B } } C_ ran E <-> ( { A , C } e. ran E /\ { A , B } e. ran E ) ) ) )
169	168	imp 430	. . . . . . . 8 |- ( ( ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) /\ { C , B , A } USGrph E ) -> ( E! x e. { C , B , A } { { x , C } , { x , B } } C_ ran E <-> ( { A , C } e. ran E /\ { A , B } e. ran E ) ) )
170	167, 169	bitrd 256	. . . . . . 7 |- ( ( ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) /\ { C , B , A } USGrph E ) -> ( E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E <-> ( { A , C } e. ran E /\ { A , B } e. ran E ) ) )
171	161, 165, 170	syl2an 479	. . . . . 6 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E <-> ( { A , C } e. ran E /\ { A , B } e. ran E ) ) )
172	155, 171	anbi12d 715	. . . . 5 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) <-> ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { A , B } e. ran E ) ) ) )
173	113, 140, 172	3anbi123d 1335	. . . 4 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) ) <-> ( ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { B , C } e. ran E ) ) /\ ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { C , A } e. ran E ) ) /\ ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { A , B } e. ran E ) ) ) ) )
174		prcom 4072	. . . . . . . . . . 11 |- { B , C } = { C , B }
175	174	eleq1i 2497	. . . . . . . . . 10 |- ( { B , C } e. ran E <-> { C , B } e. ran E )
176	175	anbi2i 698	. . . . . . . . 9 |- ( ( { B , A } e. ran E /\ { B , C } e. ran E ) <-> ( { B , A } e. ran E /\ { C , B } e. ran E ) )
177	176	anbi2i 698	. . . . . . . 8 |- ( ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { B , C } e. ran E ) ) <-> ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { C , B } e. ran E ) ) )
178		anandir 836	. . . . . . . 8 |- ( ( ( { C , A } e. ran E /\ { B , A } e. ran E ) /\ { C , B } e. ran E ) <-> ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { C , B } e. ran E ) ) )
179	177, 178	bitr4i 255	. . . . . . 7 |- ( ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { B , C } e. ran E ) ) <-> ( ( { C , A } e. ran E /\ { B , A } e. ran E ) /\ { C , B } e. ran E ) )
180		prcom 4072	. . . . . . . . . . 11 |- { C , A } = { A , C }
181	180	eleq1i 2497	. . . . . . . . . 10 |- ( { C , A } e. ran E <-> { A , C } e. ran E )
182	181	anbi2i 698	. . . . . . . . 9 |- ( ( { C , B } e. ran E /\ { C , A } e. ran E ) <-> ( { C , B } e. ran E /\ { A , C } e. ran E ) )
183	182	anbi2i 698	. . . . . . . 8 |- ( ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { C , A } e. ran E ) ) <-> ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { A , C } e. ran E ) ) )
184		anandir 836	. . . . . . . 8 |- ( ( ( { A , B } e. ran E /\ { C , B } e. ran E ) /\ { A , C } e. ran E ) <-> ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { A , C } e. ran E ) ) )
185	183, 184	bitr4i 255	. . . . . . 7 |- ( ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { C , A } e. ran E ) ) <-> ( ( { A , B } e. ran E /\ { C , B } e. ran E ) /\ { A , C } e. ran E ) )
186		prcom 4072	. . . . . . . . . . 11 |- { A , B } = { B , A }
187	186	eleq1i 2497	. . . . . . . . . 10 |- ( { A , B } e. ran E <-> { B , A } e. ran E )
188	187	anbi2i 698	. . . . . . . . 9 |- ( ( { A , C } e. ran E /\ { A , B } e. ran E ) <-> ( { A , C } e. ran E /\ { B , A } e. ran E ) )
189	188	anbi2i 698	. . . . . . . 8 |- ( ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { A , B } e. ran E ) ) <-> ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { B , A } e. ran E ) ) )
190		anandir 836	. . . . . . . 8 |- ( ( ( { B , C } e. ran E /\ { A , C } e. ran E ) /\ { B , A } e. ran E ) <-> ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { B , A } e. ran E ) ) )
191	189, 190	bitr4i 255	. . . . . . 7 |- ( ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { A , B } e. ran E ) ) <-> ( ( { B , C } e. ran E /\ { A , C } e. ran E ) /\ { B , A } e. ran E ) )
192	179, 185, 191	3anbi123i 1194	. . . . . 6 |- ( ( ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { B , C } e. ran E ) ) /\ ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { C , A } e. ran E ) ) /\ ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { A , B } e. ran E ) ) ) <-> ( ( ( { C , A } e. ran E /\ { B , A } e. ran E ) /\ { C , B } e. ran E ) /\ ( ( { A , B } e. ran E /\ { C , B } e. ran E ) /\ { A , C } e. ran E ) /\ ( ( { B , C } e. ran E /\ { A , C } e. ran E ) /\ { B , A } e. ran E ) ) )
193		df-3an 984	. . . . . . . 8 |- ( ( { C , A } e. ran E /\ { B , A } e. ran E /\ { C , B } e. ran E ) <-> ( ( { C , A } e. ran E /\ { B , A } e. ran E ) /\ { C , B } e. ran E ) )
194		3anrot 987	. . . . . . . . 9 |- ( ( { C , A } e. ran E /\ { B , A } e. ran E /\ { C , B } e. ran E ) <-> ( { B , A } e. ran E /\ { C , B } e. ran E /\ { C , A } e. ran E ) )
195		prcom 4072	. . . . . . . . . . 11 |- { B , A } = { A , B }
196	195	eleq1i 2497	. . . . . . . . . 10 |- ( { B , A } e. ran E <-> { A , B } e. ran E )
197		prcom 4072	. . . . . . . . . . 11 |- { C , B } = { B , C }
198	197	eleq1i 2497	. . . . . . . . . 10 |- ( { C , B } e. ran E <-> { B , C } e. ran E )
199		biid 239	. . . . . . . . . 10 |- ( { C , A } e. ran E <-> { C , A } e. ran E )
200	196, 198, 199	3anbi123i 1194	. . . . . . . . 9 |- ( ( { B , A } e. ran E /\ { C , B } e. ran E /\ { C , A } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
201	194, 200	bitri 252	. . . . . . . 8 |- ( ( { C , A } e. ran E /\ { B , A } e. ran E /\ { C , B } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
202	193, 201	bitr3i 254	. . . . . . 7 |- ( ( ( { C , A } e. ran E /\ { B , A } e. ran E ) /\ { C , B } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
203		df-3an 984	. . . . . . . 8 |- ( ( { A , B } e. ran E /\ { C , B } e. ran E /\ { A , C } e. ran E ) <-> ( ( { A , B } e. ran E /\ { C , B } e. ran E ) /\ { A , C } e. ran E ) )
204		biid 239	. . . . . . . . 9 |- ( { A , B } e. ran E <-> { A , B } e. ran E )
205		prcom 4072	. . . . . . . . . 10 |- { A , C } = { C , A }
206	205	eleq1i 2497	. . . . . . . . 9 |- ( { A , C } e. ran E <-> { C , A } e. ran E )
207	204, 198, 206	3anbi123i 1194	. . . . . . . 8 |- ( ( { A , B } e. ran E /\ { C , B } e. ran E /\ { A , C } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
208	203, 207	bitr3i 254	. . . . . . 7 |- ( ( ( { A , B } e. ran E /\ { C , B } e. ran E ) /\ { A , C } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
209		df-3an 984	. . . . . . . 8 |- ( ( { B , C } e. ran E /\ { A , C } e. ran E /\ { B , A } e. ran E ) <-> ( ( { B , C } e. ran E /\ { A , C } e. ran E ) /\ { B , A } e. ran E ) )
210		3anrot 987	. . . . . . . . 9 |- ( ( { B , C } e. ran E /\ { A , C } e. ran E /\ { B , A } e. ran E ) <-> ( { A , C } e. ran E /\ { B , A } e. ran E /\ { B , C } e. ran E ) )
211		3anrot 987	. . . . . . . . 9 |- ( ( { A , C } e. ran E /\ { B , A } e. ran E /\ { B , C } e. ran E ) <-> ( { B , A } e. ran E /\ { B , C } e. ran E /\ { A , C } e. ran E ) )
212		biid 239	. . . . . . . . . 10 |- ( { B , C } e. ran E <-> { B , C } e. ran E )
213	196, 212, 206	3anbi123i 1194	. . . . . . . . 9 |- ( ( { B , A } e. ran E /\ { B , C } e. ran E /\ { A , C } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
214	210, 211, 213	3bitri 274	. . . . . . . 8 |- ( ( { B , C } e. ran E /\ { A , C } e. ran E /\ { B , A } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
215	209, 214	bitr3i 254	. . . . . . 7 |- ( ( ( { B , C } e. ran E /\ { A , C } e. ran E ) /\ { B , A } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
216	202, 208, 215	3anbi123i 1194	. . . . . 6 |- ( ( ( ( { C , A } e. ran E /\ { B , A } e. ran E ) /\ { C , B } e. ran E ) /\ ( ( { A , B } e. ran E /\ { C , B } e. ran E ) /\ { A , C } e. ran E ) /\ ( ( { B , C } e. ran E /\ { A , C } e. ran E ) /\ { B , A } e. ran 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 /\ { C , A } e. ran E ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) )
217		df-3an 984	. . . . . . 7 |- ( ( ( { 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 /\ { C , A } e. ran 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 /\ { C , A } e. ran 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 /\ { C , A } e. ran E ) ) )
218		anabs1 815	. . . . . . 7 |- ( ( ( ( { 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 /\ { C , A } e. ran 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 /\ { C , A } e. ran E ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) )
219		anidm 648	. . . . . . 7 |- ( ( ( { 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 /\ { C , A } e. ran E ) ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
220	217, 218, 219	3bitri 274	. . . . . 6 |- ( ( ( { 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 /\ { C , A } e. ran 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 /\ { C , A } e. ran E ) )
221	192, 216, 220	3bitri 274	. . . . 5 |- ( ( ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { B , C } e. ran E ) ) /\ ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { C , A } e. ran E ) ) /\ ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { A , B } e. ran E ) ) ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
222	221	a1i 11	. . . 4 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { B , C } e. ran E ) ) /\ ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { C , A } e. ran E ) ) /\ ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { A , B } e. ran E ) ) ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) )
223	173, 222	bitrd 256	. . 3 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) )
224	7, 95, 223	3bitrd 282	. 2 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( { A , B , C } FriendGrph E <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) )
225	224	ex 435	1 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( { A , B , C } USGrph E -> ( { A , B , C } FriendGrph E <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1867   =/= wne 2616   A.wral 2773   E!wreu 2775   _Vcvv 3078   \ cdif 3430   C_ wss 3433   {csn 3993   {cpr 3995   {ctp 3997   class class class wbr 4417   ran crn 4846   USGrph cusg 24900   FriendGrph cfrgra 25558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4529  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-cnex 9584  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604  ax-pre-mulgt0 9605

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-iun 4295  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-1o 7181  df-oadd 7185  df-er 7362  df-en 7569  df-dom 7570  df-sdom 7571  df-fin 7572  df-card 8363  df-cda 8587  df-pnf 9666  df-mnf 9667  df-xr 9668  df-ltxr 9669  df-le 9670  df-sub 9851  df-neg 9852  df-nn 10599  df-2 10657  df-n0 10859  df-z 10927  df-uz 11149  df-fz 11772  df-hash 12502  df-usgra 24903  df-frgra 25559

This theorem is referenced by:  3vfriswmgra  25575