Theorem cusgra3v 25993

Description: A graph with three (different) vertices is complete if and only if there is an edge between each of these three vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.)

Hypothesis

Ref	Expression
cusgra3v.v	⊢ 𝑉 = {𝐴, 𝐵, 𝐶}

Assertion

Ref	Expression
cusgra3v	⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝑉 ComplUSGrph 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))

Proof of Theorem cusgra3v

Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp2 1055	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → 𝑉 USGrph 𝐸)
2	1	biantrurd 528	. 2 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸)))
3		cusgra3v.v	. . . . . . . 8 ⊢ 𝑉 = {𝐴, 𝐵, 𝐶}
4	3	difeq1i 3686	. . . . . . 7 ⊢ (𝑉 ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑘})
5	4	a1i 11	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝑉 ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑘}))
6	5	raleqdv 3121	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸))
7	6	ralbidv 2969	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸))
8	3	raleqi 3119	. . . . 5 ⊢ (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸)
9	8	a1i 11	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸))
10		sneq 4135	. . . . . . . 8 ⊢ (𝑘 = 𝐴 → {𝑘} = {𝐴})
11	10	difeq2d 3690	. . . . . . 7 ⊢ (𝑘 = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}))
12		preq2 4213	. . . . . . . 8 ⊢ (𝑘 = 𝐴 → {𝑛, 𝑘} = {𝑛, 𝐴})
13	12	eleq1d 2672	. . . . . . 7 ⊢ (𝑘 = 𝐴 → ({𝑛, 𝑘} ∈ ran 𝐸 ↔ {𝑛, 𝐴} ∈ ran 𝐸))
14	11, 13	raleqbidv 3129	. . . . . 6 ⊢ (𝑘 = 𝐴 → (∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑛, 𝐴} ∈ ran 𝐸))
15		sneq 4135	. . . . . . . 8 ⊢ (𝑘 = 𝐵 → {𝑘} = {𝐵})
16	15	difeq2d 3690	. . . . . . 7 ⊢ (𝑘 = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}))
17		preq2 4213	. . . . . . . 8 ⊢ (𝑘 = 𝐵 → {𝑛, 𝑘} = {𝑛, 𝐵})
18	17	eleq1d 2672	. . . . . . 7 ⊢ (𝑘 = 𝐵 → ({𝑛, 𝑘} ∈ ran 𝐸 ↔ {𝑛, 𝐵} ∈ ran 𝐸))
19	16, 18	raleqbidv 3129	. . . . . 6 ⊢ (𝑘 = 𝐵 → (∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑛, 𝐵} ∈ ran 𝐸))
20		sneq 4135	. . . . . . . 8 ⊢ (𝑘 = 𝐶 → {𝑘} = {𝐶})
21	20	difeq2d 3690	. . . . . . 7 ⊢ (𝑘 = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}))
22		preq2 4213	. . . . . . . 8 ⊢ (𝑘 = 𝐶 → {𝑛, 𝑘} = {𝑛, 𝐶})
23	22	eleq1d 2672	. . . . . . 7 ⊢ (𝑘 = 𝐶 → ({𝑛, 𝑘} ∈ ran 𝐸 ↔ {𝑛, 𝐶} ∈ ran 𝐸))
24	21, 23	raleqbidv 3129	. . . . . 6 ⊢ (𝑘 = 𝐶 → (∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑛, 𝐶} ∈ ran 𝐸))
25	14, 19, 24	raltpg 4183	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ (∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑛, 𝐴} ∈ ran 𝐸 ∧ ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑛, 𝐵} ∈ ran 𝐸 ∧ ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑛, 𝐶} ∈ ran 𝐸)))
26	25	3ad2ant1 1075	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ (∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑛, 𝐴} ∈ ran 𝐸 ∧ ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑛, 𝐵} ∈ ran 𝐸 ∧ ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑛, 𝐶} ∈ ran 𝐸)))
27	7, 9, 26	3bitrd 293	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ (∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑛, 𝐴} ∈ ran 𝐸 ∧ ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑛, 𝐵} ∈ ran 𝐸 ∧ ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑛, 𝐶} ∈ ran 𝐸)))
28		tprot 4228	. . . . . . . . 9 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
29	28	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴})
30	29	difeq1d 3689	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = ({𝐵, 𝐶, 𝐴} ∖ {𝐴}))
31		necom 2835	. . . . . . . . . . 11 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
32		necom 2835	. . . . . . . . . . 11 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴)
33	31, 32	anbi12i 729	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴))
34	33	biimpi 205	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → (𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴))
35	34	3adant3 1074	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴))
36		diftpsn3 4273	. . . . . . . 8 ⊢ ((𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
37	35, 36	syl 17	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
38	30, 37	eqtrd 2644	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶})
39	38	3ad2ant3 1077	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶})
40	39	raleqdv 3121	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑛, 𝐴} ∈ ran 𝐸 ↔ ∀𝑛 ∈ {𝐵, 𝐶} {𝑛, 𝐴} ∈ ran 𝐸))
41		tpcomb 4230	. . . . . . . . 9 ⊢ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵}
42	41	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵})
43	42	difeq1d 3689	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = ({𝐴, 𝐶, 𝐵} ∖ {𝐵}))
44		necom 2835	. . . . . . . . . . 11 ⊢ (𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵)
45	44	biimpi 205	. . . . . . . . . 10 ⊢ (𝐵 ≠ 𝐶 → 𝐶 ≠ 𝐵)
46	45	anim2i 591	. . . . . . . . 9 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵))
47	46	3adant2 1073	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵))
48		diftpsn3 4273	. . . . . . . 8 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) → ({𝐴, 𝐶, 𝐵} ∖ {𝐵}) = {𝐴, 𝐶})
49	47, 48	syl 17	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐶, 𝐵} ∖ {𝐵}) = {𝐴, 𝐶})
50	43, 49	eqtrd 2644	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐴, 𝐶})
51	50	3ad2ant3 1077	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐴, 𝐶})
52	51	raleqdv 3121	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑛, 𝐵} ∈ ran 𝐸 ↔ ∀𝑛 ∈ {𝐴, 𝐶} {𝑛, 𝐵} ∈ ran 𝐸))
53		diftpsn3 4273	. . . . . . 7 ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
54	53	3adant1 1072	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
55	54	3ad2ant3 1077	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
56	55	raleqdv 3121	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑛, 𝐶} ∈ ran 𝐸 ↔ ∀𝑛 ∈ {𝐴, 𝐵} {𝑛, 𝐶} ∈ ran 𝐸))
57	40, 52, 56	3anbi123d 1391	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑛, 𝐴} ∈ ran 𝐸 ∧ ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑛, 𝐵} ∈ ran 𝐸 ∧ ∀𝑛 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑛, 𝐶} ∈ ran 𝐸) ↔ (∀𝑛 ∈ {𝐵, 𝐶} {𝑛, 𝐴} ∈ ran 𝐸 ∧ ∀𝑛 ∈ {𝐴, 𝐶} {𝑛, 𝐵} ∈ ran 𝐸 ∧ ∀𝑛 ∈ {𝐴, 𝐵} {𝑛, 𝐶} ∈ ran 𝐸)))
58		preq1 4212	. . . . . . . . 9 ⊢ (𝑛 = 𝐵 → {𝑛, 𝐴} = {𝐵, 𝐴})
59	58	eleq1d 2672	. . . . . . . 8 ⊢ (𝑛 = 𝐵 → ({𝑛, 𝐴} ∈ ran 𝐸 ↔ {𝐵, 𝐴} ∈ ran 𝐸))
60		preq1 4212	. . . . . . . . 9 ⊢ (𝑛 = 𝐶 → {𝑛, 𝐴} = {𝐶, 𝐴})
61	60	eleq1d 2672	. . . . . . . 8 ⊢ (𝑛 = 𝐶 → ({𝑛, 𝐴} ∈ ran 𝐸 ↔ {𝐶, 𝐴} ∈ ran 𝐸))
62	59, 61	ralprg 4181	. . . . . . 7 ⊢ ((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑛 ∈ {𝐵, 𝐶} {𝑛, 𝐴} ∈ ran 𝐸 ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
63	62	3adant1 1072	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑛 ∈ {𝐵, 𝐶} {𝑛, 𝐴} ∈ ran 𝐸 ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
64	63	3ad2ant1 1075	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑛 ∈ {𝐵, 𝐶} {𝑛, 𝐴} ∈ ran 𝐸 ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
65		preq1 4212	. . . . . . . . 9 ⊢ (𝑛 = 𝐴 → {𝑛, 𝐵} = {𝐴, 𝐵})
66	65	eleq1d 2672	. . . . . . . 8 ⊢ (𝑛 = 𝐴 → ({𝑛, 𝐵} ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸))
67		preq1 4212	. . . . . . . . 9 ⊢ (𝑛 = 𝐶 → {𝑛, 𝐵} = {𝐶, 𝐵})
68	67	eleq1d 2672	. . . . . . . 8 ⊢ (𝑛 = 𝐶 → ({𝑛, 𝐵} ∈ ran 𝐸 ↔ {𝐶, 𝐵} ∈ ran 𝐸))
69	66, 68	ralprg 4181	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) → (∀𝑛 ∈ {𝐴, 𝐶} {𝑛, 𝐵} ∈ ran 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))
70	69	3adant2 1073	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑛 ∈ {𝐴, 𝐶} {𝑛, 𝐵} ∈ ran 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))
71	70	3ad2ant1 1075	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑛 ∈ {𝐴, 𝐶} {𝑛, 𝐵} ∈ ran 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))
72		preq1 4212	. . . . . . . . 9 ⊢ (𝑛 = 𝐴 → {𝑛, 𝐶} = {𝐴, 𝐶})
73	72	eleq1d 2672	. . . . . . . 8 ⊢ (𝑛 = 𝐴 → ({𝑛, 𝐶} ∈ ran 𝐸 ↔ {𝐴, 𝐶} ∈ ran 𝐸))
74		preq1 4212	. . . . . . . . 9 ⊢ (𝑛 = 𝐵 → {𝑛, 𝐶} = {𝐵, 𝐶})
75	74	eleq1d 2672	. . . . . . . 8 ⊢ (𝑛 = 𝐵 → ({𝑛, 𝐶} ∈ ran 𝐸 ↔ {𝐵, 𝐶} ∈ ran 𝐸))
76	73, 75	ralprg 4181	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (∀𝑛 ∈ {𝐴, 𝐵} {𝑛, 𝐶} ∈ ran 𝐸 ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))
77	76	3adant3 1074	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑛 ∈ {𝐴, 𝐵} {𝑛, 𝐶} ∈ ran 𝐸 ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))
78	77	3ad2ant1 1075	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∀𝑛 ∈ {𝐴, 𝐵} {𝑛, 𝐶} ∈ ran 𝐸 ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))
79	64, 71, 78	3anbi123d 1391	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((∀𝑛 ∈ {𝐵, 𝐶} {𝑛, 𝐴} ∈ ran 𝐸 ∧ ∀𝑛 ∈ {𝐴, 𝐶} {𝑛, 𝐵} ∈ ran 𝐸 ∧ ∀𝑛 ∈ {𝐴, 𝐵} {𝑛, 𝐶} ∈ ran 𝐸) ↔ (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))))
80		ancom 465	. . . . . . 7 ⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ↔ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸))
81	80	3anbi2i 1247	. . . . . 6 ⊢ ((({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ↔ (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))
82		3an6 1401	. . . . . 6 ⊢ ((({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ↔ (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))
83	81, 82	bitri 263	. . . . 5 ⊢ ((({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ↔ (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))
84	83	a1i 11	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ↔ (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))))
85		prcom 4211	. . . . . . . . 9 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
86	85	eleq1i 2679	. . . . . . . 8 ⊢ ({𝐵, 𝐴} ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸)
87		prcom 4211	. . . . . . . . 9 ⊢ {𝐶, 𝐵} = {𝐵, 𝐶}
88	87	eleq1i 2679	. . . . . . . 8 ⊢ ({𝐶, 𝐵} ∈ ran 𝐸 ↔ {𝐵, 𝐶} ∈ ran 𝐸)
89		prcom 4211	. . . . . . . . 9 ⊢ {𝐴, 𝐶} = {𝐶, 𝐴}
90	89	eleq1i 2679	. . . . . . . 8 ⊢ ({𝐴, 𝐶} ∈ ran 𝐸 ↔ {𝐶, 𝐴} ∈ ran 𝐸)
91	86, 88, 90	3anbi123i 1244	. . . . . . 7 ⊢ (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
92		3anrot 1036	. . . . . . 7 ⊢ (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
93	91, 92	anbi12i 729	. . . . . 6 ⊢ ((({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
94		anidm 674	. . . . . 6 ⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
95	93, 94	bitri 263	. . . . 5 ⊢ ((({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))
96	95	a1i 11	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
97	79, 84, 96	3bitrd 293	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((∀𝑛 ∈ {𝐵, 𝐶} {𝑛, 𝐴} ∈ ran 𝐸 ∧ ∀𝑛 ∈ {𝐴, 𝐶} {𝑛, 𝐵} ∈ ran 𝐸 ∧ ∀𝑛 ∈ {𝐴, 𝐵} {𝑛, 𝐶} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))
98	27, 57, 97	3bitrrd 294	. 2 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸))
99		usgrav 25867	. . . 4 ⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V))
100		iscusgra 25985	. . . 4 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ComplUSGrph 𝐸 ↔ (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸)))
101	99, 100	syl 17	. . 3 ⊢ (𝑉 USGrph 𝐸 → (𝑉 ComplUSGrph 𝐸 ↔ (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸)))
102	101	3ad2ant2 1076	. 2 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝑉 ComplUSGrph 𝐸 ↔ (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸)))
103	2, 98, 102	3bitr4rd 300	1 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝑉 USGrph 𝐸 ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝑉 ComplUSGrph 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  Vcvv 3173   ∖ cdif 3537  {csn 4125  {cpr 4127  {ctp 4129   class class class wbr 4583  ran crn 5039   USGrph cusg 25859   ComplUSGrph ccusgra 25947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-rel 5045  df-cnv 5046  df-dm 5048  df-rn 5049  df-usgra 25862  df-cusgra 25950

This theorem is referenced by:  cusgra3vnbpr  25994