Theorem frgra3v 30741

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 23421	. . . . . 6 |- ( { A , B , C } USGrph E -> ( { A , B , C } e. _V /\ E e. _V ) )
2		isfrgra 30729	. . . . . 6 |- ( ( { A , B , C } e. _V /\ E e. _V ) -> ( { A , B , C } FriendGrph E <-> ( { A , B , C } USGrph E /\ A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E ) ) )
3	1, 2	syl 16	. . . . 5 |- ( { A , B , C } USGrph E -> ( { A , B , C } FriendGrph E <-> ( { A , B , C } USGrph E /\ A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E ) ) )
4	3	adantl 466	. . . 4 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( { A , B , C } FriendGrph E <-> ( { A , B , C } USGrph E /\ A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E ) ) )
5		ibar 504	. . . . 5 |- ( { A , B , C } USGrph E -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> ( { A , B , C } USGrph E /\ A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E ) ) )
6	5	adantl 466	. . . 4 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> ( { A , B , C } USGrph E /\ A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E ) ) )
7	4, 6	bitr4d 256	. . 3 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( { A , B , C } FriendGrph E <-> A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E ) )
8		sneq 3994	. . . . . . . . 9 |- ( k = A -> { k } = { A } )
9	8	difeq2d 3581	. . . . . . . 8 |- ( k = A -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { A } ) )
10		preq2 4062	. . . . . . . . . . 11 |- ( k = A -> { x , k } = { x , A } )
11	10	preq1d 4067	. . . . . . . . . 10 |- ( k = A -> { { x , k } , { x , l } } = { { x , A } , { x , l } } )
12	11	sseq1d 3490	. . . . . . . . 9 |- ( k = A -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , A } , { x , l } } C_ ran E ) )
13	12	reubidv 3009	. . . . . . . 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 3035	. . . . . . 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 3994	. . . . . . . . 9 |- ( k = B -> { k } = { B } )
16	15	difeq2d 3581	. . . . . . . 8 |- ( k = B -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { B } ) )
17		preq2 4062	. . . . . . . . . . 11 |- ( k = B -> { x , k } = { x , B } )
18	17	preq1d 4067	. . . . . . . . . 10 |- ( k = B -> { { x , k } , { x , l } } = { { x , B } , { x , l } } )
19	18	sseq1d 3490	. . . . . . . . 9 |- ( k = B -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , B } , { x , l } } C_ ran E ) )
20	19	reubidv 3009	. . . . . . . 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 3035	. . . . . . 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 3994	. . . . . . . . 9 |- ( k = C -> { k } = { C } )
23	22	difeq2d 3581	. . . . . . . 8 |- ( k = C -> ( { A , B , C } \ { k } ) = ( { A , B , C } \ { C } ) )
24		preq2 4062	. . . . . . . . . . 11 |- ( k = C -> { x , k } = { x , C } )
25	24	preq1d 4067	. . . . . . . . . 10 |- ( k = C -> { { x , k } , { x , l } } = { { x , C } , { x , l } } )
26	25	sseq1d 3490	. . . . . . . . 9 |- ( k = C -> ( { { x , k } , { x , l } } C_ ran E <-> { { x , C } , { x , l } } C_ ran E ) )
27	26	reubidv 3009	. . . . . . . 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 3035	. . . . . . 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 4034	. . . . . 6 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) ) )
30	29	adantr 465	. . . . 5 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) ) )
31	30	adantr 465	. . . 4 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) ) )
32		tprot 4077	. . . . . . . . . . 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 3580	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = ( { B , C , A } \ { A } ) )
35		necom 2720	. . . . . . . . . . . . 13 |- ( A =/= B <-> B =/= A )
36	35	biimpi 194	. . . . . . . . . . . 12 |- ( A =/= B -> B =/= A )
37		necom 2720	. . . . . . . . . . . . 13 |- ( A =/= C <-> C =/= A )
38	37	biimpi 194	. . . . . . . . . . . 12 |- ( A =/= C -> C =/= A )
39	36, 38	anim12i 566	. . . . . . . . . . 11 |- ( ( A =/= B /\ A =/= C ) -> ( B =/= A /\ C =/= A ) )
40	39	3adant3 1008	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( B =/= A /\ C =/= A ) )
41		diftpsn3 4119	. . . . . . . . . 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 2495	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { A } ) = { B , C } )
44	43	raleqdv 3027	. . . . . . 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 4077	. . . . . . . . . . . 12 |- { C , A , B } = { A , B , C }
46	45	eqcomi 2467	. . . . . . . . . . 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 3580	. . . . . . . . 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 2720	. . . . . . . . . . . . 13 |- ( B =/= C <-> C =/= B )
51	50	biimpi 194	. . . . . . . . . . . 12 |- ( B =/= C -> C =/= B )
52	49, 51	anim12ci 567	. . . . . . . . . . 11 |- ( ( A =/= B /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
53	52	3adant2 1007	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= B /\ A =/= B ) )
54		diftpsn3 4119	. . . . . . . . . 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 2495	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { B } ) = { C , A } )
57	56	raleqdv 3027	. . . . . . 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 4119	. . . . . . . . 9 |- ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
59	58	3adant1 1006	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
60	59	raleqdv 3027	. . . . . . 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 1290	. . . . . 6 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) <-> ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) ) )
62	61	adantl 466	. . . . 5 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) <-> ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) ) )
63	62	adantr 465	. . . 4 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( A. l e. ( { A , B , C } \ { A } ) E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { B } ) E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. ( { A , B , C } \ { C } ) E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) <-> ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) ) )
64		preq2 4062	. . . . . . . . . . . 12 |- ( l = B -> { x , l } = { x , B } )
65	64	preq2d 4068	. . . . . . . . . . 11 |- ( l = B -> { { x , A } , { x , l } } = { { x , A } , { x , B } } )
66	65	sseq1d 3490	. . . . . . . . . 10 |- ( l = B -> ( { { x , A } , { x , l } } C_ ran E <-> { { x , A } , { x , B } } C_ ran E ) )
67	66	reubidv 3009	. . . . . . . . 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 4062	. . . . . . . . . . . 12 |- ( l = C -> { x , l } = { x , C } )
69	68	preq2d 4068	. . . . . . . . . . 11 |- ( l = C -> { { x , A } , { x , l } } = { { x , A } , { x , C } } )
70	69	sseq1d 3490	. . . . . . . . . 10 |- ( l = C -> ( { { x , A } , { x , l } } C_ ran E <-> { { x , A } , { x , C } } C_ ran E ) )
71	70	reubidv 3009	. . . . . . . . 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 4032	. . . . . . . 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 1006	. . . . . . 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 4068	. . . . . . . . . . . 12 |- ( l = C -> { { x , B } , { x , l } } = { { x , B } , { x , C } } )
75	74	sseq1d 3490	. . . . . . . . . . 11 |- ( l = C -> ( { { x , B } , { x , l } } C_ ran E <-> { { x , B } , { x , C } } C_ ran E ) )
76	75	reubidv 3009	. . . . . . . . . 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 4062	. . . . . . . . . . . . 13 |- ( l = A -> { x , l } = { x , A } )
78	77	preq2d 4068	. . . . . . . . . . . 12 |- ( l = A -> { { x , B } , { x , l } } = { { x , B } , { x , A } } )
79	78	sseq1d 3490	. . . . . . . . . . 11 |- ( l = A -> ( { { x , B } , { x , l } } C_ ran E <-> { { x , B } , { x , A } } C_ ran E ) )
80	79	reubidv 3009	. . . . . . . . . 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 4032	. . . . . . . . 9 |- ( ( C e. Z /\ A e. X ) -> ( A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E <-> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) ) )
82	81	ancoms 453	. . . . . . . 8 |- ( ( A e. X /\ C e. Z ) -> ( A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E <-> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) ) )
83	82	3adant2 1007	. . . . . . 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 4068	. . . . . . . . . . 11 |- ( l = A -> { { x , C } , { x , l } } = { { x , C } , { x , A } } )
85	84	sseq1d 3490	. . . . . . . . . 10 |- ( l = A -> ( { { x , C } , { x , l } } C_ ran E <-> { { x , C } , { x , A } } C_ ran E ) )
86	85	reubidv 3009	. . . . . . . . 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 4068	. . . . . . . . . . 11 |- ( l = B -> { { x , C } , { x , l } } = { { x , C } , { x , B } } )
88	87	sseq1d 3490	. . . . . . . . . 10 |- ( l = B -> ( { { x , C } , { x , l } } C_ ran E <-> { { x , C } , { x , B } } C_ ran E ) )
89	88	reubidv 3009	. . . . . . . . 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 4032	. . . . . . . 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 1008	. . . . . . 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 1290	. . . . . 6 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) <-> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) ) ) )
93	92	adantr 465	. . . . 5 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) <-> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) ) ) )
94	93	adantr 465	. . . 4 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( A. l e. { B , C } E! x e. { A , B , C } { { x , A } , { x , l } } C_ ran E /\ A. l e. { C , A } E! x e. { A , B , C } { { x , B } , { x , l } } C_ ran E /\ A. l e. { A , B } E! x e. { A , B , C } { { x , C } , { x , l } } C_ ran E ) <-> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) ) ) )
95	31, 63, 94	3bitrd 279	. . 3 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( A. k e. { A , B , C } A. l e. ( { A , B , C } \ { k } ) E! x e. { A , B , C } { { x , k } , { x , l } } C_ ran E <-> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) ) ) )
96		frgra3vlem2 30740	. . . . . . 7 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( { A , B , C } USGrph E -> ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E <-> ( { C , A } e. ran E /\ { C , B } e. ran E ) ) ) )
97	96	imp 429	. . . . . 6 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E <-> ( { C , A } e. ran E /\ { C , B } e. ran E ) ) )
98		3ancomb 974	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( A e. X /\ C e. Z /\ B e. Y ) )
99		3ancoma 972	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ B =/= C ) )
100		biid 236	. . . . . . . . . 10 |- ( A =/= C <-> A =/= C )
101		biid 236	. . . . . . . . . 10 |- ( A =/= B <-> A =/= B )
102	100, 101, 50	3anbi123i 1177	. . . . . . . . 9 |- ( ( A =/= C /\ A =/= B /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ C =/= B ) )
103	99, 102	bitri 249	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ A =/= B /\ C =/= B ) )
104	98, 103	anbi12i 697	. . . . . . 7 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) <-> ( ( A e. X /\ C e. Z /\ B e. Y ) /\ ( A =/= C /\ A =/= B /\ C =/= B ) ) )
105		tpcomb 4079	. . . . . . . 8 |- { A , B , C } = { A , C , B }
106	105	breq1i 4406	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { A , C , B } USGrph E )
107		reueq1 3023	. . . . . . . . 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 30740	. . . . . . . . 9 |- ( ( ( A e. X /\ C e. Z /\ B e. Y ) /\ ( A =/= C /\ A =/= B /\ C =/= B ) ) -> ( { A , C , B } USGrph E -> ( E! x e. { A , C , B } { { x , A } , { x , C } } C_ ran E <-> ( { B , A } e. ran E /\ { B , C } e. ran E ) ) ) )
110	109	imp 429	. . . . . . . 8 |- ( ( ( ( A e. X /\ C e. Z /\ B e. Y ) /\ ( A =/= C /\ A =/= B /\ C =/= B ) ) /\ { A , C , B } USGrph E ) -> ( E! x e. { A , C , B } { { x , A } , { x , C } } C_ ran E <-> ( { B , A } e. ran E /\ { B , C } e. ran E ) ) )
111	108, 110	bitrd 253	. . . . . . 7 |- ( ( ( ( A e. X /\ C e. Z /\ B e. Y ) /\ ( A =/= C /\ A =/= B /\ C =/= B ) ) /\ { A , C , B } USGrph E ) -> ( E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E <-> ( { B , A } e. ran E /\ { B , C } e. ran E ) ) )
112	104, 106, 111	syl2anb 479	. . . . . 6 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E <-> ( { B , A } e. ran E /\ { B , C } e. ran E ) ) )
113	97, 112	anbi12d 710	. . . . 5 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) <-> ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { B , C } e. ran E ) ) ) )
114		3anrot 970	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ C e. Z /\ A e. X ) )
115		3anrot 970	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= B /\ A =/= C ) <-> ( A =/= B /\ A =/= C /\ B =/= C ) )
116		biid 236	. . . . . . . . . 10 |- ( B =/= C <-> B =/= C )
117	116, 35, 37	3anbi123i 1177	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= B /\ A =/= C ) <-> ( B =/= C /\ B =/= A /\ C =/= A ) )
118	115, 117	bitr3i 251	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( B =/= C /\ B =/= A /\ C =/= A ) )
119	114, 118	anbi12i 697	. . . . . . 7 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) <-> ( ( B e. Y /\ C e. Z /\ A e. X ) /\ ( B =/= C /\ B =/= A /\ C =/= A ) ) )
120	32	breq1i 4406	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { B , C , A } USGrph E )
121		reueq1 3023	. . . . . . . . 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 30740	. . . . . . . . 9 |- ( ( ( B e. Y /\ C e. Z /\ A e. X ) /\ ( B =/= C /\ B =/= A /\ C =/= A ) ) -> ( { B , C , A } USGrph E -> ( E! x e. { B , C , A } { { x , B } , { x , C } } C_ ran E <-> ( { A , B } e. ran E /\ { A , C } e. ran E ) ) ) )
124	123	imp 429	. . . . . . . 8 |- ( ( ( ( B e. Y /\ C e. Z /\ A e. X ) /\ ( B =/= C /\ B =/= A /\ C =/= A ) ) /\ { B , C , A } USGrph E ) -> ( E! x e. { B , C , A } { { x , B } , { x , C } } C_ ran E <-> ( { A , B } e. ran E /\ { A , C } e. ran E ) ) )
125	122, 124	bitrd 253	. . . . . . 7 |- ( ( ( ( B e. Y /\ C e. Z /\ A e. X ) /\ ( B =/= C /\ B =/= A /\ C =/= A ) ) /\ { B , C , A } USGrph E ) -> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E <-> ( { A , B } e. ran E /\ { A , C } e. ran E ) ) )
126	119, 120, 125	syl2anb 479	. . . . . 6 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E <-> ( { A , B } e. ran E /\ { A , C } e. ran E ) ) )
127		3ancoma 972	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( B e. Y /\ A e. X /\ C e. Z ) )
128		3ancomb 974	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= B /\ B =/= C /\ A =/= C ) )
129	35, 116, 100	3anbi123i 1177	. . . . . . . . 9 |- ( ( A =/= B /\ B =/= C /\ A =/= C ) <-> ( B =/= A /\ B =/= C /\ A =/= C ) )
130	128, 129	bitri 249	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( B =/= A /\ B =/= C /\ A =/= C ) )
131	127, 130	anbi12i 697	. . . . . . 7 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) <-> ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( B =/= A /\ B =/= C /\ A =/= C ) ) )
132		tpcoma 4078	. . . . . . . 8 |- { A , B , C } = { B , A , C }
133	132	breq1i 4406	. . . . . . 7 |- ( { A , B , C } USGrph E <-> { B , A , C } USGrph E )
134		reueq1 3023	. . . . . . . . 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 30740	. . . . . . . . 9 |- ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( B =/= A /\ B =/= C /\ A =/= C ) ) -> ( { B , A , C } USGrph E -> ( E! x e. { B , A , C } { { x , B } , { x , A } } C_ ran E <-> ( { C , B } e. ran E /\ { C , A } e. ran E ) ) ) )
137	136	imp 429	. . . . . . . 8 |- ( ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( B =/= A /\ B =/= C /\ A =/= C ) ) /\ { B , A , C } USGrph E ) -> ( E! x e. { B , A , C } { { x , B } , { x , A } } C_ ran E <-> ( { C , B } e. ran E /\ { C , A } e. ran E ) ) )
138	135, 137	bitrd 253	. . . . . . 7 |- ( ( ( ( B e. Y /\ A e. X /\ C e. Z ) /\ ( B =/= A /\ B =/= C /\ A =/= C ) ) /\ { B , A , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E <-> ( { C , B } e. ran E /\ { C , A } e. ran E ) ) )
139	131, 133, 138	syl2anb 479	. . . . . 6 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E <-> ( { C , B } e. ran E /\ { C , A } e. ran E ) ) )
140	126, 139	anbi12d 710	. . . . 5 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) <-> ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { C , A } e. ran E ) ) ) )
141		3anrot 970	. . . . . . . . 9 |- ( ( C e. Z /\ A e. X /\ B e. Y ) <-> ( A e. X /\ B e. Y /\ C e. Z ) )
142	141	biimpri 206	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( C e. Z /\ A e. X /\ B e. Y ) )
143		3anrot 970	. . . . . . . . . 10 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( A =/= C /\ B =/= C /\ A =/= B ) )
144	37, 50, 101	3anbi123i 1177	. . . . . . . . . 10 |- ( ( A =/= C /\ B =/= C /\ A =/= B ) <-> ( C =/= A /\ C =/= B /\ A =/= B ) )
145	143, 144	bitri 249	. . . . . . . . 9 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) <-> ( C =/= A /\ C =/= B /\ A =/= B ) )
146	145	biimpi 194	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= A /\ C =/= B /\ A =/= B ) )
147	142, 146	anim12i 566	. . . . . . 7 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( C =/= A /\ C =/= B /\ A =/= B ) ) )
148	46	breq1i 4406	. . . . . . . 8 |- ( { A , B , C } USGrph E <-> { C , A , B } USGrph E )
149	148	biimpi 194	. . . . . . 7 |- ( { A , B , C } USGrph E -> { C , A , B } USGrph E )
150		reueq1 3023	. . . . . . . . 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 30740	. . . . . . . . 9 |- ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( C =/= A /\ C =/= B /\ A =/= B ) ) -> ( { C , A , B } USGrph E -> ( E! x e. { C , A , B } { { x , C } , { x , A } } C_ ran E <-> ( { B , C } e. ran E /\ { B , A } e. ran E ) ) ) )
153	152	imp 429	. . . . . . . 8 |- ( ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( C =/= A /\ C =/= B /\ A =/= B ) ) /\ { C , A , B } USGrph E ) -> ( E! x e. { C , A , B } { { x , C } , { x , A } } C_ ran E <-> ( { B , C } e. ran E /\ { B , A } e. ran E ) ) )
154	151, 153	bitrd 253	. . . . . . 7 |- ( ( ( ( C e. Z /\ A e. X /\ B e. Y ) /\ ( C =/= A /\ C =/= B /\ A =/= B ) ) /\ { C , A , B } USGrph E ) -> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E <-> ( { B , C } e. ran E /\ { B , A } e. ran E ) ) )
155	147, 149, 154	syl2an 477	. . . . . 6 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E <-> ( { B , C } e. ran E /\ { B , A } e. ran E ) ) )
156		3anrev 976	. . . . . . . . 9 |- ( ( A e. X /\ B e. Y /\ C e. Z ) <-> ( C e. Z /\ B e. Y /\ A e. X ) )
157	156	biimpi 194	. . . . . . . 8 |- ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( C e. Z /\ B e. Y /\ A e. X ) )
158	50, 37, 35	3anbi123i 1177	. . . . . . . . . 10 |- ( ( B =/= C /\ A =/= C /\ A =/= B ) <-> ( C =/= B /\ C =/= A /\ B =/= A ) )
159	158	biimpi 194	. . . . . . . . 9 |- ( ( B =/= C /\ A =/= C /\ A =/= B ) -> ( C =/= B /\ C =/= A /\ B =/= A ) )
160	159	3com13 1193	. . . . . . . 8 |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( C =/= B /\ C =/= A /\ B =/= A ) )
161	157, 160	anim12i 566	. . . . . . 7 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) )
162		tpcoma 4078	. . . . . . . . . 10 |- { B , C , A } = { C , B , A }
163	32, 162	eqtri 2483	. . . . . . . . 9 |- { A , B , C } = { C , B , A }
164	163	breq1i 4406	. . . . . . . 8 |- ( { A , B , C } USGrph E <-> { C , B , A } USGrph E )
165	164	biimpi 194	. . . . . . 7 |- ( { A , B , C } USGrph E -> { C , B , A } USGrph E )
166		reueq1 3023	. . . . . . . . 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 30740	. . . . . . . . 9 |- ( ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) -> ( { C , B , A } USGrph E -> ( E! x e. { C , B , A } { { x , C } , { x , B } } C_ ran E <-> ( { A , C } e. ran E /\ { A , B } e. ran E ) ) ) )
169	168	imp 429	. . . . . . . 8 |- ( ( ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) /\ { C , B , A } USGrph E ) -> ( E! x e. { C , B , A } { { x , C } , { x , B } } C_ ran E <-> ( { A , C } e. ran E /\ { A , B } e. ran E ) ) )
170	167, 169	bitrd 253	. . . . . . 7 |- ( ( ( ( C e. Z /\ B e. Y /\ A e. X ) /\ ( C =/= B /\ C =/= A /\ B =/= A ) ) /\ { C , B , A } USGrph E ) -> ( E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E <-> ( { A , C } e. ran E /\ { A , B } e. ran E ) ) )
171	161, 165, 170	syl2an 477	. . . . . 6 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E <-> ( { A , C } e. ran E /\ { A , B } e. ran E ) ) )
172	155, 171	anbi12d 710	. . . . 5 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) <-> ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { A , B } e. ran E ) ) ) )
173	113, 140, 172	3anbi123d 1290	. . . 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 4060	. . . . . . . . . . 11 |- { B , C } = { C , B }
175	174	eleq1i 2531	. . . . . . . . . 10 |- ( { B , C } e. ran E <-> { C , B } e. ran E )
176	175	anbi2i 694	. . . . . . . . 9 |- ( ( { B , A } e. ran E /\ { B , C } e. ran E ) <-> ( { B , A } e. ran E /\ { C , B } e. ran E ) )
177	176	anbi2i 694	. . . . . . . 8 |- ( ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { B , C } e. ran E ) ) <-> ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { C , B } e. ran E ) ) )
178		anandir 825	. . . . . . . 8 |- ( ( ( { C , A } e. ran E /\ { B , A } e. ran E ) /\ { C , B } e. ran E ) <-> ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { C , B } e. ran E ) ) )
179	177, 178	bitr4i 252	. . . . . . 7 |- ( ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { B , C } e. ran E ) ) <-> ( ( { C , A } e. ran E /\ { B , A } e. ran E ) /\ { C , B } e. ran E ) )
180		prcom 4060	. . . . . . . . . . 11 |- { C , A } = { A , C }
181	180	eleq1i 2531	. . . . . . . . . 10 |- ( { C , A } e. ran E <-> { A , C } e. ran E )
182	181	anbi2i 694	. . . . . . . . 9 |- ( ( { C , B } e. ran E /\ { C , A } e. ran E ) <-> ( { C , B } e. ran E /\ { A , C } e. ran E ) )
183	182	anbi2i 694	. . . . . . . 8 |- ( ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { C , A } e. ran E ) ) <-> ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { A , C } e. ran E ) ) )
184		anandir 825	. . . . . . . 8 |- ( ( ( { A , B } e. ran E /\ { C , B } e. ran E ) /\ { A , C } e. ran E ) <-> ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { A , C } e. ran E ) ) )
185	183, 184	bitr4i 252	. . . . . . 7 |- ( ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { C , A } e. ran E ) ) <-> ( ( { A , B } e. ran E /\ { C , B } e. ran E ) /\ { A , C } e. ran E ) )
186		prcom 4060	. . . . . . . . . . 11 |- { A , B } = { B , A }
187	186	eleq1i 2531	. . . . . . . . . 10 |- ( { A , B } e. ran E <-> { B , A } e. ran E )
188	187	anbi2i 694	. . . . . . . . 9 |- ( ( { A , C } e. ran E /\ { A , B } e. ran E ) <-> ( { A , C } e. ran E /\ { B , A } e. ran E ) )
189	188	anbi2i 694	. . . . . . . 8 |- ( ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { A , B } e. ran E ) ) <-> ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { B , A } e. ran E ) ) )
190		anandir 825	. . . . . . . 8 |- ( ( ( { B , C } e. ran E /\ { A , C } e. ran E ) /\ { B , A } e. ran E ) <-> ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { B , A } e. ran E ) ) )
191	189, 190	bitr4i 252	. . . . . . 7 |- ( ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { A , B } e. ran E ) ) <-> ( ( { B , C } e. ran E /\ { A , C } e. ran E ) /\ { B , A } e. ran E ) )
192	179, 185, 191	3anbi123i 1177	. . . . . 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 967	. . . . . . . 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 970	. . . . . . . . 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 4060	. . . . . . . . . . 11 |- { B , A } = { A , B }
196	195	eleq1i 2531	. . . . . . . . . 10 |- ( { B , A } e. ran E <-> { A , B } e. ran E )
197		prcom 4060	. . . . . . . . . . 11 |- { C , B } = { B , C }
198	197	eleq1i 2531	. . . . . . . . . 10 |- ( { C , B } e. ran E <-> { B , C } e. ran E )
199		biid 236	. . . . . . . . . 10 |- ( { C , A } e. ran E <-> { C , A } e. ran E )
200	196, 198, 199	3anbi123i 1177	. . . . . . . . 9 |- ( ( { B , A } e. ran E /\ { C , B } e. ran E /\ { C , A } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
201	194, 200	bitri 249	. . . . . . . 8 |- ( ( { C , A } e. ran E /\ { B , A } e. ran E /\ { C , B } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
202	193, 201	bitr3i 251	. . . . . . 7 |- ( ( ( { C , A } e. ran E /\ { B , A } e. ran E ) /\ { C , B } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
203		df-3an 967	. . . . . . . 8 |- ( ( { A , B } e. ran E /\ { C , B } e. ran E /\ { A , C } e. ran E ) <-> ( ( { A , B } e. ran E /\ { C , B } e. ran E ) /\ { A , C } e. ran E ) )
204		biid 236	. . . . . . . . 9 |- ( { A , B } e. ran E <-> { A , B } e. ran E )
205		prcom 4060	. . . . . . . . . 10 |- { A , C } = { C , A }
206	205	eleq1i 2531	. . . . . . . . 9 |- ( { A , C } e. ran E <-> { C , A } e. ran E )
207	204, 198, 206	3anbi123i 1177	. . . . . . . 8 |- ( ( { A , B } e. ran E /\ { C , B } e. ran E /\ { A , C } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
208	203, 207	bitr3i 251	. . . . . . 7 |- ( ( ( { A , B } e. ran E /\ { C , B } e. ran E ) /\ { A , C } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
209		df-3an 967	. . . . . . . 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 970	. . . . . . . . 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 970	. . . . . . . . 9 |- ( ( { A , C } e. ran E /\ { B , A } e. ran E /\ { B , C } e. ran E ) <-> ( { B , A } e. ran E /\ { B , C } e. ran E /\ { A , C } e. ran E ) )
212		biid 236	. . . . . . . . . 10 |- ( { B , C } e. ran E <-> { B , C } e. ran E )
213	196, 212, 206	3anbi123i 1177	. . . . . . . . 9 |- ( ( { B , A } e. ran E /\ { B , C } e. ran E /\ { A , C } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
214	210, 211, 213	3bitri 271	. . . . . . . 8 |- ( ( { B , C } e. ran E /\ { A , C } e. ran E /\ { B , A } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
215	209, 214	bitr3i 251	. . . . . . 7 |- ( ( ( { B , C } e. ran E /\ { A , C } e. ran E ) /\ { B , A } e. ran E ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
216	202, 208, 215	3anbi123i 1177	. . . . . 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 967	. . . . . . 7 |- ( ( ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) <-> ( ( ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) )
218		anabs1 806	. . . . . . 7 |- ( ( ( ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) <-> ( ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) )
219		anidm 644	. . . . . . 7 |- ( ( ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
220	217, 218, 219	3bitri 271	. . . . . 6 |- ( ( ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
221	192, 216, 220	3bitri 271	. . . . 5 |- ( ( ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { B , C } e. ran E ) ) /\ ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { C , A } e. ran E ) ) /\ ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { A , B } e. ran E ) ) ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) )
222	221	a1i 11	. . . 4 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( ( ( { C , A } e. ran E /\ { C , B } e. ran E ) /\ ( { B , A } e. ran E /\ { B , C } e. ran E ) ) /\ ( ( { A , B } e. ran E /\ { A , C } e. ran E ) /\ ( { C , B } e. ran E /\ { C , A } e. ran E ) ) /\ ( ( { B , C } e. ran E /\ { B , A } e. ran E ) /\ ( { A , C } e. ran E /\ { A , B } e. ran E ) ) ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) )
223	173, 222	bitrd 253	. . 3 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( ( ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ ran E /\ E! x e. { A , B , C } { { x , A } , { x , C } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , B } , { x , C } } C_ ran E /\ E! x e. { A , B , C } { { x , B } , { x , A } } C_ ran E ) /\ ( E! x e. { A , B , C } { { x , C } , { x , A } } C_ ran E /\ E! x e. { A , B , C } { { x , C } , { x , B } } C_ ran E ) ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) )
224	7, 95, 223	3bitrd 279	. 2 |- ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ { A , B , C } USGrph E ) -> ( { A , B , C } FriendGrph E <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) )
225	224	ex 434	1 |- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( { A , B , C } USGrph E -> ( { A , B , C } FriendGrph E <-> ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1758   =/= wne 2647   A.wral 2798   E!wreu 2800   _Vcvv 3076   \ cdif 3432   C_ wss 3435   {csn 3984   {cpr 3986   {ctp 3988   class class class wbr 4399   ran crn 4948   USGrph cusg 23415   FriendGrph cfrgra 30727

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4510  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-cnex 9448  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-mulcom 9456  ax-addass 9457  ax-mulass 9458  ax-distr 9459  ax-i2m1 9460  ax-1ne0 9461  ax-1rid 9462  ax-rnegex 9463  ax-rrecex 9464  ax-cnre 9465  ax-pre-lttri 9466  ax-pre-lttrn 9467  ax-pre-ltadd 9468  ax-pre-mulgt0 9469

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-nel 2650  df-ral 2803  df-rex 2804  df-reu 2805  df-rmo 2806  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-int 4236  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-riota 6160  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-om 6586  df-1st 6686  df-2nd 6687  df-recs 6941  df-rdg 6975  df-1o 7029  df-oadd 7033  df-er 7210  df-en 7420  df-dom 7421  df-sdom 7422  df-fin 7423  df-card 8219  df-cda 8447  df-pnf 9530  df-mnf 9531  df-xr 9532  df-ltxr 9533  df-le 9534  df-sub 9707  df-neg 9708  df-nn 10433  df-2 10490  df-n0 10690  df-z 10757  df-uz 10972  df-fz 11554  df-hash 12220  df-usgra 23417  df-frgra 30728

This theorem is referenced by:  3vfriswmgra  30744