isuspgrim0lem - Mathbox for Alexander van der Vekens

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

Theorem isuspgrim0lem 49084

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-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → (𝑁:dom 𝐼–1-1-onto→dom 𝐽 ∧ ∀𝑖 ∈ 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 29759	. . . . . . 7 ⊢ (𝐻 ∈ USPGraph → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
3	2	3ad2ant2 1152	. . . . . 6 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
4	3	ad2antrr 739	. . . . 5 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
5		f1of 6824	. . . . . . . . 9 ⊢ (𝑀:𝐸–1-1-onto→𝐷 → 𝑀:𝐸⟶𝐷)
6	5	adantl 487	. . . . . . . 8 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑀:𝐸⟶𝐷)
7	6	adantr 486	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → 𝑀:𝐸⟶𝐷)
8		uspgruhgr 29770	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
9		isuspgrim0lem.i	. . . . . . . . . . . . 13 ⊢ 𝐼 = (iEdg‘𝐺)
10	9	uhgrfun 29649	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ UHGraph → Fun 𝐼)
11	8, 10	syl 18	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USPGraph → Fun 𝐼)
12		isusgrim.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (Edg‘𝐺)
13		edgval 29632	. . . . . . . . . . . . . 14 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
14	9	eqcomi 2769	. . . . . . . . . . . . . . 15 ⊢ (iEdg‘𝐺) = 𝐼
15	14	rneqi 5918	. . . . . . . . . . . . . 14 ⊢ ran (iEdg‘𝐺) = ran 𝐼
16	12, 13, 15	3eqtri 2787	. . . . . . . . . . . . 13 ⊢ 𝐸 = ran 𝐼
17		feq3 6689	. . . . . . . . . . . . 13 ⊢ (𝐸 = ran 𝐼 → (𝐼:dom 𝐼⟶𝐸 ↔ 𝐼:dom 𝐼⟶ran 𝐼))
18	16, 17	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝐼:dom 𝐼⟶𝐸 ↔ 𝐼:dom 𝐼⟶ran 𝐼)
19		fdmrn 6741	. . . . . . . . . . . 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-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐼:dom 𝐼⟶𝐸)
24	23	ffvelcdmda 7084	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
25	7, 24	ffvelcdmd 7085	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ 𝐷)
26		isusgrim.d	. . . . . 6 ⊢ 𝐷 = (Edg‘𝐻)
27	25, 26	eleqtrdi 2870	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻))
28		f1ocnvdm 7293	. . . . 5 ⊢ ((𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻)) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
29	4, 27, 28	syl2an2r 698	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
30	29	ralrimiva 3154	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → ∀𝑥 ∈ dom 𝐼(^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
31		2fveq3 6890	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))))))
32	31	eqeq2d 2771	. . . . . . . 8 ⊢ (𝑥 = (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) → ((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖)))))))
33	9	uspgrf1oedg 29759	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USPGraph → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
34	33	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
35	34	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
36		f1oeq2 6813	. . . . . . . . . . . 12 ⊢ (𝐸 = (Edg‘𝐺) → (𝑀:𝐸–1-1-onto→𝐷 ↔ 𝑀:(Edg‘𝐺)–1-1-onto→𝐷))
37	12, 36	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑀:𝐸–1-1-onto→𝐷 ↔ 𝑀:(Edg‘𝐺)–1-1-onto→𝐷)
38	37	bilani 510	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑀:(Edg‘𝐺)–1-1-onto→𝐷)
39		f1oeq3 6814	. . . . . . . . . . . . . 14 ⊢ (𝐷 = (Edg‘𝐻) → (𝐽:dom 𝐽–1-1-onto→𝐷 ↔ 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻)))
40	26, 39	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐽:dom 𝐽–1-1-onto→𝐷 ↔ 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
41	4, 40	sylibr 237	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐽:dom 𝐽–1-1-onto→𝐷)
42		f1of 6824	. . . . . . . . . . . 12 ⊢ (𝐽:dom 𝐽–1-1-onto→𝐷 → 𝐽:dom 𝐽⟶𝐷)
43	41, 42	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐽:dom 𝐽⟶𝐷)
44	43	ffvelcdmda 7084	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐽‘𝑖) ∈ 𝐷)
45		f1ocnvdm 7293	. . . . . . . . . 10 ⊢ ((𝑀:(Edg‘𝐺)–1-1-onto→𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
46	38, 44, 45	syl2an2r 698	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
47		f1ocnvdm 7293	. . . . . . . . 9 ⊢ ((𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺) ∧ (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺)) → (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) ∈ dom 𝐼)
48	35, 46, 47	syl2an2r 698	. . . . . . . 8 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) ∈ dom 𝐼)
49		simpll1 1231	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐺 ∈ USPGraph)
50	49, 33	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
51		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑀:𝐸–1-1-onto→𝐷)
52		f1ocnvdm 7293	. . . . . . . . . . . . 13 ⊢ ((𝑀:𝐸–1-1-onto→𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (^◡𝑀‘(𝐽‘𝑖)) ∈ 𝐸)
53	51, 44, 52	syl2an2r 698	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝑀‘(𝐽‘𝑖)) ∈ 𝐸)
54	53, 12	eleqtrdi 2870	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
55		f1ocnvfv2 7285	. . . . . . . . . . 11 ⊢ ((𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺) ∧ (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺)) → (𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖)))) = (^◡𝑀‘(𝐽‘𝑖)))
56	50, 54, 55	syl2an2r 698	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖)))) = (^◡𝑀‘(𝐽‘𝑖)))
57	56	fveq2d 6889	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))))) = (𝑀‘(^◡𝑀‘(𝐽‘𝑖))))
58		f1ocnvfv2 7285	. . . . . . . . . 10 ⊢ ((𝑀:𝐸–1-1-onto→𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (𝑀‘(^◡𝑀‘(𝐽‘𝑖))) = (𝐽‘𝑖))
59	51, 44, 58	syl2an2r 698	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝑀‘(^◡𝑀‘(𝐽‘𝑖))) = (𝐽‘𝑖))
60	57, 59	eqtr2d 2796	. . . . . . . 8 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐽‘𝑖) = (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))))))
61	32, 48, 60	rspcedvdw 3579	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)))
62		eqtr2 2781	. . . . . . . . 9 ⊢ (((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)))
63		f1of1 6823	. . . . . . . . . . . . 13 ⊢ (𝑀:𝐸–1-1-onto→𝐷 → 𝑀:𝐸–1-1→𝐷)
64	63	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑀:𝐸–1-1→𝐷)
65	64	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝑀:𝐸–1-1→𝐷)
66	9	iedgedg 29633	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐼 ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ (Edg‘𝐺))
67	11, 66	sylan 592	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ (Edg‘𝐺))
68	67, 12	eleqtrrdi 2871	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
69	68	ex 418	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (𝑥 ∈ dom 𝐼 → (𝐼‘𝑥) ∈ 𝐸))
70	9	iedgedg 29633	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐼 ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ (Edg‘𝐺))
71	11, 70	sylan 592	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ (Edg‘𝐺))
72	71, 12	eleqtrrdi 2871	. . . . . . . . . . . . . . . 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-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ((𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)))
77	76	imp 412	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸))
78		f1fveq 7266	. . . . . . . . . . 11 ⊢ ((𝑀:𝐸–1-1→𝐷 ∧ ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)) → ((𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)) ↔ (𝐼‘𝑥) = (𝐼‘𝑦)))
79	65, 77, 78	syl2an2r 698	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)) ↔ (𝐼‘𝑥) = (𝐼‘𝑦)))
80		f1of1 6823	. . . . . . . . . . . . . 14 ⊢ (𝐼:dom 𝐼–1-1-onto→(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-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐼:dom 𝐼–1-1→(Edg‘𝐺))
84		f1veqaeq 7260	. . . . . . . . . . 11 ⊢ ((𝐼:dom 𝐼–1-1→(Edg‘𝐺) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝐼‘𝑥) = (𝐼‘𝑦) → 𝑥 = 𝑦))
85	83, 84	sylan 592	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝐼‘𝑥) = (𝐼‘𝑦) → 𝑥 = 𝑦))
86	79, 85	sylbid 243	. . . . . . . . 9 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)) → 𝑥 = 𝑦))
87	62, 86	syl5 35	. . . . . . . 8 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → (((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → 𝑥 = 𝑦))
88	87	ralrimivva 3205	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∀𝑥 ∈ dom 𝐼∀𝑦 ∈ dom 𝐼(((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → 𝑥 = 𝑦))
89		2fveq3 6890	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)))
90	89	eqeq2d 2771	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))))
91	90	reu4 3688	. . . . . . 7 ⊢ (∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (∃𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ ∀𝑥 ∈ dom 𝐼∀𝑦 ∈ dom 𝐼(((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → 𝑥 = 𝑦)))
92	61, 88, 91	sylanbrc 595	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)))
93	3	ad3antrrr 743	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
94	6	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝑀:𝐸⟶𝐷)
95	22	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐼:dom 𝐼⟶𝐸)
96	95	ffvelcdmda 7084	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
97	94, 96	ffvelcdmd 7085	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ 𝐷)
98	97, 26	eleqtrdi 2870	. . . . . . . . 9 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻))
99		f1ocnvfv2 7285	. . . . . . . . 9 ⊢ ((𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻)) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) = (𝑀‘(𝐼‘𝑥)))
100	93, 98, 99	syl2an2r 698	. . . . . . . 8 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) = (𝑀‘(𝐼‘𝑥)))
101	100	eqeq2d 2771	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → ((𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥))))
102	101	reubidva 3379	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) ↔ ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥))))
103	92, 102	mpbird 260	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))))
104	4	ad2antrr 739	. . . . . . . 8 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
105		f1of1 6823	. . . . . . . 8 ⊢ (𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) → 𝐽:dom 𝐽–1-1→(Edg‘𝐻))
106	104, 105	syl 18	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝐽:dom 𝐽–1-1→(Edg‘𝐻))
107		simplr 781	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝑖 ∈ dom 𝐽)
108	29	adantlr 728	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
109		f1fveq 7266	. . . . . . . 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-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ↔ (𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥))))))
112	111	reubidva 3379	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ↔ ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥))))))
113	103, 112	mpbird 260	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))))
114	113	ralrimiva 3154	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → ∀𝑖 ∈ dom 𝐽∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))))
115		isuspgrim0lem.n	. . . 4 ⊢ 𝑁 = (𝑥 ∈ dom 𝐼 ↦ (^◡𝐽‘(𝑀‘(𝐼‘𝑥))))
116	115	f1ompt 7111	. . 3 ⊢ (𝑁:dom 𝐼–1-1-onto→dom 𝐽 ↔ (∀𝑥 ∈ dom 𝐼(^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽 ∧ ∀𝑖 ∈ dom 𝐽∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥)))))
117	30, 114, 116	sylanbrc 595	. 2 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑁:dom 𝐼–1-1-onto→dom 𝐽)
118		2fveq3 6890	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑖)))
119	118	fveq2d 6889	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) = (^◡𝐽‘(𝑀‘(𝐼‘𝑖))))
120	119	adantl 487	. . . . . 6 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑥 = 𝑖) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) = (^◡𝐽‘(𝑀‘(𝐼‘𝑖))))
121		simpr 490	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → 𝑖 ∈ dom 𝐼)
122		fvexd 6900	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (^◡𝐽‘(𝑀‘(𝐼‘𝑖))) ∈ V)
123	115, 120, 121, 122	fvmptd2 7002	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑁‘𝑖) = (^◡𝐽‘(𝑀‘(𝐼‘𝑖))))
124	123	fveq2d 6889	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐽‘(𝑁‘𝑖)) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑖)))))
125	6	adantr 486	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → 𝑀:𝐸⟶𝐷)
126	23	ffvelcdmda 7084	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) ∈ 𝐸)
127	125, 126	ffvelcdmd 7085	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) ∈ 𝐷)
128	127, 26	eleqtrdi 2870	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) ∈ (Edg‘𝐻))
129		f1ocnvfv2 7285	. . . . 5 ⊢ ((𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑖)) ∈ (Edg‘𝐻)) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑖)))) = (𝑀‘(𝐼‘𝑖)))
130	4, 128, 129	syl2an2r 698	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑖)))) = (𝑀‘(𝐼‘𝑖)))
131		isuspgrim0lem.m	. . . . 5 ⊢ 𝑀 = (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))
132		simpr 490	. . . . . 6 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑥 = (𝐼‘𝑖)) → 𝑥 = (𝐼‘𝑖))
133	132	imaeq2d 6051	. . . . 5 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑥 = (𝐼‘𝑖)) → (𝐹 “ 𝑥) = (𝐹 “ (𝐼‘𝑖)))
134		simp3 1156	. . . . . . 7 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐹 ∈ 𝑋)
135	134	ad3antrrr 743	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → 𝐹 ∈ 𝑋)
136	135	imaexd 7928	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐹 “ (𝐼‘𝑖)) ∈ V)
137	131, 133, 126, 136	fvmptd2 7002	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
138	124, 130, 137	3eqtrd 2799	. . 3 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
139	138	ralrimiva 3154	. 2 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → ∀𝑖 ∈ dom 𝐼(𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
140	117, 139	jca 521	1 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → (𝑁:dom 𝐼–1-1-onto→dom 𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ∃wrex 3086 ∃!wreu 3363 Vcvv 3450 ↦ cmpt 5185 ^◡ccnv 5649 dom cdm 5650 ran crn 5651 “ cima 5653 Fun wfun 6532 ⟶wf 6534 –1-1→wf1 6535 –1-1-onto→wf1o 6537 ‘cfv 6538 Vtxcvtx 29579 iEdgciedg 29580 Edgcedg 29630 UHGraphcuhgr 29639 USPGraphcuspgr 29734

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pr 5390 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-edg 29631 df-uhgr 29641 df-upgr 29665 df-uspgr 29736

This theorem is used by: isuspgrim0 49085

W3C validator