Metamath Proof Explorer


Theorem isubgr3stgrlem1

Description: Lemma 1 for isubgr3stgr . (Contributed by AV, 16-Sep-2025)

Ref Expression
Hypotheses isubgr3stgr.v V = Vtx G
isubgr3stgr.u U = G NeighbVtx X
isubgr3stgr.c C = G ClNeighbVtx X
isubgr3stgr.f F = H X Y
Assertion isubgr3stgrlem1 H : U 1-1 onto R X V Y W Y R F : C 1-1 onto R Y

Proof

Step Hyp Ref Expression
1 isubgr3stgr.v V = Vtx G
2 isubgr3stgr.u U = G NeighbVtx X
3 isubgr3stgr.c C = G ClNeighbVtx X
4 isubgr3stgr.f F = H X Y
5 f1oeq2 U = G NeighbVtx X H : U 1-1 onto R H : G NeighbVtx X 1-1 onto R
6 2 5 ax-mp H : U 1-1 onto R H : G NeighbVtx X 1-1 onto R
7 6 biimpi H : U 1-1 onto R H : G NeighbVtx X 1-1 onto R
8 7 3ad2ant1 H : U 1-1 onto R X V Y W Y R H : G NeighbVtx X 1-1 onto R
9 simpl Y W Y R Y W
10 9 anim2i X V Y W Y R X V Y W
11 10 3adant1 H : U 1-1 onto R X V Y W Y R X V Y W
12 nbgrnself2 X G NeighbVtx X
13 12 a1i H : U 1-1 onto R X V Y W Y R X G NeighbVtx X
14 simp3r H : U 1-1 onto R X V Y W Y R Y R
15 4 f1ounsn H : G NeighbVtx X 1-1 onto R X V Y W X G NeighbVtx X Y R F : G NeighbVtx X X 1-1 onto R Y
16 8 11 13 14 15 syl112anc H : U 1-1 onto R X V Y W Y R F : G NeighbVtx X X 1-1 onto R Y
17 1 dfclnbgr4 X V G ClNeighbVtx X = X G NeighbVtx X
18 17 3ad2ant2 H : U 1-1 onto R X V Y W Y R G ClNeighbVtx X = X G NeighbVtx X
19 uncom X G NeighbVtx X = G NeighbVtx X X
20 18 19 eqtrdi H : U 1-1 onto R X V Y W Y R G ClNeighbVtx X = G NeighbVtx X X
21 3 20 eqtrid H : U 1-1 onto R X V Y W Y R C = G NeighbVtx X X
22 21 f1oeq2d H : U 1-1 onto R X V Y W Y R F : C 1-1 onto R Y F : G NeighbVtx X X 1-1 onto R Y
23 16 22 mpbird H : U 1-1 onto R X V Y W Y R F : C 1-1 onto R Y