Theorem isomuspgrlem2e

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

	Ref	Expression
Hypotheses	isomushgr.v	$$⊢V=\mathrm{Vtx}\left(A\right)$$
	isomushgr.w	$$⊢W=\mathrm{Vtx}\left(B\right)$$
	isomushgr.e	$$⊢E=\mathrm{Edg}\left(A\right)$$
	isomushgr.k	$$⊢K=\mathrm{Edg}\left(B\right)$$
	isomuspgrlem2.g	$$⊢G=\left(x\in E⟼F\left[x\right]\right)$$
	isomuspgrlem2.a	$$⊢\phi \to A\in \mathrm{USHGraph}$$
	isomuspgrlem2.f	$$⊢\phi \to F:V\underset{1-1\; onto}{⟶}W$$
	isomuspgrlem2.i	$$⊢\phi \to \forall a\in V\forall b\in V\left(\left\{a,b\right\}\in E\leftrightarrow \left\{F\left(a\right),F\left(b\right)\right\}\in K\right)$$
	isomuspgrlem2.x	$$⊢\phi \to F\in X$$
	isomuspgrlem2.b	$$⊢\phi \to B\in \mathrm{USHGraph}$$
Assertion	isomuspgrlem2e	$$⊢\phi \to G:E\underset{1-1\; onto}{⟶}K$$

Proof

Step	Hyp	Ref	Expression
1		isomushgr.v	$$⊢V=\mathrm{Vtx}\left(A\right)$$
2		isomushgr.w	$$⊢W=\mathrm{Vtx}\left(B\right)$$
3		isomushgr.e	$$⊢E=\mathrm{Edg}\left(A\right)$$
4		isomushgr.k	$$⊢K=\mathrm{Edg}\left(B\right)$$
5		isomuspgrlem2.g	$$⊢G=\left(x\in E⟼F\left[x\right]\right)$$
6		isomuspgrlem2.a	$$⊢\phi \to A\in \mathrm{USHGraph}$$
7		isomuspgrlem2.f	$$⊢\phi \to F:V\underset{1-1\; onto}{⟶}W$$
8		isomuspgrlem2.i	$$⊢\phi \to \forall a\in V\forall b\in V\left(\left\{a,b\right\}\in E\leftrightarrow \left\{F\left(a\right),F\left(b\right)\right\}\in K\right)$$
9		isomuspgrlem2.x	$$⊢\phi \to F\in X$$
10		isomuspgrlem2.b	$$⊢\phi \to B\in \mathrm{USHGraph}$$
11	1 2 3 4 5 6 7 8 9	isomuspgrlem2c	$$⊢\phi \to G:E\underset{1-1}{⟶}K$$
12	1 2 3 4 5 6 7 8 9 10	isomuspgrlem2d	$$⊢\phi \to G:E\underset{onto}{⟶}K$$
13		df-f1o	$$⊢G:E\underset{1-1\; onto}{⟶}K\leftrightarrow \left(G:E\underset{1-1}{⟶}K\wedge G:E\underset{onto}{⟶}K\right)$$
14	11 12 13	sylanbrc	$$⊢\phi \to G:E\underset{1-1\; onto}{⟶}K$$