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 49363

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 49354). (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-1onto𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁⟶1-1onto𝑀 ∧ ∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))))

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 2763	. . 3 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
6		eqid 2763	. . 3 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
7		eqid 2763	. . 3 ⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}
8		eqid 2763	. . 3 ⊢ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}
9	1, 2, 3, 4, 5, 6, 7, 8	isgrlim2 49354	. 2 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ (𝐹:𝑉⟶1-1onto𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁⟶1-1onto𝑀 ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))))))
10		fvex 6929	. . . . . . . . . . . . . 14 ⊢ (iEdg‘𝐻) ∈ V
11		vex 3458	. . . . . . . . . . . . . 14 ⊢ ℎ ∈ V
12	10, 11	coex 7976	. . . . . . . . . . . . 13 ⊢ ((iEdg‘𝐻) ∘ ℎ) ∈ V
13		fvex 6929	. . . . . . . . . . . . . 14 ⊢ (iEdg‘𝐺) ∈ V
14	13	cnvex 7971	. . . . . . . . . . . . 13 ⊢ ^◡(iEdg‘𝐺) ∈ V
15	12, 14	coex 7976	. . . . . . . . . . . 12 ⊢ (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) ∈ V
16	15	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) ∈ V)
17	5	uspgrf1oedg 29811	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶1-1onto(Edg‘𝐺))
18	17	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶1-1onto(Edg‘𝐺))
19		simprl 783	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})
20	6	uspgrf1oedg 29811	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ USPGraph → (iEdg‘𝐻):dom (iEdg‘𝐻)⟶1-1onto(Edg‘𝐻))
21	20	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (iEdg‘𝐻):dom (iEdg‘𝐻)⟶1-1onto(Edg‘𝐻))
22		ssrab2 4008	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)
23		ssrab2 4008	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ⊆ dom (iEdg‘𝐻)
24	22, 23	pm3.2i 476	. . . . . . . . . . . . . . 15 ⊢ ({𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ⊆ dom (iEdg‘𝐻))
25	24	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ({𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ⊆ dom (iEdg‘𝐻)))
26		3f1oss1 48418	. . . . . . . . . . . . . 14 ⊢ ((((iEdg‘𝐺):dom (iEdg‘𝐺)⟶1-1onto(Edg‘𝐺) ∧ ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ (iEdg‘𝐻):dom (iEdg‘𝐻)⟶1-1onto(Edg‘𝐻)) ∧ ({𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ⊆ dom (iEdg‘𝐻))) → (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})⟶1-1onto((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
27	18, 19, 21, 25, 26	syl31anc 1401	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})⟶1-1onto((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
28		eqidd 2764	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ 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 49359	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → 𝐾 = ((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}))
32	31	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ 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 49359	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ USPGraph → 𝐿 = ((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
36	35	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → 𝐿 = ((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
37	28, 32, 36	f1oeq123d 6848	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):𝐾⟶1-1onto𝐿 ↔ (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):((iEdg‘𝐺) “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})⟶1-1onto((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})))
38	27, 37	mpbird 260	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):𝐾⟶1-1onto𝐿)
39		simpll 779	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → 𝐺 ∈ USPGraph)
40		simprr 785	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))
41	1, 2, 3, 4, 29, 33, 30, 34	uspgrlimlem3 49361	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ USPGraph ∧ ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) → (𝑒 ∈ 𝐾 → (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
42	39, 19, 40, 41	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → (𝑒 ∈ 𝐾 → (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
43	42	ralrimiv 3157	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒))
44	38, 43	jca 521	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
45		f1oeq1 6842	. . . . . . . . . . . 12 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → (𝑔:𝐾⟶1-1onto𝐿 ↔ (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):𝐾⟶1-1onto𝐿))
46		fveq1 6915	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → (𝑔‘𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒))
47	46	eqeq2d 2774	. . . . . . . . . . . . 13 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
48	47	ralbidv 3189	. . . . . . . . . . . 12 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → (∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒)))
49	45, 48	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑔 = (((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)) → ((𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)) ↔ ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺)):𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ^◡(iEdg‘𝐺))‘𝑒))))
50	16, 44, 49	spcedv 3556	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) → ∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)))
51	50	ex 418	. . . . . . . . 9 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → ((ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) → ∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
52	51	exlimdv 1968	. . . . . . . 8 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) → ∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
53	10	cnvex 7971	. . . . . . . . . . . . . 14 ⊢ ^◡(iEdg‘𝐻) ∈ V
54		vex 3458	. . . . . . . . . . . . . 14 ⊢ 𝑔 ∈ V
55	53, 54	coex 7976	. . . . . . . . . . . . 13 ⊢ (^◡(iEdg‘𝐻) ∘ 𝑔) ∈ V
56	55, 13	coex 7976	. . . . . . . . . . . 12 ⊢ ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) ∈ V
57	56	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) ∈ V)
58	17	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶1-1onto(Edg‘𝐺))
59		simprl 783	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → 𝑔:𝐾⟶1-1onto𝐿)
60	20	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐻):dom (iEdg‘𝐻)⟶1-1onto(Edg‘𝐻))
61	29	rabeqi 3429	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁} = {𝑥 ∈ (Edg‘𝐺) ∣ 𝑥 ⊆ 𝑁}
62	30, 61	eqtri 2786	. . . . . . . . . . . . . . . . 17 ⊢ 𝐾 = {𝑥 ∈ (Edg‘𝐺) ∣ 𝑥 ⊆ 𝑁}
63	62	ssrab3 4010	. . . . . . . . . . . . . . . 16 ⊢ 𝐾 ⊆ (Edg‘𝐺)
64	33	rabeqi 3429	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀} = {𝑥 ∈ (Edg‘𝐻) ∣ 𝑥 ⊆ 𝑀}
65	34, 64	eqtri 2786	. . . . . . . . . . . . . . . . 17 ⊢ 𝐿 = {𝑥 ∈ (Edg‘𝐻) ∣ 𝑥 ⊆ 𝑀}
66	65	ssrab3 4010	. . . . . . . . . . . . . . . 16 ⊢ 𝐿 ⊆ (Edg‘𝐻)
67	63, 66	pm3.2i 476	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ⊆ (Edg‘𝐺) ∧ 𝐿 ⊆ (Edg‘𝐻))
68	67	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝐾 ⊆ (Edg‘𝐺) ∧ 𝐿 ⊆ (Edg‘𝐻)))
69		3f1oss2 48419	. . . . . . . . . . . . . 14 ⊢ ((((iEdg‘𝐺):dom (iEdg‘𝐺)⟶1-1onto(Edg‘𝐺) ∧ 𝑔:𝐾⟶1-1onto𝐿 ∧ (iEdg‘𝐻):dom (iEdg‘𝐻)⟶1-1onto(Edg‘𝐻)) ∧ (𝐾 ⊆ (Edg‘𝐺) ∧ 𝐿 ⊆ (Edg‘𝐻))) → ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):(^◡(iEdg‘𝐺) “ 𝐾)⟶1-1onto(^◡(iEdg‘𝐻) “ 𝐿))
70	58, 59, 60, 68, 69	syl31anc 1401	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):(^◡(iEdg‘𝐺) “ 𝐾)⟶1-1onto(^◡(iEdg‘𝐻) “ 𝐿))
71		eqidd 2764	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)))
72	3, 29, 30	uspgrlimlem2 49360	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (^◡(iEdg‘𝐺) “ 𝐾) = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})
73	72	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐺) “ 𝐾) = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})
74	4, 33, 34	uspgrlimlem2 49360	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ USPGraph → (^◡(iEdg‘𝐻) “ 𝐿) = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})
75	74	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐻) “ 𝐿) = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})
76	71, 73, 75	f1oeq123d 6848	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):(^◡(iEdg‘𝐺) “ 𝐾)⟶1-1onto(^◡(iEdg‘𝐻) “ 𝐿) ↔ ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
77	70, 76	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})
78		fveq2 6916	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑖 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝑖))
79	78	sseq1d 3944	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑖 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
80	79	elrab 3648	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ↔ (𝑖 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
81	1, 2, 3, 4, 29, 33, 30, 34	uspgrlimlem4 49362	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((𝑖 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁) → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))))
82	80, 81	biimtrid 245	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))))
83	82	ralrimiv 3157	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖)))
84	77, 83	jca 521	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))))
85		f1oeq1 6842	. . . . . . . . . . . 12 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ↔ ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
86		fveq1 6915	. . . . . . . . . . . . . . 15 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → (ℎ‘𝑖) = (((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))
87	86	fveq2d 6920	. . . . . . . . . . . . . 14 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(ℎ‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖)))
88	87	eqeq2d 2774	. . . . . . . . . . . . 13 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → ((𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))))
89	88	ralbidv 3189	. . . . . . . . . . . 12 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))))
90	85, 89	anbi12d 644	. . . . . . . . . . 11 ⊢ (ℎ = ((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)) → ((ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) ↔ (((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺)):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((^◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖)))))
91	57, 84, 90	spcedv 3556	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))
92	91	ex 418	. . . . . . . . 9 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → ((𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))))
93	92	exlimdv 1968	. . . . . . . 8 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))))
94	52, 93	impbid 215	. . . . . . 7 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) ↔ ∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
95	94	anbi2d 642	. . . . . 6 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → ((𝑓:𝑁⟶1-1onto𝑀 ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) ↔ (𝑓:𝑁⟶1-1onto𝑀 ∧ ∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
96	95	exbidv 1956	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (∃𝑓(𝑓:𝑁⟶1-1onto𝑀 ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) ↔ ∃𝑓(𝑓:𝑁⟶1-1onto𝑀 ∧ ∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
97	96	ralbidv 3189	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁⟶1-1onto𝑀 ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) ↔ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁⟶1-1onto𝑀 ∧ ∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
98	97	anbi2d 642	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → ((𝐹:𝑉⟶1-1onto𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁⟶1-1onto𝑀 ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))) ↔ (𝐹:𝑉⟶1-1onto𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁⟶1-1onto𝑀 ∧ ∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))))
99	98	3adant3 1150	. 2 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑍) → ((𝐹:𝑉⟶1-1onto𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁⟶1-1onto𝑀 ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶1-1onto{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))) ↔ (𝐹:𝑉⟶1-1onto𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁⟶1-1onto𝑀 ∧ ∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))))
100	9, 99	bitrd 282	1 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ (𝐹:𝑉⟶1-1onto𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁⟶1-1onto𝑀 ∧ ∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2147 ∀wral 3080 {crab 3416 Vcvv 3454 ⊆ wss 3900 ^◡ccnv 5657 dom cdm 5658 “ cima 5661 ∘ ccom 5662 ⟶1-1ontowf1o 6565 ‘cfv 6566 (class class class)co 7451 Vtxcvtx 29631 iEdgciedg 29632 Edgcedg 29682 USPGraphcuspgr 29786 ClNeighbVtx cclnbgr 49189 GraphLocIso cgrlim 49347

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-id 5553 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-ov 7454 df-oprab 7455 df-mpo 7456 df-1st 8035 df-2nd 8036 df-1o 8514 df-map 8887 df-vtx 29633 df-iedg 29634 df-edg 29683 df-uspgr 29788 df-clnbgr 49190 df-isubgr 49232 df-grim 49249 df-gric 49252 df-grlim 49349

This theorem is used by: usgrlimprop 49364

W3C validator