uspgrlim - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > uspgrlim		Structured version Visualization version GIF version

Theorem uspgrlim 48480

Description: A local isomorphism of simple pseudographs is a bijection between their vertices that preserves neighborhoods, expressed by properties of their edges (not edge functions as in isgrlim2 48471). (Contributed by AV, 15-Aug-2025.)

**Hypotheses**
Ref	Expression
uspgrlim.v	⊢ 𝑉 = (Vtx‘𝐺)
uspgrlim.w	⊢ 𝑊 = (Vtx‘𝐻)
uspgrlim.n	⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣)
uspgrlim.m	⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣))
uspgrlim.i	⊢ 𝐼 = (Edg‘𝐺)
uspgrlim.j	⊢ 𝐽 = (Edg‘𝐻)
uspgrlim.k	⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}
uspgrlim.l	⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}

**Assertion**
Ref	Expression
uspgrlim	⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))))

Distinct variable groups: 𝑥,𝐺 𝑥,𝐻 𝑥,𝐼 𝑥,𝐽 𝑥,𝑀 𝑥,𝑁,𝑒 𝑒,𝐺 𝑒,𝐾,𝑥 𝑥,𝐿 𝑒,𝑓,𝑔 𝑓,𝐹,𝑣 𝑓,𝐺,𝑔,𝑣 𝑒,𝐻,𝑓,𝑔,𝑣 𝑔,𝐾 𝑔,𝐿 𝑒,𝑀,𝑓,𝑔 𝑒,𝑁,𝑓,𝑔 𝑣,𝑉 𝑓,𝑍,𝑣 𝑥,𝑔 Allowed substitution hints: 𝐹(𝑥,𝑒,𝑔) 𝐼(𝑣,𝑒,𝑓,𝑔) 𝐽(𝑣,𝑒,𝑓,𝑔) 𝐾(𝑣,𝑓) 𝐿(𝑣,𝑒,𝑓) 𝑀(𝑣) 𝑁(𝑣) 𝑉(𝑥,𝑒,𝑓,𝑔) 𝑊(𝑥,𝑣,𝑒,𝑓,𝑔) 𝑍(𝑥,𝑒,𝑔)

