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 e. I | x C_ N }
Assertion	grlimgrtrilem1	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> ( { a , b } e. K /\ { a , c } e. K /\ { b , c } e. 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 e. I | x C_ N }
5		simpr1	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> { a , b } e. I )
6		simpl	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> G e. UHGraph )
7		vex	|- a e. _V
8	7	prid1	|- a e. { a , b }
9	8	a1i	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> a e. { a , b } )
10	3 2	clnbgrssedg	|- ( ( G e. UHGraph /\ { a , b } e. I /\ a e. { a , b } ) -> { a , b } C_ N )
11	6 5 9 10	syl3anc	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> { a , b } C_ N )
12	5 11	jca	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> ( { a , b } e. I /\ { a , b } C_ N ) )
13		simpr2	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> { a , c } e. I )
14	7	prid1	|- a e. { a , c }
15	14	a1i	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> a e. { a , c } )
16	3 2	clnbgrssedg	|- ( ( G e. UHGraph /\ { a , c } e. I /\ a e. { a , c } ) -> { a , c } C_ N )
17	6 13 15 16	syl3anc	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> { a , c } C_ N )
18	13 17	jca	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> ( { a , c } e. I /\ { a , c } C_ N ) )
19		simpr3	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> { b , c } e. I )
20		id	|- ( { a , b } e. I -> { a , b } e. I )
21	8	a1i	|- ( { a , b } e. I -> a e. { a , b } )
22		vex	|- b e. _V
23	22	prid2	|- b e. { a , b }
24	23	a1i	|- ( { a , b } e. I -> b e. { a , b } )
25	20 21 24	3jca	|- ( { a , b } e. I -> ( { a , b } e. I /\ a e. { a , b } /\ b e. { a , b } ) )
26	25	3ad2ant1	|- ( ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) -> ( { a , b } e. I /\ a e. { a , b } /\ b e. { a , b } ) )
27	3 2	clnbgredg	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ a e. { a , b } /\ b e. { a , b } ) ) -> b e. N )
28	26 27	sylan2	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> b e. N )
29		id	|- ( { a , c } e. I -> { a , c } e. I )
30	14	a1i	|- ( { a , c } e. I -> a e. { a , c } )
31		vex	|- c e. _V
32	31	prid2	|- c e. { a , c }
33	32	a1i	|- ( { a , c } e. I -> c e. { a , c } )
34	29 30 33	3jca	|- ( { a , c } e. I -> ( { a , c } e. I /\ a e. { a , c } /\ c e. { a , c } ) )
35	34	3ad2ant2	|- ( ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) -> ( { a , c } e. I /\ a e. { a , c } /\ c e. { a , c } ) )
36	3 2	clnbgredg	|- ( ( G e. UHGraph /\ ( { a , c } e. I /\ a e. { a , c } /\ c e. { a , c } ) ) -> c e. N )
37	35 36	sylan2	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> c e. N )
38	28 37	prssd	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> { b , c } C_ N )
39	19 38	jca	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> ( { b , c } e. I /\ { b , c } C_ N ) )
40	4	eleq2i	|- ( { a , b } e. K <-> { a , b } e. { x e. I | x C_ N } )
41		sseq1	|- ( x = { a , b } -> ( x C_ N <-> { a , b } C_ N ) )
42	41	elrab	|- ( { a , b } e. { x e. I | x C_ N } <-> ( { a , b } e. I /\ { a , b } C_ N ) )
43	40 42	bitri	|- ( { a , b } e. K <-> ( { a , b } e. I /\ { a , b } C_ N ) )
44	4	eleq2i	|- ( { a , c } e. K <-> { a , c } e. { x e. I | x C_ N } )
45		sseq1	|- ( x = { a , c } -> ( x C_ N <-> { a , c } C_ N ) )
46	45	elrab	|- ( { a , c } e. { x e. I | x C_ N } <-> ( { a , c } e. I /\ { a , c } C_ N ) )
47	44 46	bitri	|- ( { a , c } e. K <-> ( { a , c } e. I /\ { a , c } C_ N ) )
48	4	eleq2i	|- ( { b , c } e. K <-> { b , c } e. { x e. I | x C_ N } )
49		sseq1	|- ( x = { b , c } -> ( x C_ N <-> { b , c } C_ N ) )
50	49	elrab	|- ( { b , c } e. { x e. I | x C_ N } <-> ( { b , c } e. I /\ { b , c } C_ N ) )
51	48 50	bitri	|- ( { b , c } e. K <-> ( { b , c } e. I /\ { b , c } C_ N ) )
52	43 47 51	3anbi123i	|- ( ( { a , b } e. K /\ { a , c } e. K /\ { b , c } e. K ) <-> ( ( { a , b } e. I /\ { a , b } C_ N ) /\ ( { a , c } e. I /\ { a , c } C_ N ) /\ ( { b , c } e. I /\ { b , c } C_ N ) ) )
53	12 18 39 52	syl3anbrc	|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> ( { a , b } e. K /\ { a , c } e. K /\ { b , c } e. K ) )