Theorem grlimgrtrilem1

Description: Lemma 3 for grlimgrtri . (Contributed by AV, 24-Aug-2025)

	Ref	Expression
Hypotheses	grlimgrtrilem1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	grlimgrtrilem1.n	⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑎 )
	grlimgrtrilem1.i	⊢ 𝐼 = ( Edg ‘ 𝐺 )
	grlimgrtrilem1.k	⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
Assertion	grlimgrtrilem1	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐾 ∧ { 𝑎 , 𝑐 } ∈ 𝐾 ∧ { 𝑏 , 𝑐 } ∈ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		grlimgrtrilem1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		grlimgrtrilem1.n	⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑎 )
3		grlimgrtrilem1.i	⊢ 𝐼 = ( Edg ‘ 𝐺 )
4		grlimgrtrilem1.k	⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
5		simpr1	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → { 𝑎 , 𝑏 } ∈ 𝐼 )
6		simpl	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → 𝐺 ∈ UHGraph )
7		vex	⊢ 𝑎 ∈ V
8	7	prid1	⊢ 𝑎 ∈ { 𝑎 , 𝑏 }
9	8	a1i	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → 𝑎 ∈ { 𝑎 , 𝑏 } )
10	3 2	clnbgrssedg	⊢ ( ( 𝐺 ∈ UHGraph ∧ { 𝑎 , 𝑏 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑏 } ) → { 𝑎 , 𝑏 } ⊆ 𝑁 )
11	6 5 9 10	syl3anc	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → { 𝑎 , 𝑏 } ⊆ 𝑁 )
12	5 11	jca	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑏 } ⊆ 𝑁 ) )
13		simpr2	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → { 𝑎 , 𝑐 } ∈ 𝐼 )
14	7	prid1	⊢ 𝑎 ∈ { 𝑎 , 𝑐 }
15	14	a1i	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → 𝑎 ∈ { 𝑎 , 𝑐 } )
16	3 2	clnbgrssedg	⊢ ( ( 𝐺 ∈ UHGraph ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑐 } ) → { 𝑎 , 𝑐 } ⊆ 𝑁 )
17	6 13 15 16	syl3anc	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → { 𝑎 , 𝑐 } ⊆ 𝑁 )
18	13 17	jca	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → ( { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ⊆ 𝑁 ) )
19		simpr3	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → { 𝑏 , 𝑐 } ∈ 𝐼 )
20		id	⊢ ( { 𝑎 , 𝑏 } ∈ 𝐼 → { 𝑎 , 𝑏 } ∈ 𝐼 )
21	8	a1i	⊢ ( { 𝑎 , 𝑏 } ∈ 𝐼 → 𝑎 ∈ { 𝑎 , 𝑏 } )
22		vex	⊢ 𝑏 ∈ V
23	22	prid2	⊢ 𝑏 ∈ { 𝑎 , 𝑏 }
24	23	a1i	⊢ ( { 𝑎 , 𝑏 } ∈ 𝐼 → 𝑏 ∈ { 𝑎 , 𝑏 } )
25	20 21 24	3jca	⊢ ( { 𝑎 , 𝑏 } ∈ 𝐼 → ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑏 } ∧ 𝑏 ∈ { 𝑎 , 𝑏 } ) )
26	25	3ad2ant1	⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) → ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑏 } ∧ 𝑏 ∈ { 𝑎 , 𝑏 } ) )
27	3 2	clnbgredg	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑏 } ∧ 𝑏 ∈ { 𝑎 , 𝑏 } ) ) → 𝑏 ∈ 𝑁 )
28	26 27	sylan2	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → 𝑏 ∈ 𝑁 )
29		id	⊢ ( { 𝑎 , 𝑐 } ∈ 𝐼 → { 𝑎 , 𝑐 } ∈ 𝐼 )
30	14	a1i	⊢ ( { 𝑎 , 𝑐 } ∈ 𝐼 → 𝑎 ∈ { 𝑎 , 𝑐 } )
31		vex	⊢ 𝑐 ∈ V
32	31	prid2	⊢ 𝑐 ∈ { 𝑎 , 𝑐 }
33	32	a1i	⊢ ( { 𝑎 , 𝑐 } ∈ 𝐼 → 𝑐 ∈ { 𝑎 , 𝑐 } )
34	29 30 33	3jca	⊢ ( { 𝑎 , 𝑐 } ∈ 𝐼 → ( { 𝑎 , 𝑐 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑐 } ∧ 𝑐 ∈ { 𝑎 , 𝑐 } ) )
35	34	3ad2ant2	⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) → ( { 𝑎 , 𝑐 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑐 } ∧ 𝑐 ∈ { 𝑎 , 𝑐 } ) )
36	3 2	clnbgredg	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑐 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑐 } ∧ 𝑐 ∈ { 𝑎 , 𝑐 } ) ) → 𝑐 ∈ 𝑁 )
37	35 36	sylan2	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → 𝑐 ∈ 𝑁 )
38	28 37	prssd	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → { 𝑏 , 𝑐 } ⊆ 𝑁 )
39	19 38	jca	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → ( { 𝑏 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ⊆ 𝑁 ) )
40	4	eleq2i	⊢ ( { 𝑎 , 𝑏 } ∈ 𝐾 ↔ { 𝑎 , 𝑏 } ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 } )
41		sseq1	⊢ ( 𝑥 = { 𝑎 , 𝑏 } → ( 𝑥 ⊆ 𝑁 ↔ { 𝑎 , 𝑏 } ⊆ 𝑁 ) )
42	41	elrab	⊢ ( { 𝑎 , 𝑏 } ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 } ↔ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑏 } ⊆ 𝑁 ) )
43	40 42	bitri	⊢ ( { 𝑎 , 𝑏 } ∈ 𝐾 ↔ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑏 } ⊆ 𝑁 ) )
44	4	eleq2i	⊢ ( { 𝑎 , 𝑐 } ∈ 𝐾 ↔ { 𝑎 , 𝑐 } ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 } )
45		sseq1	⊢ ( 𝑥 = { 𝑎 , 𝑐 } → ( 𝑥 ⊆ 𝑁 ↔ { 𝑎 , 𝑐 } ⊆ 𝑁 ) )
46	45	elrab	⊢ ( { 𝑎 , 𝑐 } ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 } ↔ ( { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ⊆ 𝑁 ) )
47	44 46	bitri	⊢ ( { 𝑎 , 𝑐 } ∈ 𝐾 ↔ ( { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ⊆ 𝑁 ) )
48	4	eleq2i	⊢ ( { 𝑏 , 𝑐 } ∈ 𝐾 ↔ { 𝑏 , 𝑐 } ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 } )
49		sseq1	⊢ ( 𝑥 = { 𝑏 , 𝑐 } → ( 𝑥 ⊆ 𝑁 ↔ { 𝑏 , 𝑐 } ⊆ 𝑁 ) )
50	49	elrab	⊢ ( { 𝑏 , 𝑐 } ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 } ↔ ( { 𝑏 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ⊆ 𝑁 ) )
51	48 50	bitri	⊢ ( { 𝑏 , 𝑐 } ∈ 𝐾 ↔ ( { 𝑏 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ⊆ 𝑁 ) )
52	43 47 51	3anbi123i	⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐾 ∧ { 𝑎 , 𝑐 } ∈ 𝐾 ∧ { 𝑏 , 𝑐 } ∈ 𝐾 ) ↔ ( ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑏 } ⊆ 𝑁 ) ∧ ( { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ⊆ 𝑁 ) ∧ ( { 𝑏 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ⊆ 𝑁 ) ) )
53	12 18 39 52	syl3anbrc	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐾 ∧ { 𝑎 , 𝑐 } ∈ 𝐾 ∧ { 𝑏 , 𝑐 } ∈ 𝐾 ) )