Metamath Proof Explorer

Theorem grlimgrtrilem1

Description: Lemma 3 for grlimgrtri . (Contributed by AV, 24-Aug-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 simpr1 ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a b ∈ I
6 simpl ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → G ∈ UHGraph
7 vex ⊢ a ∈ V
8 7 prid1 ⊢ a ∈ a b
9 8 a1i ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a ∈ a b
10 3 2 clnbgrssedg ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a ∈ a b → a b ⊆ N
11 6 5 9 10 syl3anc ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a b ⊆ N
12 5 11 jca ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a b ∈ I ∧ a b ⊆ N
13 simpr2 ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a c ∈ I
14 7 prid1 ⊢ a ∈ a c
15 14 a1i ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a ∈ a c
16 3 2 clnbgrssedg ⊢ G ∈ UHGraph ∧ a c ∈ I ∧ a ∈ a c → a c ⊆ N
17 6 13 15 16 syl3anc ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a c ⊆ N
18 13 17 jca ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a c ∈ I ∧ a c ⊆ N
19 simpr3 ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → b c ∈ I
20 id ⊢ a b ∈ I → a b ∈ I
21 8 a1i ⊢ a b ∈ I → a ∈ a b
22 vex ⊢ b ∈ V
23 22 prid2 ⊢ b ∈ a b
24 23 a1i ⊢ a b ∈ I → b ∈ a b
25 20 21 24 3jca ⊢ a b ∈ I → a b ∈ I ∧ a ∈ a b ∧ b ∈ a b
26 25 3ad2ant1 ⊢ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a b ∈ I ∧ a ∈ a b ∧ b ∈ a b
27 3 2 clnbgredg ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a ∈ a b ∧ b ∈ a b → b ∈ N
28 26 27 sylan2 ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → b ∈ N
29 id ⊢ a c ∈ I → a c ∈ I
30 14 a1i ⊢ a c ∈ I → a ∈ a c
31 vex ⊢ c ∈ V
32 31 prid2 ⊢ c ∈ a c
33 32 a1i ⊢ a c ∈ I → c ∈ a c
34 29 30 33 3jca ⊢ a c ∈ I → a c ∈ I ∧ a ∈ a c ∧ c ∈ a c
35 34 3ad2ant2 ⊢ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a c ∈ I ∧ a ∈ a c ∧ c ∈ a c
36 3 2 clnbgredg ⊢ G ∈ UHGraph ∧ a c ∈ I ∧ a ∈ a c ∧ c ∈ a c → c ∈ N
37 35 36 sylan2 ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → c ∈ N
38 28 37 prssd ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → b c ⊆ N
39 19 38 jca ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → b c ∈ I ∧ b c ⊆ N
40 4 eleq2i ⊢ a b ∈ K ↔ a b ∈ x ∈ I | x ⊆ N
41 sseq1 ⊢ x = a b → x ⊆ N ↔ a b ⊆ N
42 41 elrab ⊢ a b ∈ x ∈ I | x ⊆ N ↔ a b ∈ I ∧ a b ⊆ N
43 40 42 bitri ⊢ a b ∈ K ↔ a b ∈ I ∧ a b ⊆ N
44 4 eleq2i ⊢ a c ∈ K ↔ a c ∈ x ∈ I | x ⊆ N
45 sseq1 ⊢ x = a c → x ⊆ N ↔ a c ⊆ N
46 45 elrab ⊢ a c ∈ x ∈ I | x ⊆ N ↔ a c ∈ I ∧ a c ⊆ N
47 44 46 bitri ⊢ a c ∈ K ↔ a c ∈ I ∧ a c ⊆ N
48 4 eleq2i ⊢ b c ∈ K ↔ b c ∈ x ∈ I | x ⊆ N
49 sseq1 ⊢ x = b c → x ⊆ N ↔ b c ⊆ N
50 49 elrab ⊢ b c ∈ x ∈ I | x ⊆ N ↔ b c ∈ I ∧ b c ⊆ N
51 48 50 bitri ⊢ b c ∈ K ↔ b c ∈ I ∧ b c ⊆ N
52 43 47 51 3anbi123i ⊢ a b ∈ K ∧ a c ∈ K ∧ b c ∈ K ↔ a b ∈ I ∧ a b ⊆ N ∧ a c ∈ I ∧ a c ⊆ N ∧ b c ∈ I ∧ b c ⊆ N
53 12 18 39 52 syl3anbrc ⊢ G ∈ UHGraph ∧ a b ∈ I ∧ a c ∈ I ∧ b c ∈ I → a b ∈ K ∧ a c ∈ K ∧ b c ∈ K