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 47893

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 29100	. . . . . . 7 ⊢ (𝐻 ∈ USPGraph → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
3	2	3ad2ant2 1134	. . . . . 6 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
4	3	ad2antrr 726	. . . . 5 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
5		f1of 6800	. . . . . . . . 9 ⊢ (𝑀:𝐸–1-1-onto→𝐷 → 𝑀:𝐸⟶𝐷)
6	5	adantl 481	. . . . . . . 8 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑀:𝐸⟶𝐷)
7	6	adantr 480	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → 𝑀:𝐸⟶𝐷)
8		uspgruhgr 29111	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
9		isuspgrim0lem.i	. . . . . . . . . . . . 13 ⊢ 𝐼 = (iEdg‘𝐺)
10	9	uhgrfun 28993	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ UHGraph → Fun 𝐼)
11	8, 10	syl 17	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USPGraph → Fun 𝐼)
12		isusgrim.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (Edg‘𝐺)
13		edgval 28976	. . . . . . . . . . . . . 14 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
14	9	eqcomi 2738	. . . . . . . . . . . . . . 15 ⊢ (iEdg‘𝐺) = 𝐼
15	14	rneqi 5901	. . . . . . . . . . . . . 14 ⊢ ran (iEdg‘𝐺) = ran 𝐼
16	12, 13, 15	3eqtri 2756	. . . . . . . . . . . . 13 ⊢ 𝐸 = ran 𝐼
17		feq3 6668	. . . . . . . . . . . . 13 ⊢ (𝐸 = ran 𝐼 → (𝐼:dom 𝐼⟶𝐸 ↔ 𝐼:dom 𝐼⟶ran 𝐼))
18	16, 17	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝐼:dom 𝐼⟶𝐸 ↔ 𝐼:dom 𝐼⟶ran 𝐼)
19		fdmrn 6719	. . . . . . . . . . . 12 ⊢ (Fun 𝐼 ↔ 𝐼:dom 𝐼⟶ran 𝐼)
20	18, 19	bitr4i 278	. . . . . . . . . . 11 ⊢ (𝐼:dom 𝐼⟶𝐸 ↔ Fun 𝐼)
21	11, 20	sylibr 234	. . . . . . . . . 10 ⊢ (𝐺 ∈ USPGraph → 𝐼:dom 𝐼⟶𝐸)
22	21	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐼:dom 𝐼⟶𝐸)
23	22	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐼:dom 𝐼⟶𝐸)
24	23	ffvelcdmda 7056	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
25	7, 24	ffvelcdmd 7057	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ 𝐷)
26		isusgrim.d	. . . . . 6 ⊢ 𝐷 = (Edg‘𝐻)
27	25, 26	eleqtrdi 2838	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻))
28		f1ocnvdm 7260	. . . . 5 ⊢ ((𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻)) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
29	4, 27, 28	syl2an2r 685	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
30	29	ralrimiva 3125	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → ∀𝑥 ∈ dom 𝐼(^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
31		2fveq3 6863	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))))))
32	31	eqeq2d 2740	. . . . . . . 8 ⊢ (𝑥 = (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) → ((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖)))))))
33	9	uspgrf1oedg 29100	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USPGraph → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
34	33	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
35	34	ad2antrr 726	. . . . . . . . 9 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
36		f1oeq2 6789	. . . . . . . . . . . . 13 ⊢ (𝐸 = (Edg‘𝐺) → (𝑀:𝐸–1-1-onto→𝐷 ↔ 𝑀:(Edg‘𝐺)–1-1-onto→𝐷))
37	12, 36	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝑀:𝐸–1-1-onto→𝐷 ↔ 𝑀:(Edg‘𝐺)–1-1-onto→𝐷)
38	37	biimpi 216	. . . . . . . . . . 11 ⊢ (𝑀:𝐸–1-1-onto→𝐷 → 𝑀:(Edg‘𝐺)–1-1-onto→𝐷)
39	38	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑀:(Edg‘𝐺)–1-1-onto→𝐷)
40		f1oeq3 6790	. . . . . . . . . . . . . 14 ⊢ (𝐷 = (Edg‘𝐻) → (𝐽:dom 𝐽–1-1-onto→𝐷 ↔ 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻)))
41	26, 40	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐽:dom 𝐽–1-1-onto→𝐷 ↔ 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
42	4, 41	sylibr 234	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐽:dom 𝐽–1-1-onto→𝐷)
43		f1of 6800	. . . . . . . . . . . 12 ⊢ (𝐽:dom 𝐽–1-1-onto→𝐷 → 𝐽:dom 𝐽⟶𝐷)
44	42, 43	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐽:dom 𝐽⟶𝐷)
45	44	ffvelcdmda 7056	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐽‘𝑖) ∈ 𝐷)
46		f1ocnvdm 7260	. . . . . . . . . 10 ⊢ ((𝑀:(Edg‘𝐺)–1-1-onto→𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
47	39, 45, 46	syl2an2r 685	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
48		f1ocnvdm 7260	. . . . . . . . 9 ⊢ ((𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺) ∧ (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺)) → (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) ∈ dom 𝐼)
49	35, 47, 48	syl2an2r 685	. . . . . . . 8 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) ∈ dom 𝐼)
50		simpll1 1213	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐺 ∈ USPGraph)
51	50, 33	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
52		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑀:𝐸–1-1-onto→𝐷)
53		f1ocnvdm 7260	. . . . . . . . . . . . 13 ⊢ ((𝑀:𝐸–1-1-onto→𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (^◡𝑀‘(𝐽‘𝑖)) ∈ 𝐸)
54	52, 45, 53	syl2an2r 685	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝑀‘(𝐽‘𝑖)) ∈ 𝐸)
55	54, 12	eleqtrdi 2838	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
56		f1ocnvfv2 7252	. . . . . . . . . . 11 ⊢ ((𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺) ∧ (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺)) → (𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖)))) = (^◡𝑀‘(𝐽‘𝑖)))
57	51, 55, 56	syl2an2r 685	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖)))) = (^◡𝑀‘(𝐽‘𝑖)))
58	57	fveq2d 6862	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))))) = (𝑀‘(^◡𝑀‘(𝐽‘𝑖))))
59		f1ocnvfv2 7252	. . . . . . . . . 10 ⊢ ((𝑀:𝐸–1-1-onto→𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (𝑀‘(^◡𝑀‘(𝐽‘𝑖))) = (𝐽‘𝑖))
60	52, 45, 59	syl2an2r 685	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝑀‘(^◡𝑀‘(𝐽‘𝑖))) = (𝐽‘𝑖))
61	58, 60	eqtr2d 2765	. . . . . . . 8 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐽‘𝑖) = (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))))))
62	32, 49, 61	rspcedvdw 3591	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)))
63		eqtr2 2750	. . . . . . . . 9 ⊢ (((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)))
64		f1of1 6799	. . . . . . . . . . . . 13 ⊢ (𝑀:𝐸–1-1-onto→𝐷 → 𝑀:𝐸–1-1→𝐷)
65	64	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑀:𝐸–1-1→𝐷)
66	65	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝑀:𝐸–1-1→𝐷)
67	9	iedgedg 28977	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐼 ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ (Edg‘𝐺))
68	11, 67	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ (Edg‘𝐺))
69	68, 12	eleqtrrdi 2839	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
70	69	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (𝑥 ∈ dom 𝐼 → (𝐼‘𝑥) ∈ 𝐸))
71	9	iedgedg 28977	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐼 ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ (Edg‘𝐺))
72	11, 71	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ (Edg‘𝐺))
73	72, 12	eleqtrrdi 2839	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ 𝐸)
74	73	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (𝑦 ∈ dom 𝐼 → (𝐼‘𝑦) ∈ 𝐸))
75	70, 74	anim12d 609	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ USPGraph → ((𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)))
76	75	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → ((𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)))
77	76	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ((𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)))
78	77	imp 406	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸))
79		f1fveq 7237	. . . . . . . . . . 11 ⊢ ((𝑀:𝐸–1-1→𝐷 ∧ ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)) → ((𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)) ↔ (𝐼‘𝑥) = (𝐼‘𝑦)))
80	66, 78, 79	syl2an2r 685	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)) ↔ (𝐼‘𝑥) = (𝐼‘𝑦)))
81		f1of1 6799	. . . . . . . . . . . . . 14 ⊢ (𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺) → 𝐼:dom 𝐼–1-1→(Edg‘𝐺))
82	33, 81	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ USPGraph → 𝐼:dom 𝐼–1-1→(Edg‘𝐺))
83	82	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐼:dom 𝐼–1-1→(Edg‘𝐺))
84	83	ad3antrrr 730	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐼:dom 𝐼–1-1→(Edg‘𝐺))
85		f1veqaeq 7231	. . . . . . . . . . 11 ⊢ ((𝐼:dom 𝐼–1-1→(Edg‘𝐺) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝐼‘𝑥) = (𝐼‘𝑦) → 𝑥 = 𝑦))
86	84, 85	sylan 580	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝐼‘𝑥) = (𝐼‘𝑦) → 𝑥 = 𝑦))
87	80, 86	sylbid 240	. . . . . . . . 9 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)) → 𝑥 = 𝑦))
88	63, 87	syl5 34	. . . . . . . 8 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → (((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → 𝑥 = 𝑦))
89	88	ralrimivva 3180	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∀𝑥 ∈ dom 𝐼∀𝑦 ∈ dom 𝐼(((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → 𝑥 = 𝑦))
90		2fveq3 6863	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)))
91	90	eqeq2d 2740	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))))
92	91	reu4 3702	. . . . . . 7 ⊢ (∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (∃𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ ∀𝑥 ∈ dom 𝐼∀𝑦 ∈ dom 𝐼(((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → 𝑥 = 𝑦)))
93	62, 89, 92	sylanbrc 583	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)))
94	3	ad3antrrr 730	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
95	6	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝑀:𝐸⟶𝐷)
96	22	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐼:dom 𝐼⟶𝐸)
97	96	ffvelcdmda 7056	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
98	95, 97	ffvelcdmd 7057	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ 𝐷)
99	98, 26	eleqtrdi 2838	. . . . . . . . 9 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻))
100		f1ocnvfv2 7252	. . . . . . . . 9 ⊢ ((𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻)) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) = (𝑀‘(𝐼‘𝑥)))
101	94, 99, 100	syl2an2r 685	. . . . . . . 8 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) = (𝑀‘(𝐼‘𝑥)))
102	101	eqeq2d 2740	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → ((𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥))))
103	102	reubidva 3370	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) ↔ ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥))))
104	93, 103	mpbird 257	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))))
105	4	ad2antrr 726	. . . . . . . 8 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
106		f1of1 6799	. . . . . . . 8 ⊢ (𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) → 𝐽:dom 𝐽–1-1→(Edg‘𝐻))
107	105, 106	syl 17	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝐽:dom 𝐽–1-1→(Edg‘𝐻))
108		simplr 768	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝑖 ∈ dom 𝐽)
109	29	adantlr 715	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
110		f1fveq 7237	. . . . . . . 8 ⊢ ((𝐽:dom 𝐽–1-1→(Edg‘𝐻) ∧ (𝑖 ∈ dom 𝐽 ∧ (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)) → ((𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) ↔ 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥)))))
111	110	bicomd 223	. . . . . . 7 ⊢ ((𝐽:dom 𝐽–1-1→(Edg‘𝐻) ∧ (𝑖 ∈ dom 𝐽 ∧ (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)) → (𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ↔ (𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥))))))
112	107, 108, 109, 111	syl12anc 836	. . . . . 6 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ↔ (𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥))))))
113	112	reubidva 3370	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ↔ ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥))))))
114	104, 113	mpbird 257	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))))
115	114	ralrimiva 3125	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → ∀𝑖 ∈ dom 𝐽∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))))
116		isuspgrim0lem.n	. . . 4 ⊢ 𝑁 = (𝑥 ∈ dom 𝐼 ↦ (^◡𝐽‘(𝑀‘(𝐼‘𝑥))))
117	116	f1ompt 7083	. . 3 ⊢ (𝑁:dom 𝐼–1-1-onto→dom 𝐽 ↔ (∀𝑥 ∈ dom 𝐼(^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽 ∧ ∀𝑖 ∈ dom 𝐽∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥)))))
118	30, 115, 117	sylanbrc 583	. 2 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑁:dom 𝐼–1-1-onto→dom 𝐽)
119		2fveq3 6863	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑖)))
120	119	fveq2d 6862	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) = (^◡𝐽‘(𝑀‘(𝐼‘𝑖))))
121	120	adantl 481	. . . . . 6 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑥 = 𝑖) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) = (^◡𝐽‘(𝑀‘(𝐼‘𝑖))))
122		simpr 484	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → 𝑖 ∈ dom 𝐼)
123		fvexd 6873	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (^◡𝐽‘(𝑀‘(𝐼‘𝑖))) ∈ V)
124	116, 121, 122, 123	fvmptd2 6976	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑁‘𝑖) = (^◡𝐽‘(𝑀‘(𝐼‘𝑖))))
125	124	fveq2d 6862	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐽‘(𝑁‘𝑖)) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑖)))))
126	6	adantr 480	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → 𝑀:𝐸⟶𝐷)
127	23	ffvelcdmda 7056	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) ∈ 𝐸)
128	126, 127	ffvelcdmd 7057	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) ∈ 𝐷)
129	128, 26	eleqtrdi 2838	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) ∈ (Edg‘𝐻))
130		f1ocnvfv2 7252	. . . . 5 ⊢ ((𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑖)) ∈ (Edg‘𝐻)) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑖)))) = (𝑀‘(𝐼‘𝑖)))
131	4, 129, 130	syl2an2r 685	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑖)))) = (𝑀‘(𝐼‘𝑖)))
132		isuspgrim0lem.m	. . . . 5 ⊢ 𝑀 = (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))
133		simpr 484	. . . . . 6 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑥 = (𝐼‘𝑖)) → 𝑥 = (𝐼‘𝑖))
134	133	imaeq2d 6031	. . . . 5 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑥 = (𝐼‘𝑖)) → (𝐹 “ 𝑥) = (𝐹 “ (𝐼‘𝑖)))
135		simp3 1138	. . . . . . 7 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐹 ∈ 𝑋)
136	135	ad3antrrr 730	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → 𝐹 ∈ 𝑋)
137	136	imaexd 7892	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐹 “ (𝐼‘𝑖)) ∈ V)
138	132, 134, 127, 137	fvmptd2 6976	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
139	125, 131, 138	3eqtrd 2768	. . 3 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
140	139	ralrimiva 3125	. 2 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → ∀𝑖 ∈ dom 𝐼(𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
141	118, 140	jca 511	1 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → (𝑁:dom 𝐼–1-1-onto→dom 𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 ∃!wreu 3352 Vcvv 3447 ↦ cmpt 5188 ^◡ccnv 5637 dom cdm 5638 ran crn 5639 “ cima 5641 Fun wfun 6505 ⟶wf 6507 –1-1→wf1 6508 –1-1-onto→wf1o 6510 ‘cfv 6511 Vtxcvtx 28923 iEdgciedg 28924 Edgcedg 28974 UHGraphcuhgr 28983 USPGraphcuspgr 29075

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5251 ax-nul 5261 ax-pr 5387 ax-un 7711

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-br 5108 df-opab 5170 df-mpt 5189 df-id 5533 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-edg 28975 df-uhgr 28985 df-upgr 29009 df-uspgr 29077

This theorem is referenced by: isuspgrim0 47894

W3C validator