Theorem frgr3v 29517

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.) (Revised by AV, 29-Mar-2021.)

Hypotheses

Ref	Expression
frgr3v.v	⊢ 𝑉 = (Vtx‘𝐺)
frgr3v.e	⊢ 𝐸 = (Edg‘𝐺)

Assertion

Ref	Expression
frgr3v	⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))

Proof of Theorem frgr3v

Dummy variables 𝑘 𝑙 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frgr3v.v	. . . . . 6 ⊢ 𝑉 = (Vtx‘𝐺)
2		frgr3v.e	. . . . . 6 ⊢ 𝐸 = (Edg‘𝐺)
3	1, 2	isfrgr 29502	. . . . 5 ⊢ (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
4	3	a1i 11	. . . 4 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)))
5		id 22	. . . . . . . 8 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐴, 𝐵, 𝐶})
6		difeq1 4114	. . . . . . . . 9 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑘}))
7		reueq1 3415	. . . . . . . . 9 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
8	6, 7	raleqbidv 3342	. . . . . . . 8 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
9	5, 8	raleqbidv 3342	. . . . . . 7 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
10	9	anbi2d 629	. . . . . 6 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → ((𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)))
11	10	baibd 540	. . . . 5 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → ((𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
12	11	adantl 482	. . . 4 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
13	4, 12	bitrd 278	. . 3 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐺 ∈ FriendGraph ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
14		sneq 4637	. . . . . . . 8 ⊢ (𝑘 = 𝐴 → {𝑘} = {𝐴})
15	14	difeq2d 4121	. . . . . . 7 ⊢ (𝑘 = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}))
16		preq2 4737	. . . . . . . . . 10 ⊢ (𝑘 = 𝐴 → {𝑥, 𝑘} = {𝑥, 𝐴})
17	16	preq1d 4742	. . . . . . . . 9 ⊢ (𝑘 = 𝐴 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝑙}})
18	17	sseq1d 4012	. . . . . . . 8 ⊢ (𝑘 = 𝐴 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
19	18	reubidv 3394	. . . . . . 7 ⊢ (𝑘 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
20	15, 19	raleqbidv 3342	. . . . . 6 ⊢ (𝑘 = 𝐴 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
21		sneq 4637	. . . . . . . 8 ⊢ (𝑘 = 𝐵 → {𝑘} = {𝐵})
22	21	difeq2d 4121	. . . . . . 7 ⊢ (𝑘 = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}))
23		preq2 4737	. . . . . . . . . 10 ⊢ (𝑘 = 𝐵 → {𝑥, 𝑘} = {𝑥, 𝐵})
24	23	preq1d 4742	. . . . . . . . 9 ⊢ (𝑘 = 𝐵 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝑙}})
25	24	sseq1d 4012	. . . . . . . 8 ⊢ (𝑘 = 𝐵 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
26	25	reubidv 3394	. . . . . . 7 ⊢ (𝑘 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
27	22, 26	raleqbidv 3342	. . . . . 6 ⊢ (𝑘 = 𝐵 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
28		sneq 4637	. . . . . . . 8 ⊢ (𝑘 = 𝐶 → {𝑘} = {𝐶})
29	28	difeq2d 4121	. . . . . . 7 ⊢ (𝑘 = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}))
30		preq2 4737	. . . . . . . . . 10 ⊢ (𝑘 = 𝐶 → {𝑥, 𝑘} = {𝑥, 𝐶})
31	30	preq1d 4742	. . . . . . . . 9 ⊢ (𝑘 = 𝐶 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝑙}})
32	31	sseq1d 4012	. . . . . . . 8 ⊢ (𝑘 = 𝐶 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
33	32	reubidv 3394	. . . . . . 7 ⊢ (𝑘 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
34	29, 33	raleqbidv 3342	. . . . . 6 ⊢ (𝑘 = 𝐶 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
35	20, 27, 34	raltpg 4701	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
36	35	ad2antrr 724	. . . 4 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
37		tprot 4752	. . . . . . . . . 10 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
38	37	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴})
39	38	difeq1d 4120	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = ({𝐵, 𝐶, 𝐴} ∖ {𝐴}))
40		necom 2994	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
41	40	biimpi 215	. . . . . . . . . . 11 ⊢ (𝐴 ≠ 𝐵 → 𝐵 ≠ 𝐴)
42		necom 2994	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴)
43	42	biimpi 215	. . . . . . . . . . 11 ⊢ (𝐴 ≠ 𝐶 → 𝐶 ≠ 𝐴)
44	41, 43	anim12i 613	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → (𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴))
45	44	3adant3 1132	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴))
46		diftpsn3 4804	. . . . . . . . 9 ⊢ ((𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
47	45, 46	syl 17	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
48	39, 47	eqtrd 2772	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶})
49	48	raleqdv 3325	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
50		tprot 4752	. . . . . . . . . . 11 ⊢ {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶}
51	50	eqcomi 2741	. . . . . . . . . 10 ⊢ {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵}
52	51	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵})
53	52	difeq1d 4120	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = ({𝐶, 𝐴, 𝐵} ∖ {𝐵}))
54		id 22	. . . . . . . . . . 11 ⊢ (𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵)
55		necom 2994	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵)
56	55	biimpi 215	. . . . . . . . . . 11 ⊢ (𝐵 ≠ 𝐶 → 𝐶 ≠ 𝐵)
57	54, 56	anim12ci 614	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
58	57	3adant2 1131	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
59		diftpsn3 4804	. . . . . . . . 9 ⊢ ((𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
60	58, 59	syl 17	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
61	53, 60	eqtrd 2772	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐶, 𝐴})
62	61	raleqdv 3325	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
63		diftpsn3 4804	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
64	63	3adant1 1130	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
65	64	raleqdv 3325	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
66	49, 62, 65	3anbi123d 1436	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ((∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
67	66	ad2antlr 725	. . . 4 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
68		preq2 4737	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐵 → {𝑥, 𝑙} = {𝑥, 𝐵})
69	68	preq2d 4743	. . . . . . . . . 10 ⊢ (𝑙 = 𝐵 → {{𝑥, 𝐴}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝐵}})
70	69	sseq1d 4012	. . . . . . . . 9 ⊢ (𝑙 = 𝐵 → ({{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸))
71	70	reubidv 3394	. . . . . . . 8 ⊢ (𝑙 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸))
72		preq2 4737	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐶 → {𝑥, 𝑙} = {𝑥, 𝐶})
73	72	preq2d 4743	. . . . . . . . . 10 ⊢ (𝑙 = 𝐶 → {{𝑥, 𝐴}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝐶}})
74	73	sseq1d 4012	. . . . . . . . 9 ⊢ (𝑙 = 𝐶 → ({{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
75	74	reubidv 3394	. . . . . . . 8 ⊢ (𝑙 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
76	71, 75	ralprg 4697	. . . . . . 7 ⊢ ((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸)))
77	76	3adant1 1130	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸)))
78	72	preq2d 4743	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐶 → {{𝑥, 𝐵}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝐶}})
79	78	sseq1d 4012	. . . . . . . . . 10 ⊢ (𝑙 = 𝐶 → ({{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
80	79	reubidv 3394	. . . . . . . . 9 ⊢ (𝑙 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
81		preq2 4737	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝐴 → {𝑥, 𝑙} = {𝑥, 𝐴})
82	81	preq2d 4743	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐴 → {{𝑥, 𝐵}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝐴}})
83	82	sseq1d 4012	. . . . . . . . . 10 ⊢ (𝑙 = 𝐴 → ({{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
84	83	reubidv 3394	. . . . . . . . 9 ⊢ (𝑙 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
85	80, 84	ralprg 4697	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸)))
86	85	ancoms 459	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸)))
87	86	3adant2 1131	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸)))
88	81	preq2d 4743	. . . . . . . . . 10 ⊢ (𝑙 = 𝐴 → {{𝑥, 𝐶}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝐴}})
89	88	sseq1d 4012	. . . . . . . . 9 ⊢ (𝑙 = 𝐴 → ({{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
90	89	reubidv 3394	. . . . . . . 8 ⊢ (𝑙 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
91	68	preq2d 4743	. . . . . . . . . 10 ⊢ (𝑙 = 𝐵 → {{𝑥, 𝐶}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝐵}})
92	91	sseq1d 4012	. . . . . . . . 9 ⊢ (𝑙 = 𝐵 → ({{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
93	92	reubidv 3394	. . . . . . . 8 ⊢ (𝑙 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
94	90, 93	ralprg 4697	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)))
95	94	3adant3 1132	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)))
96	77, 87, 95	3anbi123d 1436	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))))
97	96	ad2antrr 724	. . . 4 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))))
98	36, 67, 97	3bitrd 304	. . 3 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))))
99	1, 2	frgr3vlem2 29516	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))))
100	99	imp 407	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))
101		simpll1 1212	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐴 ∈ 𝑋)
102		simpll3 1214	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐶 ∈ 𝑍)
103		simpll2 1213	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐵 ∈ 𝑌)
104	101, 102, 103	3jca 1128	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌))
105		simplr2 1216	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐴 ≠ 𝐶)
106		simplr1 1215	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐴 ≠ 𝐵)
107	58	simpld 495	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → 𝐶 ≠ 𝐵)
108	107	ad2antlr 725	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐶 ≠ 𝐵)
109	105, 106, 108	3jca 1128	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵))
110		tpcomb 4754	. . . . . . . . . 10 ⊢ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵}
111	5, 110	eqtrdi 2788	. . . . . . . . 9 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐴, 𝐶, 𝐵})
112	111	anim1i 615	. . . . . . . 8 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph))
113	112	adantl 482	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph))
114		reueq1 3415	. . . . . . . . 9 ⊢ ({𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
115	110, 114	mp1i 13	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌) ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵)) ∧ (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
116	1, 2	frgr3vlem2 29516	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌) ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵)) → ((𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))))
117	116	imp 407	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌) ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵)) ∧ (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
118	115, 117	bitrd 278	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌) ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵)) ∧ (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
119	104, 109, 113, 118	syl21anc 836	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
120	100, 119	anbi12d 631	. . . . 5 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))))
121	103, 102, 101	3jca 1128	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋))
122		simplr3 1217	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐵 ≠ 𝐶)
123	106	necomd 2996	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐵 ≠ 𝐴)
124	105	necomd 2996	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐶 ≠ 𝐴)
125	122, 123, 124	3jca 1128	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴))
126	37	eqeq2i 2745	. . . . . . . . . 10 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐵, 𝐶, 𝐴})
127	126	biimpi 215	. . . . . . . . 9 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐵, 𝐶, 𝐴})
128	127	anim1i 615	. . . . . . . 8 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph))
129	128	adantl 482	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph))
130		reueq1 3415	. . . . . . . . 9 ⊢ ({𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
131	37, 130	mp1i 13	. . . . . . . 8 ⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴)) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
132	1, 2	frgr3vlem2 29516	. . . . . . . . 9 ⊢ (((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴)) → ((𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))))
133	132	imp 407	. . . . . . . 8 ⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴)) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
134	131, 133	bitrd 278	. . . . . . 7 ⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴)) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
135	121, 125, 129, 134	syl21anc 836	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
136	103, 101, 102	3jca 1128	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍))
137	123, 122, 105	3jca 1128	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶))
138		tpcoma 4753	. . . . . . . . . . 11 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶}
139	138	eqeq2i 2745	. . . . . . . . . 10 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐵, 𝐴, 𝐶})
140	139	biimpi 215	. . . . . . . . 9 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐵, 𝐴, 𝐶})
141	140	anim1i 615	. . . . . . . 8 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph))
142	141	adantl 482	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph))
143		reueq1 3415	. . . . . . . . 9 ⊢ ({𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
144	138, 143	mp1i 13	. . . . . . . 8 ⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) ∧ (𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
145	1, 2	frgr3vlem2 29516	. . . . . . . . 9 ⊢ (((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) ∧ (𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)) → ((𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))
146	145	imp 407	. . . . . . . 8 ⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) ∧ (𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
147	144, 146	bitrd 278	. . . . . . 7 ⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) ∧ (𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
148	136, 137, 142, 147	syl21anc 836	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
149	135, 148	anbi12d 631	. . . . 5 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))
150	102, 101, 103	3jca 1128	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌))
151	124, 108, 106	3jca 1128	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))
152	51	eqeq2i 2745	. . . . . . . . . 10 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐶, 𝐴, 𝐵})
153	152	biimpi 215	. . . . . . . . 9 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐶, 𝐴, 𝐵})
154	153	anim1i 615	. . . . . . . 8 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph))
155	154	adantl 482	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph))
156		reueq1 3415	. . . . . . . . 9 ⊢ ({𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
157	51, 156	mp1i 13	. . . . . . . 8 ⊢ ((((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
158	1, 2	frgr3vlem2 29516	. . . . . . . . 9 ⊢ (((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) → ((𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸))))
159	158	imp 407	. . . . . . . 8 ⊢ ((((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
160	157, 159	bitrd 278	. . . . . . 7 ⊢ ((((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
161	150, 151, 155, 160	syl21anc 836	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
162		3anrev 1101	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ↔ (𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋))
163	162	biimpi 215	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋))
164	55, 42, 40	3anbi123i 1155	. . . . . . . . . 10 ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) ↔ (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴))
165	164	biimpi 215	. . . . . . . . 9 ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) → (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴))
166	165	3com13 1124	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴))
167	163, 166	anim12i 613	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴)))
168		tpcoma 4753	. . . . . . . . . . 11 ⊢ {𝐵, 𝐶, 𝐴} = {𝐶, 𝐵, 𝐴}
169	37, 168	eqtri 2760	. . . . . . . . . 10 ⊢ {𝐴, 𝐵, 𝐶} = {𝐶, 𝐵, 𝐴}
170	169	eqeq2i 2745	. . . . . . . . 9 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐶, 𝐵, 𝐴})
171	170	biimpi 215	. . . . . . . 8 ⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐶, 𝐵, 𝐴})
172	171	anim1i 615	. . . . . . 7 ⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph))
173		reueq1 3415	. . . . . . . . 9 ⊢ ({𝐴, 𝐵, 𝐶} = {𝐶, 𝐵, 𝐴} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
174	169, 173	mp1i 13	. . . . . . . 8 ⊢ ((((𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴)) ∧ (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
175	1, 2	frgr3vlem2 29516	. . . . . . . . 9 ⊢ (((𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴)) → ((𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))))
176	175	imp 407	. . . . . . . 8 ⊢ ((((𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴)) ∧ (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))
177	174, 176	bitrd 278	. . . . . . 7 ⊢ ((((𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ (𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴)) ∧ (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))
178	167, 172, 177	syl2an 596	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))
179	161, 178	anbi12d 631	. . . . 5 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))))
180	120, 149, 179	3anbi123d 1436	. . . 4 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)) ↔ ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))))
181		prcom 4735	. . . . . . . . . 10 ⊢ {𝐵, 𝐶} = {𝐶, 𝐵}
182	181	eleq1i 2824	. . . . . . . . 9 ⊢ ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐶, 𝐵} ∈ 𝐸)
183	182	anbi2i 623	. . . . . . . 8 ⊢ (({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))
184	183	anbi2i 623	. . . . . . 7 ⊢ ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))
185		anandir 675	. . . . . . 7 ⊢ ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))
186	184, 185	bitr4i 277	. . . . . 6 ⊢ ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸))
187		prcom 4735	. . . . . . . . . 10 ⊢ {𝐶, 𝐴} = {𝐴, 𝐶}
188	187	eleq1i 2824	. . . . . . . . 9 ⊢ ({𝐶, 𝐴} ∈ 𝐸 ↔ {𝐴, 𝐶} ∈ 𝐸)
189	188	anbi2i 623	. . . . . . . 8 ⊢ (({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))
190	189	anbi2i 623	. . . . . . 7 ⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
191		anandir 675	. . . . . . 7 ⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
192	190, 191	bitr4i 277	. . . . . 6 ⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸))
193		prcom 4735	. . . . . . . . . 10 ⊢ {𝐴, 𝐵} = {𝐵, 𝐴}
194	193	eleq1i 2824	. . . . . . . . 9 ⊢ ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐵, 𝐴} ∈ 𝐸)
195	194	anbi2i 623	. . . . . . . 8 ⊢ (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸))
196	195	anbi2i 623	. . . . . . 7 ⊢ ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
197		anandir 675	. . . . . . 7 ⊢ ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
198	196, 197	bitr4i 277	. . . . . 6 ⊢ ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸))
199	186, 192, 198	3anbi123i 1155	. . . . 5 ⊢ (((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))) ↔ ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸)))
200		3anrot 1100	. . . . . . 7 ⊢ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
201		df-3an 1089	. . . . . . 7 ⊢ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸))
202		prcom 4735	. . . . . . . . 9 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
203	202	eleq1i 2824	. . . . . . . 8 ⊢ ({𝐵, 𝐴} ∈ 𝐸 ↔ {𝐴, 𝐵} ∈ 𝐸)
204		prcom 4735	. . . . . . . . 9 ⊢ {𝐶, 𝐵} = {𝐵, 𝐶}
205	204	eleq1i 2824	. . . . . . . 8 ⊢ ({𝐶, 𝐵} ∈ 𝐸 ↔ {𝐵, 𝐶} ∈ 𝐸)
206		biid 260	. . . . . . . 8 ⊢ ({𝐶, 𝐴} ∈ 𝐸 ↔ {𝐶, 𝐴} ∈ 𝐸)
207	203, 205, 206	3anbi123i 1155	. . . . . . 7 ⊢ (({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
208	200, 201, 207	3bitr3i 300	. . . . . 6 ⊢ ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
209		df-3an 1089	. . . . . . 7 ⊢ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸))
210		biid 260	. . . . . . . 8 ⊢ ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐴, 𝐵} ∈ 𝐸)
211		prcom 4735	. . . . . . . . 9 ⊢ {𝐴, 𝐶} = {𝐶, 𝐴}
212	211	eleq1i 2824	. . . . . . . 8 ⊢ ({𝐴, 𝐶} ∈ 𝐸 ↔ {𝐶, 𝐴} ∈ 𝐸)
213	210, 205, 212	3anbi123i 1155	. . . . . . 7 ⊢ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
214	209, 213	bitr3i 276	. . . . . 6 ⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
215		df-3an 1089	. . . . . . 7 ⊢ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸))
216		3anrot 1100	. . . . . . . 8 ⊢ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))
217		3anrot 1100	. . . . . . . 8 ⊢ (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))
218		biid 260	. . . . . . . . 9 ⊢ ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐵, 𝐶} ∈ 𝐸)
219	203, 218, 212	3anbi123i 1155	. . . . . . . 8 ⊢ (({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
220	216, 217, 219	3bitri 296	. . . . . . 7 ⊢ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
221	215, 220	bitr3i 276	. . . . . 6 ⊢ ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
222	208, 214, 221	3anbi123i 1155	. . . . 5 ⊢ (((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
223		df-3an 1089	. . . . . 6 ⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
224		anabs1 660	. . . . . 6 ⊢ (((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
225		anidm 565	. . . . . 6 ⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
226	223, 224, 225	3bitri 296	. . . . 5 ⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
227	199, 222, 226	3bitri 296	. . . 4 ⊢ (((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
228	180, 227	bitrdi 286	. . 3 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
229	13, 98, 228	3bitrd 304	. 2 ⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
230	229	ex 413	1 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2940  ∀wral 3061  ∃!wreu 3374   ∖ cdif 3944   ⊆ wss 3947  {csn 4627  {cpr 4629  {ctp 4631  ‘cfv 6540  Vtxcvtx 28245  Edgcedg 28296  USGraphcusgr 28398   FriendGraph cfrgr 29500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-oadd 8466  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-dju 9892  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-n0 12469  df-z 12555  df-uz 12819  df-fz 13481  df-hash 14287  df-edg 28297  df-umgr 28332  df-usgr 28400  df-frgr 29501

This theorem is referenced by:  3vfriswmgr  29520