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 ⊢ V = Vtx ⁡ G
grlimgrtrilem1.n ⊢ N = G ClNeighbVtx a
grlimgrtrilem1.i ⊢ I = Edg ⁡ G
grlimgrtrilem1.k ⊢ K = x ∈ I | x ⊆ N
Assertion grlimgrtrilem1 ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a b ∈ K ∧ a c ∈ K ∧ b c ∈ K

Proof

Step Hyp Ref Expression
1 grlimgrtrilem1.v ⊢ V = Vtx ⁡ G
2 grlimgrtrilem1.n ⊢ N = G ClNeighbVtx a
3 grlimgrtrilem1.i ⊢ I = Edg ⁡ G
4 grlimgrtrilem1.k ⊢ K = x ∈ I | x ⊆ N
5 simpl ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → G ∈ UHGraph
6 simp1 ⊢ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a b ∈ I
7 6 adantl ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a b ∈ I
8 vex ⊢ a ∈ V
9 8 prid1 ⊢ a ∈ a b
10 9 a1i ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a ∈ a b
11 2 3 4 clnbgrvtxedg ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a ∈ a b → a b ∈ K
12 5 7 10 11 syl3anc ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a b ∈ K
13 simp2 ⊢ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a c ∈ I
14 13 adantl ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a c ∈ I
15 8 prid1 ⊢ a ∈ a c
16 15 a1i ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a ∈ a c
17 2 3 4 clnbgrvtxedg ⊢ G ∈ UHGraph ∧ a c ∈ I ∧ a ∈ a c → a c ∈ K
18 5 14 16 17 syl3anc ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a c ∈ K
19 simpr3 ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → b c ∈ I
20 9 a1i ⊢ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a ∈ a b
21 vex ⊢ b ∈ V
22 21 prid2 ⊢ b ∈ a b
23 22 a1i ⊢ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → b ∈ a b
24 6 20 23 3jca ⊢ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a b ∈ I ∧ a ∈ a b ∧ b ∈ a b
25 3 2 clnbgredg ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a ∈ a b ∧ b ∈ a b → b ∈ N
26 24 25 sylan2 ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → b ∈ N
27 15 a1i ⊢ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a ∈ a c
28 vex ⊢ c ∈ V
29 28 prid2 ⊢ c ∈ a c
30 29 a1i ⊢ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → c ∈ a c
31 13 27 30 3jca ⊢ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a c ∈ I ∧ a ∈ a c ∧ c ∈ a c
32 3 2 clnbgredg ⊢ G ∈ UHGraph ∧ a c ∈ I ∧ a ∈ a c ∧ c ∈ a c → c ∈ N
33 31 32 sylan2 ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → c ∈ N
34 26 33 prssd ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → b c ⊆ N
35 sseq1 ⊢ x = b c → x ⊆ N ↔ b c ⊆ N
36 35 4 elrab2 ⊢ b c ∈ K ↔ b c ∈ I ∧ b c ⊆ N
37 19 34 36 sylanbrc ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → b c ∈ K
38 12 18 37 3jca ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a b ∈ K ∧ a c ∈ K ∧ b c ∈ K