Theorem frgra3v 24675

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 24011	. . . . . 6 |- ( { A , B , C } USGrph E -> ( { A , B , C } e. _V /\ E e. _V ) )
2		isfrgra 24663	. . . . . 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 16	. . . . 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 466	. . . 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 504	. . . . 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 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 , 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 256	. . 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 4037	. . . . . . . . 9 |- ( k = A -> { k } = { A } )
9	8	difeq2d 3622	. . . . . . . 8 |- ( k = A -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { A } ) )
10		preq2 4107	. . . . . . . . . . 11 |- ( k = A -> { x , k } = { x , A } )
11	10	preq1d 4112	. . . . . . . . . 10 |- ( k = A -> { { x , k } , { x , l } } = { { x , A } , { x , l } } )
12	11	sseq1d 3531	. . . . . . . . 9 |- ( k = A -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , A } , { x , l } } C_ ran E ) )
13	12	reubidv 3046	. . . . . . . 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 3072	. . . . . . 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 4037	. . . . . . . . 9 |- ( k = B -> { k } = { B } )
16	15	difeq2d 3622	. . . . . . . 8 |- ( k = B -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { B } ) )
17		preq2 4107	. . . . . . . . . . 11 |- ( k = B -> { x , k } = { x , B } )
18	17	preq1d 4112	. . . . . . . . . 10 |- ( k = B -> { { x , k } , { x , l } } = { { x , B } , { x , l } } )
19	18	sseq1d 3531	. . . . . . . . 9 |- ( k = B -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , B } , { x , l } } C_ ran E ) )
20	19	reubidv 3046	. . . . . . . 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 3072	. . . . . . 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 4037	. . . . . . . . 9 |- ( k = C -> { k } = { C } )
23	22	difeq2d 3622	. . . . . . . 8 |- ( k = C -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { C } ) )
24		preq2 4107	. . . . . . . . . . 11 |- ( k = C -> { x , k } = { x , C } )
25	24	preq1d 4112	. . . . . . . . . 10 |- ( k = C -> { { x , k } , { x , l } } = { { x , C } , { x , l } } )
26	25	sseq1d 3531	. . . . . . . . 9 |- ( k = C -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , C } , { x , l } } C_ ran E ) )
27	26	reubidv 3046	. . . . . . . 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 3072	. . . . . . 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 4078	. . . . . 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 465	. . . . 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 465	. . . 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 4122	. . . . . . . . . . 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 3621	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = ( { B , C , A } \ { A } ) )
35		necom 2736	. . . . . . . . . . . . 13 |- ( A =/= B <-> B =/= A )
36	35	biimpi 194	. . . . . . . . . . . 12 |- ( A =/= B -> B =/= A )
37		necom 2736	. . . . . . . . . . . . 13 |- ( A =/= C <-> C =/= A )
38	37	biimpi 194	. . . . . . . . . . . 12 |- ( A =/= C -> C =/= A )
39	36, 38	anim12i 566	. . . . . . . . . . 11 |- ( ( A =/= B /\ A =/= C ) -> ( B =/= A /\ C =/= A ) )
40	39	3adant3 1016	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( B =/= A /\ C =/= A ) )
41		diftpsn3 4165	. . . . . . . . . 10 |- ( ( B =/= A /\ C =/= A ) -> ( { B , C , A } \ { A } ) = { B , C } )
42	40, 41	syl 16	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { B , C , A } \ { A } ) = { B , C } )
43	34, 42	eqtrd 2508	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = { B , C } )
44	43	raleqdv 3064	. . . . . . 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 4122	. . . . . . . . . . . 12 |- { C , A , B } = { A , B , C }
46	45	eqcomi 2480	. . . . . . . . . . 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 3621	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = ( { C , A , B } \ { B } ) )
49		id 22	. . . . . . . . . . . 12 |- ( A =/= B -> A =/= B )
50		necom 2736	. . . . . . . . . . . . 13 |- ( B =/= C <-> C =/= B )
51	50	biimpi 194	. . . . . . . . . . . 12 |- ( B =/= C -> C =/= B )
52	49, 51	anim12ci 567	. . . . . . . . . . 11 |- ( ( A =/= B /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
53	52	3adant2 1015	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
54		diftpsn3 4165	. . . . . . . . . 10 |- ( ( C =/= B /\ A =/= B ) -> ( { C , A , B } \ { B } ) = { C , A } )
55	53, 54	syl 16	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { C , A , B } \ { B } ) = { C , A } )
56	48, 55	eqtrd 2508	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = { C , A } )
57	56	raleqdv 3064	. . . . . . 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 4165	. . . . . . . . 9 |- ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
59	58	3adant1 1014	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
60	59	raleqdv 3064	. . . . . . 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 1299	. . . . . 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 466	. . . . 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 465	. . . 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 4107	. . . . . . . . . . . 12 |- ( l = B -> { x , l } = { x , B } )
65	64	preq2d 4113	. . . . . . . . . . 11 |- ( l = B -> { { x , A } , { x , l } } = { { x , A } , { x , B } } )
66	65	sseq1d 3531	. . . . . . . . . 10 |- ( l = B -> ( { { x , A } , { x , l } } C_ ran E <-> { { x , A } , { x , B } } C_ ran E ) )
67	66	reubidv 3046	. . . . . . . . 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 4107	. . . . . . . . . . . 12 |- ( l = C -> { x , l } = { x , C } )
69	68	preq2d 4113	. . . . . . . . . . 11 |- ( l = C -> { { x , A } , { x , l } } = { { x , A } , { x , C } } )
70	69	sseq1d 3531	. . . . . . . . . 10 |- ( l = C -> ( { { x , A } , { x , l } } C_ ran E <-> { { x , A } , { x , C } } C_ ran E ) )
71	70	reubidv 3046	. . . . . . . . 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 4076	. . . . . . . 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 1014	. . . . . . 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 4113	. . . . . . . . . . . 12 |- ( l = C -> { { x , B } , { x , l } } = { { x , B } , { x , C } } )
75	74	sseq1d 3531	. . . . . . . . . . 11 |- ( l = C -> ( { { x , B } , { x , l } } C_ ran E <-> { { x , B } , { x , C } } C_ ran E ) )
76	75	reubidv 3046	. . . . . . . . . 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 4107	. . . . . . . . . . . . 13 |- ( l = A -> { x , l } = { x , A } )
78	77	preq2d 4113	. . . . . . . . . . . 12 |- ( l = A -> { { x , B } , { x , l } } = { { x , B } , { x , A } } )
79	78	sseq1d 3531	. . . . . . . . . . 11 |- ( l = A -> ( { { x , B } , { x , l } } C_ ran E <-> { { x , B } , { x , A } } C_ ran E ) )
80	79	reubidv 3046	. . . . . . . . . 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 4076	. . . . . . . . 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 453	. . . . . . . 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 1015	. . . . . . 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 4113	. . . . . . . . . . 11 |- ( l = A -> { { x , C } , { x , l } } = { { x , C } , { x , A } } )
85	84	sseq1d 3531	. . . . . . . . . 10 |- ( l = A -> ( { { x , C } , { x , l } } C_ ran E <-> { { x , C } , { x , A } } C_ ran E ) )
86	85	reubidv 3046	. . . . . . . . 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 4113	. . . . . . . . . . 11 |- ( l = B -> { { x , C } , { x , l } } = { { x , C } , { x , B } } )
88	87	sseq1d 3531	. . . . . . . . . 10 |- ( l = B -> ( { { x , C } , { x , l } } C_ ran E <-> { { x , C } , { x , B } } C_ ran E ) )
89	88	reubidv 3046	. . . . . . . . 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 4076	. . . . . . . 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 1016	. . . . . . 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 1299	. . . . . 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 465	. . . . 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 465	. . . 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 279	. . 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 24674	. . . . . . 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 429	. . . . . 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 982	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( A e. X /\ C e. Z /\ B e. Y ) )
99		3ancoma 980	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ B =/= C ) )
100		biid 236	. . . . . . . . . 10 |- ( A =/= C <-> A =/= C )
101		biid 236	. . . . . . . . . 10 |- ( A =/= B <-> A =/= B )
102	100, 101, 50	3anbi123i 1185	. . . . . . . . 9 |- ( ( A =/= C /\ A =/= B /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ C =/= B ) )
103	99, 102	bitri 249	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ C =/= B ) )
104	98, 103	anbi12i 697	. . . . . . 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 4124	. . . . . . . 8 |- { A , B , C } = { A , C , B }
106	105	breq1i 4454	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { A , C , B } USGrph E )
107		reueq1 3060	. . . . . . . . 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 12	. . . . . . . 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 24674	. . . . . . . . 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 429	. . . . . . . 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 253	. . . . . . 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 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 , A } , { x , C } } C_ ran E <-> ( { B , A } e. ran E /\ { B , C } e. ran E ) ) )
113	97, 112	anbi12d 710	. . . . 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 978	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ C e. Z /\ A e. X ) )
115		3anrot 978	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= B /\ A =/= C ) <-> ( A =/= B /\ A =/= C /\ B =/= C ) )
116		biid 236	. . . . . . . . . 10 |- ( B =/= C <-> B =/= C )
117	116, 35, 37	3anbi123i 1185	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= B /\ A =/= C ) <-> ( B =/= C /\ B =/= A /\ C =/= A ) )
118	115, 117	bitr3i 251	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( B =/= C /\ B =/= A /\ C =/= A ) )
119	114, 118	anbi12i 697	. . . . . . 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 4454	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { B , C , A } USGrph E )
121		reueq1 3060	. . . . . . . . 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 12	. . . . . . . 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 24674	. . . . . . . . 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 429	. . . . . . . 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 253	. . . . . . 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 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 , B } , { x , C } } C_ ran E <-> ( { A , B } e. ran E /\ { A , C } e. ran E ) ) )
127		3ancoma 980	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ A e. X /\ C e. Z ) )
128		3ancomb 982	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= B /\ B =/= C /\ A =/= C ) )
129	35, 116, 100	3anbi123i 1185	. . . . . . . . 9 |- ( ( A =/= B /\ B =/= C /\ A =/= C ) <-> ( B =/= A /\ B =/= C /\ A =/= C ) )
130	128, 129	bitri 249	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( B =/= A /\ B =/= C /\ A =/= C ) )
131	127, 130	anbi12i 697	. . . . . . 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 4123	. . . . . . . 8 |- { A , B , C } = { B , A , C }
133	132	breq1i 4454	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { B , A , C } USGrph E )
134		reueq1 3060	. . . . . . . . 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 12	. . . . . . . 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 24674	. . . . . . . . 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 429	. . . . . . . 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 253	. . . . . . 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 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 , B } , { x , A } } C_ ran E <-> ( { C , B } e. ran E /\ { C , A } e. ran E ) ) )
140	126, 139	anbi12d 710	. . . . 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 978	. . . . . . . . 9 |- ( ( C e. Z /\ A e. X /\ B e. Y ) <-> ( A e. X /\ B e. Y /\ C e. Z ) )
142	141	biimpri 206	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( C e. Z /\ A e. X /\ B e. Y ) )
143		3anrot 978	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ B =/= C /\ A =/= B ) )
144	37, 50, 101	3anbi123i 1185	. . . . . . . . . 10 |- ( ( A =/= C /\ B =/= C /\ A =/= B ) <-> ( C =/= A /\ C =/= B /\ A =/= B ) )
145	143, 144	bitri 249	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( C =/= A /\ C =/= B /\ A =/= B ) )
146	145	biimpi 194	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= A /\ C =/= B /\ A =/= B ) )
147	142, 146	anim12i 566	. . . . . . 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 4454	. . . . . . . 8 |- ( { A , B , C } USGrph E <-> { C , A , B } USGrph E )
149	148	biimpi 194	. . . . . . 7 |- ( { A , B , C } USGrph E -> { C , A , B } USGrph E )
150		reueq1 3060	. . . . . . . . 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 12	. . . . . . . 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 24674	. . . . . . . . 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 429	. . . . . . . 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 253	. . . . . . 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 477	. . . . . 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 984	. . . . . . . . 9 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( C e. Z /\ B e. Y /\ A e. X ) )
157	156	biimpi 194	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( C e. Z /\ B e. Y /\ A e. X ) )
158	50, 37, 35	3anbi123i 1185	. . . . . . . . . 10 |- ( ( B =/= C /\ A =/= C /\ A =/= B ) <-> ( C =/= B /\ C =/= A /\ B =/= A ) )
159	158	biimpi 194	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= C /\ A =/= B ) -> ( C =/= B /\ C =/= A /\ B =/= A ) )
160	159	3com13 1201	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= B /\ C =/= A /\ B =/= A ) )
161	157, 160	anim12i 566	. . . . . . 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 4123	. . . . . . . . . 10 |- { B , C , A } = { C , B , A }
163	32, 162	eqtri 2496	. . . . . . . . 9 |- { A , B , C } = { C , B , A }
164	163	breq1i 4454	. . . . . . . 8 |- ( { A , B , C } USGrph E <-> { C , B , A } USGrph E )
165	164	biimpi 194	. . . . . . 7 |- ( { A , B , C } USGrph E -> { C , B , A } USGrph E )
166		reueq1 3060	. . . . . . . . 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 12	. . . . . . . 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 24674	. . . . . . . . 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 429	. . . . . . . 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 253	. . . . . . 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 477	. . . . . 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 710	. . . . 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 1299	. . . 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 4105	. . . . . . . . . . 11 |- { B , C } = { C , B }
175	174	eleq1i 2544	. . . . . . . . . 10 |- ( { B , C } e. ran E <-> { C , B } e. ran E )
176	175	anbi2i 694	. . . . . . . . 9 |- ( ( { B , A } e. ran E /\ { B , C } e. ran E ) <-> ( { B , A } e. ran E /\ { C , B } e. ran E ) )
177	176	anbi2i 694	. . . . . . . 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 827	. . . . . . . 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 252	. . . . . . 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 4105	. . . . . . . . . . 11 |- { C , A } = { A , C }
181	180	eleq1i 2544	. . . . . . . . . 10 |- ( { C , A } e. ran E <-> { A , C } e. ran E )
182	181	anbi2i 694	. . . . . . . . 9 |- ( ( { C , B } e. ran E /\ { C , A } e. ran E ) <-> ( { C , B } e. ran E /\ { A , C } e. ran E ) )
183	182	anbi2i 694	. . . . . . . 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 827	. . . . . . . 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 252	. . . . . . 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 4105	. . . . . . . . . . 11 |- { A , B } = { B , A }
187	186	eleq1i 2544	. . . . . . . . . 10 |- ( { A , B } e. ran E <-> { B , A } e. ran E )
188	187	anbi2i 694	. . . . . . . . 9 |- ( ( { A , C } e. ran E /\ { A , B } e. ran E ) <-> ( { A , C } e. ran E /\ { B , A } e. ran E ) )
189	188	anbi2i 694	. . . . . . . 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 827	. . . . . . . 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 252	. . . . . . 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 1185	. . . . . 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 975	. . . . . . . 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 978	. . . . . . . . 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 4105	. . . . . . . . . . 11 |- { B , A } = { A , B }
196	195	eleq1i 2544	. . . . . . . . . 10 |- ( { B , A } e. ran E <-> { A , B } e. ran E )
197		prcom 4105	. . . . . . . . . . 11 |- { C , B } = { B , C }
198	197	eleq1i 2544	. . . . . . . . . 10 |- ( { C , B } e. ran E <-> { B , C } e. ran E )
199		biid 236	. . . . . . . . . 10 |- ( { C , A } e. ran E <-> { C , A } e. ran E )
200	196, 198, 199	3anbi123i 1185	. . . . . . . . 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 249	. . . . . . . 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 251	. . . . . . 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 975	. . . . . . . 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 236	. . . . . . . . 9 |- ( { A , B } e. ran E <-> { A , B } e. ran E )
205		prcom 4105	. . . . . . . . . 10 |- { A , C } = { C , A }
206	205	eleq1i 2544	. . . . . . . . 9 |- ( { A , C } e. ran E <-> { C , A } e. ran E )
207	204, 198, 206	3anbi123i 1185	. . . . . . . 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 251	. . . . . . 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 975	. . . . . . . 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 978	. . . . . . . . 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 978	. . . . . . . . 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 236	. . . . . . . . . 10 |- ( { B , C } e. ran E <-> { B , C } e. ran E )
213	196, 212, 206	3anbi123i 1185	. . . . . . . . 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 271	. . . . . . . 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 251	. . . . . . 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 1185	. . . . . 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 975	. . . . . . 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 806	. . . . . . 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 644	. . . . . . 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 271	. . . . . 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 271	. . . . 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 253	. . 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 279	. 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 434	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 184   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2814   E!wreu 2816   _Vcvv 3113   \ cdif 3473   C_ wss 3476   {csn 4027   {cpr 4029   {ctp 4031   class class class wbr 4447   ran crn 5000   USGrph cusg 24003   FriendGrph cfrgra 24661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-oadd 7131  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-card 8316  df-cda 8544  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-nn 10533  df-2 10590  df-n0 10792  df-z 10861  df-uz 11079  df-fz 11669  df-hash 12368  df-usgra 24006  df-frgra 24662

This theorem is referenced by:  3vfriswmgra  24678