Metamath Proof Explorer


Theorem isubgr3stgrlem9

Description: Lemma 9 for isubgr3stgr . (Contributed by AV, 29-Sep-2025)

Ref Expression
Hypotheses isubgr3stgr.v V = Vtx G
isubgr3stgr.u U = G NeighbVtx X
isubgr3stgr.c C = G ClNeighbVtx X
isubgr3stgr.n N 0
isubgr3stgr.s No typesetting found for |- S = ( StarGr ` N ) with typecode |-
isubgr3stgr.w W = Vtx S
isubgr3stgr.e E = Edg G
isubgr3stgr.i I = Edg G ISubGr C
isubgr3stgr.h H = i I F i
Assertion isubgr3stgrlem9 Could not format assertion : No typesetting found for |- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( H : I -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. I ( F " e ) = ( H ` e ) ) ) with typecode |-

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.n N 0
5 isubgr3stgr.s Could not format S = ( StarGr ` N ) : No typesetting found for |- S = ( StarGr ` N ) with typecode |-
6 isubgr3stgr.w W = Vtx S
7 isubgr3stgr.e E = Edg G
8 isubgr3stgr.i I = Edg G ISubGr C
9 isubgr3stgr.h H = i I F i
10 1 2 3 4 5 6 7 8 9 isubgr3stgrlem8 Could not format ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> H : I -1-1-onto-> ( Edg ` ( StarGr ` N ) ) ) : No typesetting found for |- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> H : I -1-1-onto-> ( Edg ` ( StarGr ` N ) ) ) with typecode |-
11 f1of F : C 1-1 onto W F : C W
12 11 ad2antrl G USGraph X V U = N x U y U x y E F : C 1-1 onto W F X = 0 F : C W
13 1 2 3 4 5 6 7 8 9 isubgr3stgrlem5 F : C W e I H e = F e
14 13 eqcomd F : C W e I F e = H e
15 12 14 sylan G USGraph X V U = N x U y U x y E F : C 1-1 onto W F X = 0 e I F e = H e
16 15 ralrimiva G USGraph X V U = N x U y U x y E F : C 1-1 onto W F X = 0 e I F e = H e
17 10 16 jca Could not format ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( H : I -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. I ( F " e ) = ( H ` e ) ) ) : No typesetting found for |- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( H : I -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. I ( F " e ) = ( H ` e ) ) ) with typecode |-