grlimgrtrilem1

Description: Lemma 3 for grlimgrtri . (Contributed by AV, 24-Aug-2025) (Proof shortened by AV, 27-Dec-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		simpl	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → 𝐺 ∈ UHGraph )
6		simp1	⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) → { 𝑎 , 𝑏 } ∈ 𝐼 )
7	6	adantl	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → { 𝑎 , 𝑏 } ∈ 𝐼 )
8		vex	⊢ 𝑎 ∈ V
9	8	prid1	⊢ 𝑎 ∈ { 𝑎 , 𝑏 }
10	9	a1i	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → 𝑎 ∈ { 𝑎 , 𝑏 } )
11	2 3 4	clnbgrvtxedg	⊢ ( ( 𝐺 ∈ UHGraph ∧ { 𝑎 , 𝑏 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑏 } ) → { 𝑎 , 𝑏 } ∈ 𝐾 )
12	5 7 10 11	syl3anc	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → { 𝑎 , 𝑏 } ∈ 𝐾 )
13		simp2	⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) → { 𝑎 , 𝑐 } ∈ 𝐼 )
14	13	adantl	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → { 𝑎 , 𝑐 } ∈ 𝐼 )
15	8	prid1	⊢ 𝑎 ∈ { 𝑎 , 𝑐 }
16	15	a1i	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → 𝑎 ∈ { 𝑎 , 𝑐 } )
17	2 3 4	clnbgrvtxedg	⊢ ( ( 𝐺 ∈ UHGraph ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑐 } ) → { 𝑎 , 𝑐 } ∈ 𝐾 )
18	5 14 16 17	syl3anc	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → { 𝑎 , 𝑐 } ∈ 𝐾 )
19		simpr3	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → { 𝑏 , 𝑐 } ∈ 𝐼 )
20	9	a1i	⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) → 𝑎 ∈ { 𝑎 , 𝑏 } )
21		vex	⊢ 𝑏 ∈ V
22	21	prid2	⊢ 𝑏 ∈ { 𝑎 , 𝑏 }
23	22	a1i	⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) → 𝑏 ∈ { 𝑎 , 𝑏 } )
24	6 20 23	3jca	⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) → ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑏 } ∧ 𝑏 ∈ { 𝑎 , 𝑏 } ) )
25	3 2	clnbgredg	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑏 } ∧ 𝑏 ∈ { 𝑎 , 𝑏 } ) ) → 𝑏 ∈ 𝑁 )
26	24 25	sylan2	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → 𝑏 ∈ 𝑁 )
27	15	a1i	⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) → 𝑎 ∈ { 𝑎 , 𝑐 } )
28		vex	⊢ 𝑐 ∈ V
29	28	prid2	⊢ 𝑐 ∈ { 𝑎 , 𝑐 }
30	29	a1i	⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) → 𝑐 ∈ { 𝑎 , 𝑐 } )
31	13 27 30	3jca	⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) → ( { 𝑎 , 𝑐 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑐 } ∧ 𝑐 ∈ { 𝑎 , 𝑐 } ) )
32	3 2	clnbgredg	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑐 } ∈ 𝐼 ∧ 𝑎 ∈ { 𝑎 , 𝑐 } ∧ 𝑐 ∈ { 𝑎 , 𝑐 } ) ) → 𝑐 ∈ 𝑁 )
33	31 32	sylan2	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → 𝑐 ∈ 𝑁 )
34	26 33	prssd	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → { 𝑏 , 𝑐 } ⊆ 𝑁 )
35		sseq1	⊢ ( 𝑥 = { 𝑏 , 𝑐 } → ( 𝑥 ⊆ 𝑁 ↔ { 𝑏 , 𝑐 } ⊆ 𝑁 ) )
36	35 4	elrab2	⊢ ( { 𝑏 , 𝑐 } ∈ 𝐾 ↔ ( { 𝑏 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ⊆ 𝑁 ) )
37	19 34 36	sylanbrc	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → { 𝑏 , 𝑐 } ∈ 𝐾 )
38	12 18 37	3jca	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐾 ∧ { 𝑎 , 𝑐 } ∈ 𝐾 ∧ { 𝑏 , 𝑐 } ∈ 𝐾 ) )

Metamath Proof Explorer

Theorem grlimgrtrilem1

Proof