Theorem isuspgrim0lem 49196

Description: An isomorphism of simple pseudographs is a bijection between their vertices which induces a bijection between their edges. (Contributed by AV, 21-Apr-2025.)

Hypotheses

Ref	Expression
isusgrim.v	⊢ 𝑉 = (Vtx‘𝐺)
isusgrim.w	⊢ 𝑊 = (Vtx‘𝐻)
isusgrim.e	⊢ 𝐸 = (Edg‘𝐺)
isusgrim.d	⊢ 𝐷 = (Edg‘𝐻)
isuspgrim0lem.i	⊢ 𝐼 = (iEdg‘𝐺)
isuspgrim0lem.j	⊢ 𝐽 = (iEdg‘𝐻)
isuspgrim0lem.m	⊢ 𝑀 = (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))
isuspgrim0lem.n	⊢ 𝑁 = (𝑥 ∈ dom 𝐼 ↦ (◡𝐽‘(𝑀‘(𝐼‘𝑥))))

Assertion

Ref	Expression
isuspgrim0lem	⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → (𝑁:dom 𝐼⟶1-1ontodom 𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖))))

Distinct variable groups:   𝐷,𝑖   𝑖,𝐸,𝑥   𝑖,𝐹,𝑥   𝑖,𝐺   𝑖,𝐻   𝑖,𝑉   𝑖,𝑊   𝑖,𝑋   𝑥,𝐷   𝑥,𝐺   𝑥,𝐻   𝑖,𝐼,𝑥   𝑖,𝐽,𝑥   𝑖,𝑀,𝑥   𝑖,𝑁   𝑥,𝑉   𝑥,𝑊   𝑥,𝑋

Allowed substitution hint:   𝑁(𝑥)