Proof of Theorem uspgrlim Dummy variables 𝑖 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		uspgrlim.v	. . 3 ⊢ 𝑉 = (Vtx‘𝐺)
2		uspgrlim.w	. . 3 ⊢ 𝑊 = (Vtx‘𝐻)
3		uspgrlim.n	. . 3 ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣)
4		uspgrlim.m	. . 3 ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣))
5		eqid 2737	. . 3 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
6		eqid 2737	. . 3 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
7		eqid 2737	. . 3 ⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}
8		eqid 2737	. . 3 ⊢ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}
9	1, 2, 3, 4, 5, 6, 7, 8	isgrlim2 48471	. 2 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))))))
10		fvex 6847	. . . . . . . . . . . . . 14 ⊢ (iEdg‘𝐻) ∈ V
11		vex 3434	. . . . . . . . . . . . . 14 ⊢ ℎ ∈ V
12	10, 11	coex 7874	. . . . . . . . . . . . 13 ⊢ ((iEdg‘𝐻) ∘ ℎ) ∈ V
13		fvex 6847	. . . . . . . . . . . . . 14 ⊢ (iEdg‘𝐺) ∈ V
14	13	cnvex 7869	. . . . . . . . . . . . 13 ⊢ ^◡(iEdg‘𝐺) ∈ V
15	12, 14	coex 7874	. . . . . . . . . . . 12 ⊢ (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) ∈ V
16	15	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) ∈ V)
17	5	uspgrf1oedg 29256	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺))
18	17	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺))
19		simprl 771	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})
20	6	uspgrf1oedg 29256	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ USPGraph → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1-onto→(Edg‘𝐻))
21	20	ad2antlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1-onto→(Edg‘𝐻))
22		ssrab2 4021	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)
23		ssrab2 4021	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ⊆ dom (iEdg‘𝐻)
24	22, 23	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ ({𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ⊆ dom (iEdg‘𝐻))
25	24	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ({𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ⊆ dom (iEdg‘𝐻)))
26		3f1oss1 47535	. . . . . . . . . . . . . 14 ⊢ ((((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺) ∧ ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1-onto→(Edg‘𝐻)) ∧ ({𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ⊆ dom (iEdg‘𝐻))) → (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})–1-1-onto→((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
27	18, 19, 21, 25, 26	syl31anc 1376	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})–1-1-onto→((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
28		eqidd 2738	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)))
29		uspgrlim.i	. . . . . . . . . . . . . . . 16 ⊢ 𝐼 = (Edg‘𝐺)
30		uspgrlim.k	. . . . . . . . . . . . . . . 16 ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}
31	3, 29, 30	uspgrlimlem1 48476	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → 𝐾 = ((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}))
32	31	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → 𝐾 = ((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}))
33		uspgrlim.j	. . . . . . . . . . . . . . . 16 ⊢ 𝐽 = (Edg‘𝐻)
34		uspgrlim.l	. . . . . . . . . . . . . . . 16 ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}
35	4, 33, 34	uspgrlimlem1 48476	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ USPGraph → 𝐿 = ((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
36	35	ad2antlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → 𝐿 = ((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
37	28, 32, 36	f1oeq123d 6768	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):𝐾–1-1-onto→𝐿 ↔ (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})–1-1-onto→((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})))
38	27, 37	mpbird 257	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):𝐾–1-1-onto→𝐿)
39		simpll 767	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → 𝐺 ∈ USPGraph)
40		simprr 773	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))
41	1, 2, 3, 4, 29, 33, 30, 34	uspgrlimlem3 48478	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ USPGraph ∧ ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) → (𝑒 ∈ 𝐾 → (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
42	39, 19, 40, 41	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (𝑒 ∈ 𝐾 → (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
43	42	ralrimiv 3129	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒))
44	38, 43	jca 511	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
45		f1oeq1 6762	. . . . . . . . . . . 12 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → (𝑔:𝐾–1-1-onto→𝐿 ↔ (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):𝐾–1-1-onto→𝐿))
46		fveq1 6833	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → (𝑔‘𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒))
47	46	eqeq2d 2748	. . . . . . . . . . . . 13 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
48	47	ralbidv 3161	. . . . . . . . . . . 12 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → (∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
49	45, 48	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → ((𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)) ↔ ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒))))
50	16, 44, 49	spcedv 3541	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)))
51	50	ex 412	. . . . . . . . 9 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → ((ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) → ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
52	51	exlimdv 1935	. . . . . . . 8 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) → ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
53	10	cnvex 7869	. . . . . . . . . . . . . 14 ⊢ ^◡(iEdg‘𝐻) ∈ V
54		vex 3434	. . . . . . . . . . . . . 14 ⊢ 𝑔 ∈ V
55	53, 54	coex 7874	. . . . . . . . . . . . 13 ⊢ (^◡(iEdg‘𝐻) ∘ 𝑔) ∈ V
56	55, 13	coex 7874	. . . . . . . . . . . 12 ⊢ ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) ∈ V
57	56	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) ∈ V)
58	17	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺))
59		simprl 771	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → 𝑔:𝐾–1-1-onto→𝐿)
60	20	ad2antlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1-onto→(Edg‘𝐻))
61	29	rabeqi 3403	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁} = {𝑥 ∈ (Edg‘𝐺) ∣ 𝑥 ⊆ 𝑁}
62	30, 61	eqtri 2760	. . . . . . . . . . . . . . . . 17 ⊢ 𝐾 = {𝑥 ∈ (Edg‘𝐺) ∣ 𝑥 ⊆ 𝑁}
63	62	ssrab3 4023	. . . . . . . . . . . . . . . 16 ⊢ 𝐾 ⊆ (Edg‘𝐺)
64	33	rabeqi 3403	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀} = {𝑥 ∈ (Edg‘𝐻) ∣ 𝑥 ⊆ 𝑀}
65	34, 64	eqtri 2760	. . . . . . . . . . . . . . . . 17 ⊢ 𝐿 = {𝑥 ∈ (Edg‘𝐻) ∣ 𝑥 ⊆ 𝑀}
66	65	ssrab3 4023	. . . . . . . . . . . . . . . 16 ⊢ 𝐿 ⊆ (Edg‘𝐻)
67	63, 66	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ⊆ (Edg‘𝐺) ∧ 𝐿 ⊆ (Edg‘𝐻))
68	67	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝐾 ⊆ (Edg‘𝐺) ∧ 𝐿 ⊆ (Edg‘𝐻)))
69		3f1oss2 47536	. . . . . . . . . . . . . 14 ⊢ ((((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺) ∧ 𝑔:𝐾–1-1-onto→𝐿 ∧ (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1-onto→(Edg‘𝐻)) ∧ (𝐾 ⊆ (Edg‘𝐺) ∧ 𝐿 ⊆ (Edg‘𝐻))) → ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):(^◡(iEdg‘𝐺) “ 𝐾)–1-1-onto→(^◡(iEdg‘𝐻) “ 𝐿))
70	58, 59, 60, 68, 69	syl31anc 1376	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):(^◡(iEdg‘𝐺) “ 𝐾)–1-1-onto→(^◡(iEdg‘𝐻) “ 𝐿))
71		eqidd 2738	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)))
72	3, 29, 30	uspgrlimlem2 48477	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (^◡(iEdg‘𝐺) “ 𝐾) = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})
73	72	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐺) “ 𝐾) = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})
74	4, 33, 34	uspgrlimlem2 48477	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ USPGraph → (^◡(iEdg‘𝐻) “ 𝐿) = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})
75	74	ad2antlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐻) “ 𝐿) = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})
76	71, 73, 75	f1oeq123d 6768	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):(^◡(iEdg‘𝐺) “ 𝐾)–1-1-onto→(^◡(iEdg‘𝐻) “ 𝐿) ↔ ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
77	70, 76	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})
78		fveq2 6834	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑖 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝑖))
79	78	sseq1d 3954	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑖 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
80	79	elrab 3635	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ↔ (𝑖 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
81	1, 2, 3, 4, 29, 33, 30, 34	uspgrlimlem4 48479	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((𝑖 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁) → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))))
82	80, 81	biimtrid 242	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))))
83	82	ralrimiv 3129	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖)))
84	77, 83	jca 511	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))))
85		f1oeq1 6762	. . . . . . . . . . . 12 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ↔ ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
86		fveq1 6833	. . . . . . . . . . . . . . 15 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → (ℎ‘𝑖) = (((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))
87	86	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(ℎ‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖)))
88	87	eqeq2d 2748	. . . . . . . . . . . . 13 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → ((𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))))
89	88	ralbidv 3161	. . . . . . . . . . . 12 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))))
90	85, 89	anbi12d 633	. . . . . . . . . . 11 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → ((ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) ↔ (((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖)))))
91	57, 84, 90	spcedv 3541	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))
92	91	ex 412	. . . . . . . . 9 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → ((𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))))
93	92	exlimdv 1935	. . . . . . . 8 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))))
94	52, 93	impbid 212	. . . . . . 7 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) ↔ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
95	94	anbi2d 631	. . . . . 6 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → ((𝑓:𝑁–1-1-onto→𝑀 ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) ↔ (𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
96	95	exbidv 1923	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) ↔ ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
97	96	ralbidv 3161	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) ↔ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
98	97	anbi2d 631	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → ((𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))))
99	98	3adant3 1133	. 2 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑍) → ((𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))))
100	9, 99	bitrd 279	1 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ∀wral 3052 {crab 3390 Vcvv 3430 ⊆ wss 3890 ^◡ccnv 5623 dom cdm 5624 “ cima 5627 ∘ ccom 5628 –1-1-onto→wf1o 6491 ‘cfv 6492 (class class class)co 7360 Vtxcvtx 29079 iEdgciedg 29080 Edgcedg 29130 USPGraphcuspgr 29231 ClNeighbVtx cclnbgr 48306 GraphLocIso cgrlim 48464

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7363 df-oprab 7364 df-mpo 7365 df-1st 7935 df-2nd 7936 df-1o 8398 df-map 8768 df-vtx 29081 df-iedg 29082 df-edg 29131 df-uspgr 29233 df-clnbgr 48307 df-isubgr 48349 df-grim 48366 df-gric 48369 df-grlim 48466

This theorem is referenced by: usgrlimprop 48481

W3C validator