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 47817

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 47808). (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 2733	. . 3 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
6		eqid 2733	. . 3 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
7		eqid 2733	. . 3 ⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}
8		eqid 2733	. . 3 ⊢ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}
9	1, 2, 3, 4, 5, 6, 7, 8	isgrlim2 47808	. 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 6914	. . . . . . . . . . . . . 14 ⊢ (iEdg‘𝐻) ∈ V
11		vex 3481	. . . . . . . . . . . . . 14 ⊢ ℎ ∈ V
12	10, 11	coex 7947	. . . . . . . . . . . . 13 ⊢ ((iEdg‘𝐻) ∘ ℎ) ∈ V
13		fvex 6914	. . . . . . . . . . . . . 14 ⊢ (iEdg‘𝐺) ∈ V
14	13	cnvex 7942	. . . . . . . . . . . . 13 ⊢ ^◡(iEdg‘𝐺) ∈ V
15	12, 14	coex 7947	. . . . . . . . . . . 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 29186	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺))
18	17	ad2antrr 725	. . . . . . . . . . . . . 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 770	. . . . . . . . . . . . . 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 29186	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ USPGraph → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1-onto→(Edg‘𝐻))
21	20	ad2antlr 726	. . . . . . . . . . . . . 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 4090	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)
23		ssrab2 4090	. . . . . . . . . . . . . . . 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 46975	. . . . . . . . . . . . . 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 1371	. . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . 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 47813	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → 𝐾 = ((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}))
32	31	ad2antrr 725	. . . . . . . . . . . . . 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 47813	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ USPGraph → 𝐿 = ((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
36	35	ad2antlr 726	. . . . . . . . . . . . . 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 6837	. . . . . . . . . . . . 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 766	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → 𝐺 ∈ USPGraph)
40		simprr 772	. . . . . . . . . . . . . 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 47815	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ USPGraph ∧ ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) → (𝑒 ∈ 𝐾 → (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
42	39, 19, 40, 41	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (𝑒 ∈ 𝐾 → (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
43	42	ralrimiv 3141	. . . . . . . . . . . 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 6831	. . . . . . . . . . . 12 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → (𝑔:𝐾–1-1-onto→𝐿 ↔ (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):𝐾–1-1-onto→𝐿))
46		fveq1 6900	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → (𝑔‘𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒))
47	46	eqeq2d 2744	. . . . . . . . . . . . 13 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
48	47	ralbidv 3174	. . . . . . . . . . . 12 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → (∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
49	45, 48	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → ((𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)) ↔ ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒))))
50	16, 44, 49	spcedv 3598	. . . . . . . . . 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 1929	. . . . . . . 8 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) → ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
53	10	cnvex 7942	. . . . . . . . . . . . . 14 ⊢ ^◡(iEdg‘𝐻) ∈ V
54		vex 3481	. . . . . . . . . . . . . 14 ⊢ 𝑔 ∈ V
55	53, 54	coex 7947	. . . . . . . . . . . . 13 ⊢ (^◡(iEdg‘𝐻) ∘ 𝑔) ∈ V
56	55, 13	coex 7947	. . . . . . . . . . . 12 ⊢ ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) ∈ V
57	56	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) ∈ V)
58	17	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺))
59		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → 𝑔:𝐾–1-1-onto→𝐿)
60	20	ad2antlr 726	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐻):dom (iEdg‘𝐻)–1-1-onto→(Edg‘𝐻))
61	29	rabeqi 3446	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁} = {𝑥 ∈ (Edg‘𝐺) ∣ 𝑥 ⊆ 𝑁}
62	30, 61	eqtri 2761	. . . . . . . . . . . . . . . . 17 ⊢ 𝐾 = {𝑥 ∈ (Edg‘𝐺) ∣ 𝑥 ⊆ 𝑁}
63	62	ssrab3 4092	. . . . . . . . . . . . . . . 16 ⊢ 𝐾 ⊆ (Edg‘𝐺)
64	33	rabeqi 3446	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀} = {𝑥 ∈ (Edg‘𝐻) ∣ 𝑥 ⊆ 𝑀}
65	34, 64	eqtri 2761	. . . . . . . . . . . . . . . . 17 ⊢ 𝐿 = {𝑥 ∈ (Edg‘𝐻) ∣ 𝑥 ⊆ 𝑀}
66	65	ssrab3 4092	. . . . . . . . . . . . . . . 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 46976	. . . . . . . . . . . . . 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 1371	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):(^◡(iEdg‘𝐺) “ 𝐾)–1-1-onto→(^◡(iEdg‘𝐻) “ 𝐿))
71		eqidd 2734	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)))
72	3, 29, 30	uspgrlimlem2 47814	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (^◡(iEdg‘𝐺) “ 𝐾) = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})
73	72	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐺) “ 𝐾) = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})
74	4, 33, 34	uspgrlimlem2 47814	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ USPGraph → (^◡(iEdg‘𝐻) “ 𝐿) = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})
75	74	ad2antlr 726	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐻) “ 𝐿) = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})
76	71, 73, 75	f1oeq123d 6837	. . . . . . . . . . . . 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 6901	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑖 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝑖))
79	78	sseq1d 4027	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑖 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
80	79	elrab 3695	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ↔ (𝑖 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
81	1, 2, 3, 4, 29, 33, 30, 34	uspgrlimlem4 47816	. . . . . . . . . . . . . 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 3141	. . . . . . . . . . . 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 6831	. . . . . . . . . . . 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 6900	. . . . . . . . . . . . . . 15 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → (ℎ‘𝑖) = (((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))
87	86	fveq2d 6905	. . . . . . . . . . . . . 14 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(ℎ‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖)))
88	87	eqeq2d 2744	. . . . . . . . . . . . 13 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → ((𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))))
89	88	ralbidv 3174	. . . . . . . . . . . 12 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))))
90	85, 89	anbi12d 631	. . . . . . . . . . 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 3598	. . . . . . . . . 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 1929	. . . . . . . 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 629	. . . . . 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 1917	. . . . 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 3174	. . . 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 629	. . 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 1130	. 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 1085 = wceq 1535 ∃wex 1774 ∈ wcel 2104 ∀wral 3057 {crab 3432 Vcvv 3477 ⊆ wss 3963 ^◡ccnv 5682 dom cdm 5683 “ cima 5686 ∘ ccom 5687 –1-1-onto→wf1o 6557 ‘cfv 6558 (class class class)co 7425 Vtxcvtx 29009 iEdgciedg 29010 Edgcedg 29060 USPGraphcuspgr 29161 ClNeighbVtx cclnbgr 47693 GraphLocIso cgrlim 47801

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1963 ax-7 2003 ax-8 2106 ax-9 2114 ax-10 2137 ax-11 2153 ax-12 2173 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5366 ax-pr 5430 ax-un 7747

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1087 df-tru 1538 df-fal 1548 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2536 df-eu 2565 df-clab 2711 df-cleq 2725 df-clel 2812 df-nfc 2888 df-ne 2937 df-ral 3058 df-rex 3067 df-rab 3433 df-v 3479 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4915 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5689 df-rel 5690 df-cnv 5691 df-co 5692 df-dm 5693 df-rn 5694 df-res 5695 df-ima 5696 df-suc 6386 df-iota 6510 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-ov 7428 df-oprab 7429 df-mpo 7430 df-1st 8007 df-2nd 8008 df-1o 8499 df-map 8861 df-vtx 29011 df-iedg 29012 df-edg 29061 df-uspgr 29163 df-clnbgr 47694 df-isubgr 47734 df-grim 47749 df-gric 47752 df-grlim 47803

This theorem is referenced by: usgrlimprop 47818

W3C validator