Proof of Theorem isuspgrim0lem

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		isuspgrim0lem.j	. . . . . . . 8 ⊢ 𝐽 = (iEdg‘𝐻)
2	1	uspgrf1oedg 29784	. . . . . . 7 ⊢ (𝐻 ∈ USPGraph → 𝐽:dom 𝐽⟶1-1onto(Edg‘𝐻))
3	2	3ad2ant2 1152	. . . . . 6 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐽:dom 𝐽⟶1-1onto(Edg‘𝐻))
4	3	ad2antrr 739	. . . . 5 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → 𝐽:dom 𝐽⟶1-1onto(Edg‘𝐻))
5		f1of 6846	. . . . . . . . 9 ⊢ (𝑀:𝐸⟶1-1onto𝐷 → 𝑀:𝐸⟶𝐷)
6	5	adantl 487	. . . . . . . 8 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → 𝑀:𝐸⟶𝐷)
7	6	adantr 486	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑥 ∈ dom 𝐼) → 𝑀:𝐸⟶𝐷)
8		uspgruhgr 29795	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
9		isuspgrim0lem.i	. . . . . . . . . . . . 13 ⊢ 𝐼 = (iEdg‘𝐺)
10	9	uhgrfun 29674	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ UHGraph → Fun 𝐼)
11	8, 10	syl 18	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USPGraph → Fun 𝐼)
12		isusgrim.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (Edg‘𝐺)
13		edgval 29657	. . . . . . . . . . . . . 14 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
14	9	eqcomi 2772	. . . . . . . . . . . . . . 15 ⊢ (iEdg‘𝐺) = 𝐼
15	14	rneqi 5926	. . . . . . . . . . . . . 14 ⊢ ran (iEdg‘𝐺) = ran 𝐼
16	12, 13, 15	3eqtri 2790	. . . . . . . . . . . . 13 ⊢ 𝐸 = ran 𝐼
17		feq3 6711	. . . . . . . . . . . . 13 ⊢ (𝐸 = ran 𝐼 → (𝐼:dom 𝐼⟶𝐸 ↔ 𝐼:dom 𝐼⟶ran 𝐼))
18	16, 17	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝐼:dom 𝐼⟶𝐸 ↔ 𝐼:dom 𝐼⟶ran 𝐼)
19		fdmrn 6763	. . . . . . . . . . . 12 ⊢ (Fun 𝐼 ↔ 𝐼:dom 𝐼⟶ran 𝐼)
20	18, 19	bitr4i 281	. . . . . . . . . . 11 ⊢ (𝐼:dom 𝐼⟶𝐸 ↔ Fun 𝐼)
21	11, 20	sylibr 237	. . . . . . . . . 10 ⊢ (𝐺 ∈ USPGraph → 𝐼:dom 𝐼⟶𝐸)
22	21	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐼:dom 𝐼⟶𝐸)
23	22	ad2antrr 739	. . . . . . . 8 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → 𝐼:dom 𝐼⟶𝐸)
24	23	ffvelcdmda 7108	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
25	7, 24	ffvelcdmd 7109	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ 𝐷)
26		isusgrim.d	. . . . . 6 ⊢ 𝐷 = (Edg‘𝐻)
27	25, 26	eleqtrdi 2874	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻))
28		f1ocnvdm 7316	. . . . 5 ⊢ ((𝐽:dom 𝐽⟶1-1onto(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻)) → (◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
29	4, 27, 28	syl2an2r 698	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑥 ∈ dom 𝐼) → (◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
30	29	ralrimiva 3158	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → ∀𝑥 ∈ dom 𝐼(◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
31		2fveq3 6913	. . . . . . . . 9 ⊢ (𝑥 = (◡𝐼‘(◡𝑀‘(𝐽‘𝑖))) → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘(◡𝐼‘(◡𝑀‘(𝐽‘𝑖))))))
32	31	eqeq2d 2774	. . . . . . . 8 ⊢ (𝑥 = (◡𝐼‘(◡𝑀‘(𝐽‘𝑖))) → ((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘(◡𝐼‘(◡𝑀‘(𝐽‘𝑖)))))))
33	9	uspgrf1oedg 29784	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USPGraph → 𝐼:dom 𝐼⟶1-1onto(Edg‘𝐺))
34	33	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐼:dom 𝐼⟶1-1onto(Edg‘𝐺))
35	34	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → 𝐼:dom 𝐼⟶1-1onto(Edg‘𝐺))
36		f1oeq2 6835	. . . . . . . . . . . 12 ⊢ (𝐸 = (Edg‘𝐺) → (𝑀:𝐸⟶1-1onto𝐷 ↔ 𝑀:(Edg‘𝐺)⟶1-1onto𝐷))
37	12, 36	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑀:𝐸⟶1-1onto𝐷 ↔ 𝑀:(Edg‘𝐺)⟶1-1onto𝐷)
38	37	bilani 510	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → 𝑀:(Edg‘𝐺)⟶1-1onto𝐷)
39		f1oeq3 6836	. . . . . . . . . . . . . 14 ⊢ (𝐷 = (Edg‘𝐻) → (𝐽:dom 𝐽⟶1-1onto𝐷 ↔ 𝐽:dom 𝐽⟶1-1onto(Edg‘𝐻)))
40	26, 39	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐽:dom 𝐽⟶1-1onto𝐷 ↔ 𝐽:dom 𝐽⟶1-1onto(Edg‘𝐻))
41	4, 40	sylibr 237	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → 𝐽:dom 𝐽⟶1-1onto𝐷)
42		f1of 6846	. . . . . . . . . . . 12 ⊢ (𝐽:dom 𝐽⟶1-1onto𝐷 → 𝐽:dom 𝐽⟶𝐷)
43	41, 42	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → 𝐽:dom 𝐽⟶𝐷)
44	43	ffvelcdmda 7108	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐽‘𝑖) ∈ 𝐷)
45		f1ocnvdm 7316	. . . . . . . . . 10 ⊢ ((𝑀:(Edg‘𝐺)⟶1-1onto𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
46	38, 44, 45	syl2an2r 698	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → (◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
47		f1ocnvdm 7316	. . . . . . . . 9 ⊢ ((𝐼:dom 𝐼⟶1-1onto(Edg‘𝐺) ∧ (◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺)) → (◡𝐼‘(◡𝑀‘(𝐽‘𝑖))) ∈ dom 𝐼)
48	35, 46, 47	syl2an2r 698	. . . . . . . 8 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → (◡𝐼‘(◡𝑀‘(𝐽‘𝑖))) ∈ dom 𝐼)
49		simpll1 1231	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → 𝐺 ∈ USPGraph)
50	49, 33	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → 𝐼:dom 𝐼⟶1-1onto(Edg‘𝐺))
51		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → 𝑀:𝐸⟶1-1onto𝐷)
52		f1ocnvdm 7316	. . . . . . . . . . . . 13 ⊢ ((𝑀:𝐸⟶1-1onto𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (◡𝑀‘(𝐽‘𝑖)) ∈ 𝐸)
53	51, 44, 52	syl2an2r 698	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → (◡𝑀‘(𝐽‘𝑖)) ∈ 𝐸)
54	53, 12	eleqtrdi 2874	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → (◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
55		f1ocnvfv2 7308	. . . . . . . . . . 11 ⊢ ((𝐼:dom 𝐼⟶1-1onto(Edg‘𝐺) ∧ (◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺)) → (𝐼‘(◡𝐼‘(◡𝑀‘(𝐽‘𝑖)))) = (◡𝑀‘(𝐽‘𝑖)))
56	50, 54, 55	syl2an2r 698	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐼‘(◡𝐼‘(◡𝑀‘(𝐽‘𝑖)))) = (◡𝑀‘(𝐽‘𝑖)))
57	56	fveq2d 6912	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝑀‘(𝐼‘(◡𝐼‘(◡𝑀‘(𝐽‘𝑖))))) = (𝑀‘(◡𝑀‘(𝐽‘𝑖))))
58		f1ocnvfv2 7308	. . . . . . . . . 10 ⊢ ((𝑀:𝐸⟶1-1onto𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (𝑀‘(◡𝑀‘(𝐽‘𝑖))) = (𝐽‘𝑖))
59	51, 44, 58	syl2an2r 698	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝑀‘(◡𝑀‘(𝐽‘𝑖))) = (𝐽‘𝑖))
60	57, 59	eqtr2d 2799	. . . . . . . 8 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐽‘𝑖) = (𝑀‘(𝐼‘(◡𝐼‘(◡𝑀‘(𝐽‘𝑖))))))
61	32, 48, 60	rspcedvdw 3583	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)))
62		eqtr2 2784	. . . . . . . . 9 ⊢ (((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)))
63		f1of1 6845	. . . . . . . . . . . . 13 ⊢ (𝑀:𝐸⟶1-1onto𝐷 → 𝑀:𝐸⟶1-1𝐷)
64	63	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → 𝑀:𝐸⟶1-1𝐷)
65	64	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝑀:𝐸⟶1-1𝐷)
66	9	iedgedg 29658	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐼 ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ (Edg‘𝐺))
67	11, 66	sylan 592	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ (Edg‘𝐺))
68	67, 12	eleqtrrdi 2875	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
69	68	ex 418	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (𝑥 ∈ dom 𝐼 → (𝐼‘𝑥) ∈ 𝐸))
70	9	iedgedg 29658	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐼 ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ (Edg‘𝐺))
71	11, 70	sylan 592	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ (Edg‘𝐺))
72	71, 12	eleqtrrdi 2875	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ 𝐸)
73	72	ex 418	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (𝑦 ∈ dom 𝐼 → (𝐼‘𝑦) ∈ 𝐸))
74	69, 73	anim12d 621	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ USPGraph → ((𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)))
75	74	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → ((𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)))
76	75	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → ((𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)))
77	76	imp 412	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸))
78		f1fveq 7289	. . . . . . . . . . 11 ⊢ ((𝑀:𝐸⟶1-1𝐷 ∧ ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)) → ((𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)) ↔ (𝐼‘𝑥) = (𝐼‘𝑦)))
79	65, 77, 78	syl2an2r 698	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)) ↔ (𝐼‘𝑥) = (𝐼‘𝑦)))
80		f1of1 6845	. . . . . . . . . . . . . 14 ⊢ (𝐼:dom 𝐼⟶1-1onto(Edg‘𝐺) → 𝐼:dom 𝐼⟶1-1(Edg‘𝐺))
81	33, 80	syl 18	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ USPGraph → 𝐼:dom 𝐼⟶1-1(Edg‘𝐺))
82	81	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐼:dom 𝐼⟶1-1(Edg‘𝐺))
83	82	ad3antrrr 743	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐼:dom 𝐼⟶1-1(Edg‘𝐺))
84		f1veqaeq 7283	. . . . . . . . . . 11 ⊢ ((𝐼:dom 𝐼⟶1-1(Edg‘𝐺) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝐼‘𝑥) = (𝐼‘𝑦) → 𝑥 = 𝑦))
85	83, 84	sylan 592	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝐼‘𝑥) = (𝐼‘𝑦) → 𝑥 = 𝑦))
86	79, 85	sylbid 243	. . . . . . . . 9 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)) → 𝑥 = 𝑦))
87	62, 86	syl5 35	. . . . . . . 8 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → (((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → 𝑥 = 𝑦))
88	87	ralrimivva 3209	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∀𝑥 ∈ dom 𝐼∀𝑦 ∈ dom 𝐼(((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → 𝑥 = 𝑦))
89		2fveq3 6913	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)))
90	89	eqeq2d 2774	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))))
91	90	reu4 3692	. . . . . . 7 ⊢ (∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (∃𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ ∀𝑥 ∈ dom 𝐼∀𝑦 ∈ dom 𝐼(((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → 𝑥 = 𝑦)))
92	61, 88, 91	sylanbrc 595	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)))
93	3	ad3antrrr 743	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐽:dom 𝐽⟶1-1onto(Edg‘𝐻))
94	6	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝑀:𝐸⟶𝐷)
95	22	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐼:dom 𝐼⟶𝐸)
96	95	ffvelcdmda 7108	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
97	94, 96	ffvelcdmd 7109	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ 𝐷)
98	97, 26	eleqtrdi 2874	. . . . . . . . 9 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻))
99		f1ocnvfv2 7308	. . . . . . . . 9 ⊢ ((𝐽:dom 𝐽⟶1-1onto(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻)) → (𝐽‘(◡𝐽‘(𝑀‘(𝐼‘𝑥)))) = (𝑀‘(𝐼‘𝑥)))
100	93, 98, 99	syl2an2r 698	. . . . . . . 8 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝐽‘(◡𝐽‘(𝑀‘(𝐼‘𝑥)))) = (𝑀‘(𝐼‘𝑥)))
101	100	eqeq2d 2774	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → ((𝐽‘𝑖) = (𝐽‘(◡𝐽‘(𝑀‘(𝐼‘𝑥)))) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥))))
102	101	reubidva 3383	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → (∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝐽‘(◡𝐽‘(𝑀‘(𝐼‘𝑥)))) ↔ ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥))))
103	92, 102	mpbird 260	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝐽‘(◡𝐽‘(𝑀‘(𝐼‘𝑥)))))
104	4	ad2antrr 739	. . . . . . . 8 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝐽:dom 𝐽⟶1-1onto(Edg‘𝐻))
105		f1of1 6845	. . . . . . . 8 ⊢ (𝐽:dom 𝐽⟶1-1onto(Edg‘𝐻) → 𝐽:dom 𝐽⟶1-1(Edg‘𝐻))
106	104, 105	syl 18	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝐽:dom 𝐽⟶1-1(Edg‘𝐻))
107		simplr 781	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝑖 ∈ dom 𝐽)
108	29	adantlr 728	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
109		f1fveq 7289	. . . . . . . 8 ⊢ ((𝐽:dom 𝐽⟶1-1(Edg‘𝐻) ∧ (𝑖 ∈ dom 𝐽 ∧ (◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)) → ((𝐽‘𝑖) = (𝐽‘(◡𝐽‘(𝑀‘(𝐼‘𝑥)))) ↔ 𝑖 = (◡𝐽‘(𝑀‘(𝐼‘𝑥)))))
110	109	bicomd 226	. . . . . . 7 ⊢ ((𝐽:dom 𝐽⟶1-1(Edg‘𝐻) ∧ (𝑖 ∈ dom 𝐽 ∧ (◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)) → (𝑖 = (◡𝐽‘(𝑀‘(𝐼‘𝑥))) ↔ (𝐽‘𝑖) = (𝐽‘(◡𝐽‘(𝑀‘(𝐼‘𝑥))))))
111	106, 107, 108, 110	syl12anc 850	. . . . . 6 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑖 = (◡𝐽‘(𝑀‘(𝐼‘𝑥))) ↔ (𝐽‘𝑖) = (𝐽‘(◡𝐽‘(𝑀‘(𝐼‘𝑥))))))
112	111	reubidva 3383	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → (∃!𝑥 ∈ dom 𝐼 𝑖 = (◡𝐽‘(𝑀‘(𝐼‘𝑥))) ↔ ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝐽‘(◡𝐽‘(𝑀‘(𝐼‘𝑥))))))
113	103, 112	mpbird 260	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃!𝑥 ∈ dom 𝐼 𝑖 = (◡𝐽‘(𝑀‘(𝐼‘𝑥))))
114	113	ralrimiva 3158	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → ∀𝑖 ∈ dom 𝐽∃!𝑥 ∈ dom 𝐼 𝑖 = (◡𝐽‘(𝑀‘(𝐼‘𝑥))))
115		isuspgrim0lem.n	. . . 4 ⊢ 𝑁 = (𝑥 ∈ dom 𝐼 ↦ (◡𝐽‘(𝑀‘(𝐼‘𝑥))))
116	115	f1ompt 7135	. . 3 ⊢ (𝑁:dom 𝐼⟶1-1ontodom 𝐽 ↔ (∀𝑥 ∈ dom 𝐼(◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽 ∧ ∀𝑖 ∈ dom 𝐽∃!𝑥 ∈ dom 𝐼 𝑖 = (◡𝐽‘(𝑀‘(𝐼‘𝑥)))))
117	30, 114, 116	sylanbrc 595	. 2 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → 𝑁:dom 𝐼⟶1-1ontodom 𝐽)
118		2fveq3 6913	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑖)))
119	118	fveq2d 6912	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (◡𝐽‘(𝑀‘(𝐼‘𝑥))) = (◡𝐽‘(𝑀‘(𝐼‘𝑖))))
120	119	adantl 487	. . . . . 6 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑥 = 𝑖) → (◡𝐽‘(𝑀‘(𝐼‘𝑥))) = (◡𝐽‘(𝑀‘(𝐼‘𝑖))))
121		simpr 490	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) → 𝑖 ∈ dom 𝐼)
122		fvexd 6923	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) → (◡𝐽‘(𝑀‘(𝐼‘𝑖))) ∈ V)
123	115, 120, 121, 122	fvmptd2 7025	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑁‘𝑖) = (◡𝐽‘(𝑀‘(𝐼‘𝑖))))
124	123	fveq2d 6912	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐽‘(𝑁‘𝑖)) = (𝐽‘(◡𝐽‘(𝑀‘(𝐼‘𝑖)))))
125	6	adantr 486	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) → 𝑀:𝐸⟶𝐷)
126	23	ffvelcdmda 7108	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) ∈ 𝐸)
127	125, 126	ffvelcdmd 7109	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) ∈ 𝐷)
128	127, 26	eleqtrdi 2874	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) ∈ (Edg‘𝐻))
129		f1ocnvfv2 7308	. . . . 5 ⊢ ((𝐽:dom 𝐽⟶1-1onto(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑖)) ∈ (Edg‘𝐻)) → (𝐽‘(◡𝐽‘(𝑀‘(𝐼‘𝑖)))) = (𝑀‘(𝐼‘𝑖)))
130	4, 128, 129	syl2an2r 698	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐽‘(◡𝐽‘(𝑀‘(𝐼‘𝑖)))) = (𝑀‘(𝐼‘𝑖)))
131		isuspgrim0lem.m	. . . . 5 ⊢ 𝑀 = (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))
132		simpr 490	. . . . . 6 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑥 = (𝐼‘𝑖)) → 𝑥 = (𝐼‘𝑖))
133	132	imaeq2d 6064	. . . . 5 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑥 = (𝐼‘𝑖)) → (𝐹 “ 𝑥) = (𝐹 “ (𝐼‘𝑖)))
134		simp3 1156	. . . . . . 7 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐹 ∈ 𝑋)
135	134	ad3antrrr 743	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) → 𝐹 ∈ 𝑋)
136	135	imaexd 7952	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐹 “ (𝐼‘𝑖)) ∈ V)
137	131, 133, 126, 136	fvmptd2 7025	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
138	124, 130, 137	3eqtrd 2802	. . 3 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
139	138	ralrimiva 3158	. 2 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → ∀𝑖 ∈ dom 𝐼(𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
140	117, 139	jca 521	1 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉⟶1-1onto𝑊) ∧ 𝑀:𝐸⟶1-1onto𝐷) → (𝑁:dom 𝐼⟶1-1ontodom 𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090  ∃!wreu 3367  Vcvv 3454   ↦ cmpt 5189  ^◡ccnv 5654  dom cdm 5655  ran crn 5656   “ cima 5658  Fun wfun 6552  ⟶wf 6554  ⟶1-1wf1 6555  ⟶1-1ontowf1o 6557  ‘cfv 6558  Vtxcvtx 29604  iEdgciedg 29605  Edgcedg 29655  UHGraphcuhgr 29664  USPGraphcuspgr 29759

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 5252  ax-nul 5263  ax-pr 5395  ax-un 7775

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-rmo 3369  df-reu 3370  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 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-edg 29656  df-uhgr 29666  df-upgr 29690  df-uspgr 29761

This theorem is used by:  isuspgrim0  49197