Theorem isomuspgrlem2e

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

	Ref	Expression
Hypotheses	isomushgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐴 )
	isomushgr.w	⊢ 𝑊 = ( Vtx ‘ 𝐵 )
	isomushgr.e	⊢ 𝐸 = ( Edg ‘ 𝐴 )
	isomushgr.k	⊢ 𝐾 = ( Edg ‘ 𝐵 )
	isomuspgrlem2.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) )
	isomuspgrlem2.a	⊢ ( 𝜑 → 𝐴 ∈ USPGraph )
	isomuspgrlem2.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
	isomuspgrlem2.i	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) )
	isomuspgrlem2.x	⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
	isomuspgrlem2.b	⊢ ( 𝜑 → 𝐵 ∈ USPGraph )
Assertion	isomuspgrlem2e	⊢ ( 𝜑 → 𝐺 : 𝐸 –1-1-onto→ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		isomushgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐴 )
2		isomushgr.w	⊢ 𝑊 = ( Vtx ‘ 𝐵 )
3		isomushgr.e	⊢ 𝐸 = ( Edg ‘ 𝐴 )
4		isomushgr.k	⊢ 𝐾 = ( Edg ‘ 𝐵 )
5		isomuspgrlem2.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) )
6		isomuspgrlem2.a	⊢ ( 𝜑 → 𝐴 ∈ USPGraph )
7		isomuspgrlem2.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
8		isomuspgrlem2.i	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) )
9		isomuspgrlem2.x	⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
10		isomuspgrlem2.b	⊢ ( 𝜑 → 𝐵 ∈ USPGraph )
11	1 2 3 4 5 6 7 8 9	isomuspgrlem2c	⊢ ( 𝜑 → 𝐺 : 𝐸 –1-1→ 𝐾 )
12	1 2 3 4 5 6 7 8 9 10	isomuspgrlem2d	⊢ ( 𝜑 → 𝐺 : 𝐸 –onto→ 𝐾 )
13		df-f1o	⊢ ( 𝐺 : 𝐸 –1-1-onto→ 𝐾 ↔ ( 𝐺 : 𝐸 –1-1→ 𝐾 ∧ 𝐺 : 𝐸 –onto→ 𝐾 ) )
14	11 12 13	sylanbrc	⊢ ( 𝜑 → 𝐺 : 𝐸 –1-1-onto→ 𝐾 )