This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ∧ ( { 𝑎 , 𝑏 } ∈ 𝐼 ∧ { 𝑎 , 𝑐 } ∈ 𝐼 ∧ { 𝑏 , 𝑐 } ∈ 𝐼 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐾 ∧ { 𝑎 , 𝑐 } ∈ 𝐾 ∧ { 𝑏 , 𝑐 } ∈ 𝐾 ) )