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 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		simpl	\|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> G e. UHGraph )
6		simp1	\|- ( ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) -> { a , b } e. I )
7	6	adantl	\|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> { a , b } e. I )
8		vex	\|- a e. _V
9	8	prid1	\|- a e. { a , b }
10	9	a1i	\|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> a e. { a , b } )
11	2 3 4	clnbgrvtxedg	\|- ( ( G e. UHGraph /\ { a , b } e. I /\ a e. { a , b } ) -> { a , b } e. K )
12	5 7 10 11	syl3anc	\|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> { a , b } e. K )
13		simp2	\|- ( ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) -> { a , c } e. I )
14	13	adantl	\|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> { a , c } e. I )
15	8	prid1	\|- a e. { a , c }
16	15	a1i	\|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> a e. { a , c } )
17	2 3 4	clnbgrvtxedg	\|- ( ( G e. UHGraph /\ { a , c } e. I /\ a e. { a , c } ) -> { a , c } e. K )
18	5 14 16 17	syl3anc	\|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> { a , c } e. K )
19		simpr3	\|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> { b , c } e. I )
20	9	a1i	\|- ( ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) -> a e. { a , b } )
21		vex	\|- b e. _V
22	21	prid2	\|- b e. { a , b }
23	22	a1i	\|- ( ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) -> b e. { a , b } )
24	6 20 23	3jca	\|- ( ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) -> ( { a , b } e. I /\ a e. { a , b } /\ b e. { a , b } ) )
25	3 2	clnbgredg	\|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ a e. { a , b } /\ b e. { a , b } ) ) -> b e. N )
26	24 25	sylan2	\|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> b e. N )
27	15	a1i	\|- ( ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) -> a e. { a , c } )
28		vex	\|- c e. _V
29	28	prid2	\|- c e. { a , c }
30	29	a1i	\|- ( ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) -> c e. { a , c } )
31	13 27 30	3jca	\|- ( ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) -> ( { a , c } e. I /\ a e. { a , c } /\ c e. { a , c } ) )
32	3 2	clnbgredg	\|- ( ( G e. UHGraph /\ ( { a , c } e. I /\ a e. { a , c } /\ c e. { a , c } ) ) -> c e. N )
33	31 32	sylan2	\|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> c e. N )
34	26 33	prssd	\|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> { b , c } C_ N )
35		sseq1	\|- ( x = { b , c } -> ( x C_ N <-> { b , c } C_ N ) )
36	35 4	elrab2	\|- ( { b , c } e. K <-> ( { b , c } e. I /\ { b , c } C_ N ) )
37	19 34 36	sylanbrc	\|- ( ( G e. UHGraph /\ ( { a , b } e. I /\ { a , c } e. I /\ { b , c } e. I ) ) -> { b , c } e. K )
38	12 18 37	3jca	\|- ( ( 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 ) )

Metamath Proof Explorer

Theorem grlimgrtrilem1

Proof