Theorem frgra3v 28106

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 21324	. . . . . 6 |- ( { A , B , C } USGrph E -> ( { A , B , C } e. _V /\ E e. _V ) )
2		isfrgra 28094	. . . . . 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 453	. . . 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 491	. . . . 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 453	. . . 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 248	. . 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 3785	. . . . . . . . 9 |- ( k = A -> { k } = { A } )
9	8	difeq2d 3425	. . . . . . . 8 |- ( k = A -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { A } ) )
10		preq2 3844	. . . . . . . . . . 11 |- ( k = A -> { x , k } = { x , A } )
11	10	preq1d 3849	. . . . . . . . . 10 |- ( k = A -> { { x , k } , { x , l } } = { { x , A } , { x , l } } )
12	11	sseq1d 3335	. . . . . . . . 9 |- ( k = A -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , A } , { x , l } } C_ ran E ) )
13	12	reubidv 2852	. . . . . . . 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 2876	. . . . . . 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 3785	. . . . . . . . 9 |- ( k = B -> { k } = { B } )
16	15	difeq2d 3425	. . . . . . . 8 |- ( k = B -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { B } ) )
17		preq2 3844	. . . . . . . . . . 11 |- ( k = B -> { x , k } = { x , B } )
18	17	preq1d 3849	. . . . . . . . . 10 |- ( k = B -> { { x , k } , { x , l } } = { { x , B } , { x , l } } )
19	18	sseq1d 3335	. . . . . . . . 9 |- ( k = B -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , B } , { x , l } } C_ ran E ) )
20	19	reubidv 2852	. . . . . . . 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 2876	. . . . . . 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 3785	. . . . . . . . 9 |- ( k = C -> { k } = { C } )
23	22	difeq2d 3425	. . . . . . . 8 |- ( k = C -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { C } ) )
24		preq2 3844	. . . . . . . . . . 11 |- ( k = C -> { x , k } = { x , C } )
25	24	preq1d 3849	. . . . . . . . . 10 |- ( k = C -> { { x , k } , { x , l } } = { { x , C } , { x , l } } )
26	25	sseq1d 3335	. . . . . . . . 9 |- ( k = C -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , C } , { x , l } } C_ ran E ) )
27	26	reubidv 2852	. . . . . . . 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 2876	. . . . . . 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 3819	. . . . . 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 452	. . . . 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 452	. . . 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 3859	. . . . . . . . . . 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 3424	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = ( { B , C , A } \ { A } ) )
35		necom 2648	. . . . . . . . . . . . 13 |- ( A =/= B <-> B =/= A )
36	35	biimpi 187	. . . . . . . . . . . 12 |- ( A =/= B -> B =/= A )
37		necom 2648	. . . . . . . . . . . . 13 |- ( A =/= C <-> C =/= A )
38	37	biimpi 187	. . . . . . . . . . . 12 |- ( A =/= C -> C =/= A )
39	36, 38	anim12i 550	. . . . . . . . . . 11 |- ( ( A =/= B /\ A =/= C ) -> ( B =/= A /\ C =/= A ) )
40	39	3adant3 977	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( B =/= A /\ C =/= A ) )
41		diftpsn3 3897	. . . . . . . . . 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 2436	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = { B , C } )
44	43	raleqdv 2870	. . . . . . 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 3859	. . . . . . . . . . . 12 |- { C , A , B } = { A , B , C }
46	45	eqcomi 2408	. . . . . . . . . . 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 3424	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = ( { C , A , B } \ { B } ) )
49		id 20	. . . . . . . . . . . 12 |- ( A =/= B -> A =/= B )
50		necom 2648	. . . . . . . . . . . . 13 |- ( B =/= C <-> C =/= B )
51	50	biimpi 187	. . . . . . . . . . . 12 |- ( B =/= C -> C =/= B )
52	49, 51	anim12ci 551	. . . . . . . . . . 11 |- ( ( A =/= B /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
53	52	3adant2 976	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
54		diftpsn3 3897	. . . . . . . . . 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 2436	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = { C , A } )
57	56	raleqdv 2870	. . . . . . 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 3897	. . . . . . . . 9 |- ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
59	58	3adant1 975	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
60	59	raleqdv 2870	. . . . . . 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 1254	. . . . . 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 453	. . . . 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 452	. . . 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 3844	. . . . . . . . . . . 12 |- ( l = B -> { x , l } = { x , B } )
65	64	preq2d 3850	. . . . . . . . . . 11 |- ( l = B -> { { x , A } , { x , l } } = { { x , A } , { x , B } } )
66	65	sseq1d 3335	. . . . . . . . . 10 |- ( l = B -> ( { { x , A } , { x , l } } C_ ran E <-> { { x , A } , { x , B } } C_ ran E ) )
67	66	reubidv 2852	. . . . . . . . 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 3844	. . . . . . . . . . . 12 |- ( l = C -> { x , l } = { x , C } )
69	68	preq2d 3850	. . . . . . . . . . 11 |- ( l = C -> { { x , A } , { x , l } } = { { x , A } , { x , C } } )
70	69	sseq1d 3335	. . . . . . . . . 10 |- ( l = C -> ( { { x , A } , { x , l } } C_ ran E <-> { { x , A } , { x , C } } C_ ran E ) )
71	70	reubidv 2852	. . . . . . . . 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 3817	. . . . . . . 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 975	. . . . . . 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 3850	. . . . . . . . . . . 12 |- ( l = C -> { { x , B } , { x , l } } = { { x , B } , { x , C } } )
75	74	sseq1d 3335	. . . . . . . . . . 11 |- ( l = C -> ( { { x , B } , { x , l } } C_ ran E <-> { { x , B } , { x , C } } C_ ran E ) )
76	75	reubidv 2852	. . . . . . . . . 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 3844	. . . . . . . . . . . . 13 |- ( l = A -> { x , l } = { x , A } )
78	77	preq2d 3850	. . . . . . . . . . . 12 |- ( l = A -> { { x , B } , { x , l } } = { { x , B } , { x , A } } )
79	78	sseq1d 3335	. . . . . . . . . . 11 |- ( l = A -> ( { { x , B } , { x , l } } C_ ran E <-> { { x , B } , { x , A } } C_ ran E ) )
80	79	reubidv 2852	. . . . . . . . . 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 3817	. . . . . . . . 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 440	. . . . . . . 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 976	. . . . . . 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 3850	. . . . . . . . . . 11 |- ( l = A -> { { x , C } , { x , l } } = { { x , C } , { x , A } } )
85	84	sseq1d 3335	. . . . . . . . . 10 |- ( l = A -> ( { { x , C } , { x , l } } C_ ran E <-> { { x , C } , { x , A } } C_ ran E ) )
86	85	reubidv 2852	. . . . . . . . 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 3850	. . . . . . . . . . 11 |- ( l = B -> { { x , C } , { x , l } } = { { x , C } , { x , B } } )
88	87	sseq1d 3335	. . . . . . . . . 10 |- ( l = B -> ( { { x , C } , { x , l } } C_ ran E <-> { { x , C } , { x , B } } C_ ran E ) )
89	88	reubidv 2852	. . . . . . . . 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 3817	. . . . . . . 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 977	. . . . . . 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 1254	. . . . . 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 452	. . . . 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 452	. . . 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 271	. . 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 28105	. . . . . . 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 419	. . . . . 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 945	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( A e. X /\ C e. Z /\ B e. Y ) )
99		3ancoma 943	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ B =/= C ) )
100		biid 228	. . . . . . . . . 10 |- ( A =/= C <-> A =/= C )
101		biid 228	. . . . . . . . . 10 |- ( A =/= B <-> A =/= B )
102	100, 101, 50	3anbi123i 1142	. . . . . . . . 9 |- ( ( A =/= C /\ A =/= B /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ C =/= B ) )
103	99, 102	bitri 241	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ C =/= B ) )
104	98, 103	anbi12i 679	. . . . . . 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 3861	. . . . . . . 8 |- { A , B , C } = { A , C , B }
106	105	breq1i 4179	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { A , C , B } USGrph E )
107		reueq1 2866	. . . . . . . . 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 28105	. . . . . . . . 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 419	. . . . . . . 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 245	. . . . . . 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 466	. . . . . 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 692	. . . . 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 941	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ C e. Z /\ A e. X ) )
115		3anrot 941	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= B /\ A =/= C ) <-> ( A =/= B /\ A =/= C /\ B =/= C ) )
116		biid 228	. . . . . . . . . 10 |- ( B =/= C <-> B =/= C )
117	116, 35, 37	3anbi123i 1142	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= B /\ A =/= C ) <-> ( B =/= C /\ B =/= A /\ C =/= A ) )
118	115, 117	bitr3i 243	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( B =/= C /\ B =/= A /\ C =/= A ) )
119	114, 118	anbi12i 679	. . . . . . 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 4179	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { B , C , A } USGrph E )
121		reueq1 2866	. . . . . . . . 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 28105	. . . . . . . . 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 419	. . . . . . . 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 245	. . . . . . 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 466	. . . . . 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 943	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ A e. X /\ C e. Z ) )
128		3ancomb 945	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= B /\ B =/= C /\ A =/= C ) )
129	35, 116, 100	3anbi123i 1142	. . . . . . . . 9 |- ( ( A =/= B /\ B =/= C /\ A =/= C ) <-> ( B =/= A /\ B =/= C /\ A =/= C ) )
130	128, 129	bitri 241	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( B =/= A /\ B =/= C /\ A =/= C ) )
131	127, 130	anbi12i 679	. . . . . . 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 3860	. . . . . . . 8 |- { A , B , C } = { B , A , C }
133	132	breq1i 4179	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { B , A , C } USGrph E )
134		reueq1 2866	. . . . . . . . 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 28105	. . . . . . . . 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 419	. . . . . . . 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 245	. . . . . . 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 466	. . . . . 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 692	. . . . 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 941	. . . . . . . . 9 |- ( ( C e. Z /\ A e. X /\ B e. Y ) <-> ( A e. X /\ B e. Y /\ C e. Z ) )
142	141	biimpri 198	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( C e. Z /\ A e. X /\ B e. Y ) )
143		3anrot 941	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ B =/= C /\ A =/= B ) )
144	37, 50, 101	3anbi123i 1142	. . . . . . . . . 10 |- ( ( A =/= C /\ B =/= C /\ A =/= B ) <-> ( C =/= A /\ C =/= B /\ A =/= B ) )
145	143, 144	bitri 241	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( C =/= A /\ C =/= B /\ A =/= B ) )
146	145	biimpi 187	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= A /\ C =/= B /\ A =/= B ) )
147	142, 146	anim12i 550	. . . . . . 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 4179	. . . . . . . 8 |- ( { A , B , C } USGrph E <-> { C , A , B } USGrph E )
149	148	biimpi 187	. . . . . . 7 |- ( { A , B , C } USGrph E -> { C , A , B } USGrph E )
150		reueq1 2866	. . . . . . . . 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 28105	. . . . . . . . 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 419	. . . . . . . 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 245	. . . . . . 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 464	. . . . . 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 947	. . . . . . . . 9 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( C e. Z /\ B e. Y /\ A e. X ) )
157	156	biimpi 187	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( C e. Z /\ B e. Y /\ A e. X ) )
158	50, 37, 35	3anbi123i 1142	. . . . . . . . . 10 |- ( ( B =/= C /\ A =/= C /\ A =/= B ) <-> ( C =/= B /\ C =/= A /\ B =/= A ) )
159	158	biimpi 187	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= C /\ A =/= B ) -> ( C =/= B /\ C =/= A /\ B =/= A ) )
160	159	3com13 1158	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= B /\ C =/= A /\ B =/= A ) )
161	157, 160	anim12i 550	. . . . . . 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 3860	. . . . . . . . . 10 |- { B , C , A } = { C , B , A }
163	32, 162	eqtri 2424	. . . . . . . . 9 |- { A , B , C } = { C , B , A }
164	163	breq1i 4179	. . . . . . . 8 |- ( { A , B , C } USGrph E <-> { C , B , A } USGrph E )
165	164	biimpi 187	. . . . . . 7 |- ( { A , B , C } USGrph E -> { C , B , A } USGrph E )
166		reueq1 2866	. . . . . . . . 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 28105	. . . . . . . . 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 419	. . . . . . . 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 245	. . . . . . 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 464	. . . . . 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 692	. . . . 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 1254	. . . 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 3842	. . . . . . . . . . 11 |- { B , C } = { C , B }
175	174	eleq1i 2467	. . . . . . . . . 10 |- ( { B , C } e. ran E <-> { C , B } e. ran E )
176	175	anbi2i 676	. . . . . . . . 9 |- ( ( { B , A } e. ran E /\ { B , C } e. ran E ) <-> ( { B , A } e. ran E /\ { C , B } e. ran E ) )
177	176	anbi2i 676	. . . . . . . 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 803	. . . . . . . 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 244	. . . . . . 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 3842	. . . . . . . . . . 11 |- { C , A } = { A , C }
181	180	eleq1i 2467	. . . . . . . . . 10 |- ( { C , A } e. ran E <-> { A , C } e. ran E )
182	181	anbi2i 676	. . . . . . . . 9 |- ( ( { C , B } e. ran E /\ { C , A } e. ran E ) <-> ( { C , B } e. ran E /\ { A , C } e. ran E ) )
183	182	anbi2i 676	. . . . . . . 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 803	. . . . . . . 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 244	. . . . . . 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 3842	. . . . . . . . . . 11 |- { A , B } = { B , A }
187	186	eleq1i 2467	. . . . . . . . . 10 |- ( { A , B } e. ran E <-> { B , A } e. ran E )
188	187	anbi2i 676	. . . . . . . . 9 |- ( ( { A , C } e. ran E /\ { A , B } e. ran E ) <-> ( { A , C } e. ran E /\ { B , A } e. ran E ) )
189	188	anbi2i 676	. . . . . . . 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 803	. . . . . . . 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 244	. . . . . . 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 1142	. . . . . 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 938	. . . . . . . 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 941	. . . . . . . . 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 3842	. . . . . . . . . . 11 |- { B , A } = { A , B }
196	195	eleq1i 2467	. . . . . . . . . 10 |- ( { B , A } e. ran E <-> { A , B } e. ran E )
197		prcom 3842	. . . . . . . . . . 11 |- { C , B } = { B , C }
198	197	eleq1i 2467	. . . . . . . . . 10 |- ( { C , B } e. ran E <-> { B , C } e. ran E )
199		biid 228	. . . . . . . . . 10 |- ( { C , A } e. ran E <-> { C , A } e. ran E )
200	196, 198, 199	3anbi123i 1142	. . . . . . . . 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 241	. . . . . . . 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 243	. . . . . . 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 938	. . . . . . . 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 228	. . . . . . . . 9 |- ( { A , B } e. ran E <-> { A , B } e. ran E )
205		prcom 3842	. . . . . . . . . 10 |- { A , C } = { C , A }
206	205	eleq1i 2467	. . . . . . . . 9 |- ( { A , C } e. ran E <-> { C , A } e. ran E )
207	204, 198, 206	3anbi123i 1142	. . . . . . . 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 243	. . . . . . 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 938	. . . . . . . 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 941	. . . . . . . . 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 941	. . . . . . . . 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 228	. . . . . . . . . 10 |- ( { B , C } e. ran E <-> { B , C } e. ran E )
213	196, 212, 206	3anbi123i 1142	. . . . . . . . 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 263	. . . . . . . 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 243	. . . . . . 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 1142	. . . . . 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 938	. . . . . . 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 784	. . . . . . 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 626	. . . . . . 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 263	. . . . . 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 263	. . . . 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 245	. . 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 271	. 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 424	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 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E!wreu 2668   _Vcvv 2916   \ cdif 3277   C_ wss 3280   {csn 3774   {cpr 3775   {ctp 3776   class class class wbr 4172   ran crn 4838   USGrph cusg 21318   FriendGrph cfrgra 28092

This theorem is referenced by:  3vfriswmgra  28109

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-2 10014  df-n0 10178  df-z 10239  df-uz 10445  df-fz 11000  df-hash 11574  df-usgra 21320  df-frgra 28093