Theorem frgra3v 25809

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 25144	. . . . . 6 |- ( { A , B , C } USGrph E -> ( { A , B , C } e. _V /\ E e. _V ) )
2		isfrgra 25797	. . . . . 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 473	. . . 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 512	. . . . 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 473	. . . 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 264	. . 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 3969	. . . . . . . . 9 |- ( k = A -> { k } = { A } )
9	8	difeq2d 3540	. . . . . . . 8 |- ( k = A -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { A } ) )
10		preq2 4043	. . . . . . . . . . 11 |- ( k = A -> { x , k } = { x , A } )
11	10	preq1d 4048	. . . . . . . . . 10 |- ( k = A -> { { x , k } , { x , l } } = { { x , A } , { x , l } } )
12	11	sseq1d 3445	. . . . . . . . 9 |- ( k = A -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , A } , { x , l } } C_ ran E ) )
13	12	reubidv 2961	. . . . . . . 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 2987	. . . . . . 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 3969	. . . . . . . . 9 |- ( k = B -> { k } = { B } )
16	15	difeq2d 3540	. . . . . . . 8 |- ( k = B -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { B } ) )
17		preq2 4043	. . . . . . . . . . 11 |- ( k = B -> { x , k } = { x , B } )
18	17	preq1d 4048	. . . . . . . . . 10 |- ( k = B -> { { x , k } , { x , l } } = { { x , B } , { x , l } } )
19	18	sseq1d 3445	. . . . . . . . 9 |- ( k = B -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , B } , { x , l } } C_ ran E ) )
20	19	reubidv 2961	. . . . . . . 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 2987	. . . . . . 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 3969	. . . . . . . . 9 |- ( k = C -> { k } = { C } )
23	22	difeq2d 3540	. . . . . . . 8 |- ( k = C -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { C } ) )
24		preq2 4043	. . . . . . . . . . 11 |- ( k = C -> { x , k } = { x , C } )
25	24	preq1d 4048	. . . . . . . . . 10 |- ( k = C -> { { x , k } , { x , l } } = { { x , C } , { x , l } } )
26	25	sseq1d 3445	. . . . . . . . 9 |- ( k = C -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , C } , { x , l } } C_ ran E ) )
27	26	reubidv 2961	. . . . . . . 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 2987	. . . . . . 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 4014	. . . . . 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 472	. . . . 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 472	. . . 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 4058	. . . . . . . . . . 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 3539	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = ( { B , C , A } \ { A } ) )
35		necom 2696	. . . . . . . . . . . . 13 |- ( A =/= B <-> B =/= A )
36	35	biimpi 199	. . . . . . . . . . . 12 |- ( A =/= B -> B =/= A )
37		necom 2696	. . . . . . . . . . . . 13 |- ( A =/= C <-> C =/= A )
38	37	biimpi 199	. . . . . . . . . . . 12 |- ( A =/= C -> C =/= A )
39	36, 38	anim12i 576	. . . . . . . . . . 11 |- ( ( A =/= B /\ A =/= C ) -> ( B =/= A /\ C =/= A ) )
40	39	3adant3 1050	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( B =/= A /\ C =/= A ) )
41		diftpsn3 4101	. . . . . . . . . 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 2505	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = { B , C } )
44	43	raleqdv 2979	. . . . . . 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 4058	. . . . . . . . . . . 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 3539	. . . . . . . . 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 2696	. . . . . . . . . . . . 13 |- ( B =/= C <-> C =/= B )
51	50	biimpi 199	. . . . . . . . . . . 12 |- ( B =/= C -> C =/= B )
52	49, 51	anim12ci 577	. . . . . . . . . . 11 |- ( ( A =/= B /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
53	52	3adant2 1049	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
54		diftpsn3 4101	. . . . . . . . . 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 2505	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = { C , A } )
57	56	raleqdv 2979	. . . . . . 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 4101	. . . . . . . . 9 |- ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
59	58	3adant1 1048	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
60	59	raleqdv 2979	. . . . . . 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 1365	. . . . . 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 473	. . . . 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 472	. . . 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 4043	. . . . . . . . . . . 12 |- ( l = B -> { x , l } = { x , B } )
65	64	preq2d 4049	. . . . . . . . . . 11 |- ( l = B -> { { x , A } , { x , l } } = { { x , A } , { x , B } } )
66	65	sseq1d 3445	. . . . . . . . . 10 |- ( l = B -> ( { { x , A } , { x , l } } C_ ran E <-> { { x , A } , { x , B } } C_ ran E ) )
67	66	reubidv 2961	. . . . . . . . 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 4043	. . . . . . . . . . . 12 |- ( l = C -> { x , l } = { x , C } )
69	68	preq2d 4049	. . . . . . . . . . 11 |- ( l = C -> { { x , A } , { x , l } } = { { x , A } , { x , C } } )
70	69	sseq1d 3445	. . . . . . . . . 10 |- ( l = C -> ( { { x , A } , { x , l } } C_ ran E <-> { { x , A } , { x , C } } C_ ran E ) )
71	70	reubidv 2961	. . . . . . . . 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 4012	. . . . . . . 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 1048	. . . . . . 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 4049	. . . . . . . . . . . 12 |- ( l = C -> { { x , B } , { x , l } } = { { x , B } , { x , C } } )
75	74	sseq1d 3445	. . . . . . . . . . 11 |- ( l = C -> ( { { x , B } , { x , l } } C_ ran E <-> { { x , B } , { x , C } } C_ ran E ) )
76	75	reubidv 2961	. . . . . . . . . 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 4043	. . . . . . . . . . . . 13 |- ( l = A -> { x , l } = { x , A } )
78	77	preq2d 4049	. . . . . . . . . . . 12 |- ( l = A -> { { x , B } , { x , l } } = { { x , B } , { x , A } } )
79	78	sseq1d 3445	. . . . . . . . . . 11 |- ( l = A -> ( { { x , B } , { x , l } } C_ ran E <-> { { x , B } , { x , A } } C_ ran E ) )
80	79	reubidv 2961	. . . . . . . . . 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 4012	. . . . . . . . 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 460	. . . . . . . 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 1049	. . . . . . 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 4049	. . . . . . . . . . 11 |- ( l = A -> { { x , C } , { x , l } } = { { x , C } , { x , A } } )
85	84	sseq1d 3445	. . . . . . . . . 10 |- ( l = A -> ( { { x , C } , { x , l } } C_ ran E <-> { { x , C } , { x , A } } C_ ran E ) )
86	85	reubidv 2961	. . . . . . . . 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 4049	. . . . . . . . . . 11 |- ( l = B -> { { x , C } , { x , l } } = { { x , C } , { x , B } } )
88	87	sseq1d 3445	. . . . . . . . . 10 |- ( l = B -> ( { { x , C } , { x , l } } C_ ran E <-> { { x , C } , { x , B } } C_ ran E ) )
89	88	reubidv 2961	. . . . . . . . 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 4012	. . . . . . . 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 1050	. . . . . . 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 1365	. . . . . 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 472	. . . . 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 472	. . . 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 287	. . 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 25808	. . . . . . 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 436	. . . . . 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 1016	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( A e. X /\ C e. Z /\ B e. Y ) )
99		3ancoma 1014	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ B =/= C ) )
100		biid 244	. . . . . . . . . 10 |- ( A =/= C <-> A =/= C )
101		biid 244	. . . . . . . . . 10 |- ( A =/= B <-> A =/= B )
102	100, 101, 50	3anbi123i 1219	. . . . . . . . 9 |- ( ( A =/= C /\ A =/= B /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ C =/= B ) )
103	99, 102	bitri 257	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ C =/= B ) )
104	98, 103	anbi12i 711	. . . . . . 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 4060	. . . . . . . 8 |- { A , B , C } = { A , C , B }
106	105	breq1i 4402	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { A , C , B } USGrph E )
107		reueq1 2975	. . . . . . . . 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 25808	. . . . . . . . 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 436	. . . . . . . 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 261	. . . . . . 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 487	. . . . . 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 725	. . . . 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 1012	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ C e. Z /\ A e. X ) )
115		3anrot 1012	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= B /\ A =/= C ) <-> ( A =/= B /\ A =/= C /\ B =/= C ) )
116		biid 244	. . . . . . . . . 10 |- ( B =/= C <-> B =/= C )
117	116, 35, 37	3anbi123i 1219	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= B /\ A =/= C ) <-> ( B =/= C /\ B =/= A /\ C =/= A ) )
118	115, 117	bitr3i 259	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( B =/= C /\ B =/= A /\ C =/= A ) )
119	114, 118	anbi12i 711	. . . . . . 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 4402	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { B , C , A } USGrph E )
121		reueq1 2975	. . . . . . . . 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 25808	. . . . . . . . 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 436	. . . . . . . 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 261	. . . . . . 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 487	. . . . . 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 1014	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ A e. X /\ C e. Z ) )
128		3ancomb 1016	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= B /\ B =/= C /\ A =/= C ) )
129	35, 116, 100	3anbi123i 1219	. . . . . . . . 9 |- ( ( A =/= B /\ B =/= C /\ A =/= C ) <-> ( B =/= A /\ B =/= C /\ A =/= C ) )
130	128, 129	bitri 257	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( B =/= A /\ B =/= C /\ A =/= C ) )
131	127, 130	anbi12i 711	. . . . . . 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 4059	. . . . . . . 8 |- { A , B , C } = { B , A , C }
133	132	breq1i 4402	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { B , A , C } USGrph E )
134		reueq1 2975	. . . . . . . . 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 25808	. . . . . . . . 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 436	. . . . . . . 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 261	. . . . . . 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 487	. . . . . 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 725	. . . . 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 1012	. . . . . . . . 9 |- ( ( C e. Z /\ A e. X /\ B e. Y ) <-> ( A e. X /\ B e. Y /\ C e. Z ) )
142	141	biimpri 211	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( C e. Z /\ A e. X /\ B e. Y ) )
143		3anrot 1012	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ B =/= C /\ A =/= B ) )
144	37, 50, 101	3anbi123i 1219	. . . . . . . . . 10 |- ( ( A =/= C /\ B =/= C /\ A =/= B ) <-> ( C =/= A /\ C =/= B /\ A =/= B ) )
145	143, 144	bitri 257	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( C =/= A /\ C =/= B /\ A =/= B ) )
146	145	biimpi 199	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= A /\ C =/= B /\ A =/= B ) )
147	142, 146	anim12i 576	. . . . . . 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 4402	. . . . . . . 8 |- ( { A , B , C } USGrph E <-> { C , A , B } USGrph E )
149	148	biimpi 199	. . . . . . 7 |- ( { A , B , C } USGrph E -> { C , A , B } USGrph E )
150		reueq1 2975	. . . . . . . . 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 25808	. . . . . . . . 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 436	. . . . . . . 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 261	. . . . . . 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 485	. . . . . 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 1018	. . . . . . . . 9 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( C e. Z /\ B e. Y /\ A e. X ) )
157	156	biimpi 199	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( C e. Z /\ B e. Y /\ A e. X ) )
158	50, 37, 35	3anbi123i 1219	. . . . . . . . . 10 |- ( ( B =/= C /\ A =/= C /\ A =/= B ) <-> ( C =/= B /\ C =/= A /\ B =/= A ) )
159	158	biimpi 199	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= C /\ A =/= B ) -> ( C =/= B /\ C =/= A /\ B =/= A ) )
160	159	3com13 1236	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= B /\ C =/= A /\ B =/= A ) )
161	157, 160	anim12i 576	. . . . . . 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 4059	. . . . . . . . . 10 |- { B , C , A } = { C , B , A }
163	32, 162	eqtri 2493	. . . . . . . . 9 |- { A , B , C } = { C , B , A }
164	163	breq1i 4402	. . . . . . . 8 |- ( { A , B , C } USGrph E <-> { C , B , A } USGrph E )
165	164	biimpi 199	. . . . . . 7 |- ( { A , B , C } USGrph E -> { C , B , A } USGrph E )
166		reueq1 2975	. . . . . . . . 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 25808	. . . . . . . . 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 436	. . . . . . . 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 261	. . . . . . 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 485	. . . . . 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 725	. . . . 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 1365	. . . 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 4041	. . . . . . . . . . 11 |- { B , C } = { C , B }
175	174	eleq1i 2540	. . . . . . . . . 10 |- ( { B , C } e. ran E <-> { C , B } e. ran E )
176	175	anbi2i 708	. . . . . . . . 9 |- ( ( { B , A } e. ran E /\ { B , C } e. ran E ) <-> ( { B , A } e. ran E /\ { C , B } e. ran E ) )
177	176	anbi2i 708	. . . . . . . 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 845	. . . . . . . 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 260	. . . . . . 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 4041	. . . . . . . . . . 11 |- { C , A } = { A , C }
181	180	eleq1i 2540	. . . . . . . . . 10 |- ( { C , A } e. ran E <-> { A , C } e. ran E )
182	181	anbi2i 708	. . . . . . . . 9 |- ( ( { C , B } e. ran E /\ { C , A } e. ran E ) <-> ( { C , B } e. ran E /\ { A , C } e. ran E ) )
183	182	anbi2i 708	. . . . . . . 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 845	. . . . . . . 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 260	. . . . . . 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 4041	. . . . . . . . . . 11 |- { A , B } = { B , A }
187	186	eleq1i 2540	. . . . . . . . . 10 |- ( { A , B } e. ran E <-> { B , A } e. ran E )
188	187	anbi2i 708	. . . . . . . . 9 |- ( ( { A , C } e. ran E /\ { A , B } e. ran E ) <-> ( { A , C } e. ran E /\ { B , A } e. ran E ) )
189	188	anbi2i 708	. . . . . . . 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 845	. . . . . . . 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 260	. . . . . . 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 1219	. . . . . 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 1009	. . . . . . . 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 1012	. . . . . . . . 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 4041	. . . . . . . . . . 11 |- { B , A } = { A , B }
196	195	eleq1i 2540	. . . . . . . . . 10 |- ( { B , A } e. ran E <-> { A , B } e. ran E )
197		prcom 4041	. . . . . . . . . . 11 |- { C , B } = { B , C }
198	197	eleq1i 2540	. . . . . . . . . 10 |- ( { C , B } e. ran E <-> { B , C } e. ran E )
199		biid 244	. . . . . . . . . 10 |- ( { C , A } e. ran E <-> { C , A } e. ran E )
200	196, 198, 199	3anbi123i 1219	. . . . . . . . 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 257	. . . . . . . 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 259	. . . . . . 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 1009	. . . . . . . 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 244	. . . . . . . . 9 |- ( { A , B } e. ran E <-> { A , B } e. ran E )
205		prcom 4041	. . . . . . . . . 10 |- { A , C } = { C , A }
206	205	eleq1i 2540	. . . . . . . . 9 |- ( { A , C } e. ran E <-> { C , A } e. ran E )
207	204, 198, 206	3anbi123i 1219	. . . . . . . 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 259	. . . . . . 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 1009	. . . . . . . 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 1012	. . . . . . . . 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 1012	. . . . . . . . 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 244	. . . . . . . . . 10 |- ( { B , C } e. ran E <-> { B , C } e. ran E )
213	196, 212, 206	3anbi123i 1219	. . . . . . . . 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 279	. . . . . . . 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 259	. . . . . . 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 1219	. . . . . 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 1009	. . . . . . 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 825	. . . . . . 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 656	. . . . . . 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 279	. . . . . 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 279	. . . . 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 261	. . 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 287	. 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 441	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 189   /\ wa 376   /\ w3a 1007   = wceq 1452   e. wcel 1904   =/= wne 2641   A.wral 2756   E!wreu 2758   _Vcvv 3031   \ cdif 3387   C_ wss 3390   {csn 3959   {cpr 3961   {ctp 3963   class class class wbr 4395   ran crn 4840   USGrph cusg 25136   FriendGrph cfrgra 25795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-2 10690  df-n0 10894  df-z 10962  df-uz 11183  df-fz 11811  df-hash 12554  df-usgra 25139  df-frgra 25796

This theorem is referenced by:  3vfriswmgra  25812