Theorem isomuspgrlem2e

Description: Lemma 5 for isomuspgrlem2 . (Contributed by AV, 1-Dec-2022)

	Ref	Expression
Hypotheses	isomushgr.v	|- V = ( Vtx ` A )
	isomushgr.w	|- W = ( Vtx ` B )
	isomushgr.e	|- E = ( Edg ` A )
	isomushgr.k	|- K = ( Edg ` B )
	isomuspgrlem2.g	|- G = ( x e. E |-> ( F " x ) )
	isomuspgrlem2.a	|- ( ph -> A e. USPGraph )
	isomuspgrlem2.f	|- ( ph -> F : V -1-1-onto-> W )
	isomuspgrlem2.i	|- ( ph -> A. a e. V A. b e. V ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. K ) )
	isomuspgrlem2.x	|- ( ph -> F e. X )
	isomuspgrlem2.b	|- ( ph -> B e. USPGraph )
Assertion	isomuspgrlem2e	|- ( ph -> G : E -1-1-onto-> K )

Proof

Step	Hyp	Ref	Expression
1		isomushgr.v	|- V = ( Vtx ` A )
2		isomushgr.w	|- W = ( Vtx ` B )
3		isomushgr.e	|- E = ( Edg ` A )
4		isomushgr.k	|- K = ( Edg ` B )
5		isomuspgrlem2.g	|- G = ( x e. E |-> ( F " x ) )
6		isomuspgrlem2.a	|- ( ph -> A e. USPGraph )
7		isomuspgrlem2.f	|- ( ph -> F : V -1-1-onto-> W )
8		isomuspgrlem2.i	|- ( ph -> A. a e. V A. b e. V ( { a , b } e. E <-> { ( F ` a ) , ( F ` b ) } e. K ) )
9		isomuspgrlem2.x	|- ( ph -> F e. X )
10		isomuspgrlem2.b	|- ( ph -> B e. USPGraph )
11	1 2 3 4 5 6 7 8 9	isomuspgrlem2c	|- ( ph -> G : E -1-1-> K )
12	1 2 3 4 5 6 7 8 9 10	isomuspgrlem2d	|- ( ph -> G : E -onto-> K )
13		df-f1o	|- ( G : E -1-1-onto-> K <-> ( G : E -1-1-> K /\ G : E -onto-> K ) )
14	11 12 13	sylanbrc	|- ( ph -> G : E -1-1-onto-> K )