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 47355

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 29058	. . . . . . 7 ⊢ (𝐻 ∈ USPGraph → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
3	2	3ad2ant2 1131	. . . . . 6 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
4	3	ad2antrr 724	. . . . 5 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
5		f1of 6838	. . . . . . . . 9 ⊢ (𝑀:𝐸–1-1-onto→𝐷 → 𝑀:𝐸⟶𝐷)
6	5	adantl 480	. . . . . . . 8 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑀:𝐸⟶𝐷)
7	6	adantr 479	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → 𝑀:𝐸⟶𝐷)
8		uspgruhgr 29069	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
9		isuspgrim0lem.i	. . . . . . . . . . . . 13 ⊢ 𝐼 = (iEdg‘𝐺)
10	9	uhgrfun 28951	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ UHGraph → Fun 𝐼)
11	8, 10	syl 17	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USPGraph → Fun 𝐼)
12		isusgrim.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (Edg‘𝐺)
13		edgval 28934	. . . . . . . . . . . . . 14 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
14	9	eqcomi 2734	. . . . . . . . . . . . . . 15 ⊢ (iEdg‘𝐺) = 𝐼
15	14	rneqi 5939	. . . . . . . . . . . . . 14 ⊢ ran (iEdg‘𝐺) = ran 𝐼
16	12, 13, 15	3eqtri 2757	. . . . . . . . . . . . 13 ⊢ 𝐸 = ran 𝐼
17		feq3 6706	. . . . . . . . . . . . 13 ⊢ (𝐸 = ran 𝐼 → (𝐼:dom 𝐼⟶𝐸 ↔ 𝐼:dom 𝐼⟶ran 𝐼))
18	16, 17	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝐼:dom 𝐼⟶𝐸 ↔ 𝐼:dom 𝐼⟶ran 𝐼)
19		fdmrn 6755	. . . . . . . . . . . 12 ⊢ (Fun 𝐼 ↔ 𝐼:dom 𝐼⟶ran 𝐼)
20	18, 19	bitr4i 277	. . . . . . . . . . 11 ⊢ (𝐼:dom 𝐼⟶𝐸 ↔ Fun 𝐼)
21	11, 20	sylibr 233	. . . . . . . . . 10 ⊢ (𝐺 ∈ USPGraph → 𝐼:dom 𝐼⟶𝐸)
22	21	3ad2ant1 1130	. . . . . . . . 9 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐼:dom 𝐼⟶𝐸)
23	22	ad2antrr 724	. . . . . . . 8 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐼:dom 𝐼⟶𝐸)
24	23	ffvelcdmda 7093	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
25	7, 24	ffvelcdmd 7094	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ 𝐷)
26		isusgrim.d	. . . . . 6 ⊢ 𝐷 = (Edg‘𝐻)
27	25, 26	eleqtrdi 2835	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻))
28		f1ocnvdm 7294	. . . . 5 ⊢ ((𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻)) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
29	4, 27, 28	syl2an2r 683	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
30	29	ralrimiva 3135	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → ∀𝑥 ∈ dom 𝐼(^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
31		2fveq3 6901	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))))))
32	31	eqeq2d 2736	. . . . . . . 8 ⊢ (𝑥 = (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) → ((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖)))))))
33	9	uspgrf1oedg 29058	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USPGraph → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
34	33	3ad2ant1 1130	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
35	34	ad2antrr 724	. . . . . . . . 9 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
36		f1oeq2 6827	. . . . . . . . . . . . 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 215	. . . . . . . . . . 11 ⊢ (𝑀:𝐸–1-1-onto→𝐷 → 𝑀:(Edg‘𝐺)–1-1-onto→𝐷)
39	38	adantl 480	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑀:(Edg‘𝐺)–1-1-onto→𝐷)
40		f1oeq3 6828	. . . . . . . . . . . . . 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 233	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐽:dom 𝐽–1-1-onto→𝐷)
43		f1of 6838	. . . . . . . . . . . 12 ⊢ (𝐽:dom 𝐽–1-1-onto→𝐷 → 𝐽:dom 𝐽⟶𝐷)
44	42, 43	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐽:dom 𝐽⟶𝐷)
45	44	ffvelcdmda 7093	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐽‘𝑖) ∈ 𝐷)
46		f1ocnvdm 7294	. . . . . . . . . 10 ⊢ ((𝑀:(Edg‘𝐺)–1-1-onto→𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
47	39, 45, 46	syl2an2r 683	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
48		f1ocnvdm 7294	. . . . . . . . 9 ⊢ ((𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺) ∧ (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺)) → (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) ∈ dom 𝐼)
49	35, 47, 48	syl2an2r 683	. . . . . . . 8 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) ∈ dom 𝐼)
50		simpll1 1209	. . . . . . . . . . . 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 483	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑀:𝐸–1-1-onto→𝐷)
53		f1ocnvdm 7294	. . . . . . . . . . . . 13 ⊢ ((𝑀:𝐸–1-1-onto→𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (^◡𝑀‘(𝐽‘𝑖)) ∈ 𝐸)
54	52, 45, 53	syl2an2r 683	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝑀‘(𝐽‘𝑖)) ∈ 𝐸)
55	54, 12	eleqtrdi 2835	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
56		f1ocnvfv2 7286	. . . . . . . . . . 11 ⊢ ((𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺) ∧ (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺)) → (𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖)))) = (^◡𝑀‘(𝐽‘𝑖)))
57	51, 55, 56	syl2an2r 683	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖)))) = (^◡𝑀‘(𝐽‘𝑖)))
58	57	fveq2d 6900	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))))) = (𝑀‘(^◡𝑀‘(𝐽‘𝑖))))
59		f1ocnvfv2 7286	. . . . . . . . . 10 ⊢ ((𝑀:𝐸–1-1-onto→𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (𝑀‘(^◡𝑀‘(𝐽‘𝑖))) = (𝐽‘𝑖))
60	52, 45, 59	syl2an2r 683	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝑀‘(^◡𝑀‘(𝐽‘𝑖))) = (𝐽‘𝑖))
61	58, 60	eqtr2d 2766	. . . . . . . 8 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐽‘𝑖) = (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))))))
62	32, 49, 61	rspcedvdw 3609	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)))
63		eqtr2 2749	. . . . . . . . 9 ⊢ (((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)))
64		f1of1 6837	. . . . . . . . . . . . 13 ⊢ (𝑀:𝐸–1-1-onto→𝐷 → 𝑀:𝐸–1-1→𝐷)
65	64	adantl 480	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑀:𝐸–1-1→𝐷)
66	65	adantr 479	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝑀:𝐸–1-1→𝐷)
67	9	iedgedg 28935	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐼 ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ (Edg‘𝐺))
68	11, 67	sylan 578	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ (Edg‘𝐺))
69	68, 12	eleqtrrdi 2836	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
70	69	ex 411	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (𝑥 ∈ dom 𝐼 → (𝐼‘𝑥) ∈ 𝐸))
71	9	iedgedg 28935	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐼 ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ (Edg‘𝐺))
72	11, 71	sylan 578	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ (Edg‘𝐺))
73	72, 12	eleqtrrdi 2836	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ 𝐸)
74	73	ex 411	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (𝑦 ∈ dom 𝐼 → (𝐼‘𝑦) ∈ 𝐸))
75	70, 74	anim12d 607	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ USPGraph → ((𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)))
76	75	3ad2ant1 1130	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → ((𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)))
77	76	ad3antrrr 728	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ((𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)))
78	77	imp 405	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸))
79		f1fveq 7272	. . . . . . . . . . 11 ⊢ ((𝑀:𝐸–1-1→𝐷 ∧ ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)) → ((𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)) ↔ (𝐼‘𝑥) = (𝐼‘𝑦)))
80	66, 78, 79	syl2an2r 683	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)) ↔ (𝐼‘𝑥) = (𝐼‘𝑦)))
81		f1of1 6837	. . . . . . . . . . . . . 14 ⊢ (𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺) → 𝐼:dom 𝐼–1-1→(Edg‘𝐺))
82	33, 81	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ USPGraph → 𝐼:dom 𝐼–1-1→(Edg‘𝐺))
83	82	3ad2ant1 1130	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐼:dom 𝐼–1-1→(Edg‘𝐺))
84	83	ad3antrrr 728	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐼:dom 𝐼–1-1→(Edg‘𝐺))
85		f1veqaeq 7267	. . . . . . . . . . 11 ⊢ ((𝐼:dom 𝐼–1-1→(Edg‘𝐺) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝐼‘𝑥) = (𝐼‘𝑦) → 𝑥 = 𝑦))
86	84, 85	sylan 578	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝐼‘𝑥) = (𝐼‘𝑦) → 𝑥 = 𝑦))
87	80, 86	sylbid 239	. . . . . . . . 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 3190	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∀𝑥 ∈ dom 𝐼∀𝑦 ∈ dom 𝐼(((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → 𝑥 = 𝑦))
90		2fveq3 6901	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)))
91	90	eqeq2d 2736	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))))
92	91	reu4 3723	. . . . . . 7 ⊢ (∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (∃𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ ∀𝑥 ∈ dom 𝐼∀𝑦 ∈ dom 𝐼(((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → 𝑥 = 𝑦)))
93	62, 89, 92	sylanbrc 581	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)))
94	3	ad3antrrr 728	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
95	6	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝑀:𝐸⟶𝐷)
96	22	ad3antrrr 728	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐼:dom 𝐼⟶𝐸)
97	96	ffvelcdmda 7093	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
98	95, 97	ffvelcdmd 7094	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ 𝐷)
99	98, 26	eleqtrdi 2835	. . . . . . . . 9 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻))
100		f1ocnvfv2 7286	. . . . . . . . 9 ⊢ ((𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻)) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) = (𝑀‘(𝐼‘𝑥)))
101	94, 99, 100	syl2an2r 683	. . . . . . . 8 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) = (𝑀‘(𝐼‘𝑥)))
102	101	eqeq2d 2736	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → ((𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥))))
103	102	reubidva 3379	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) ↔ ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥))))
104	93, 103	mpbird 256	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))))
105	4	ad2antrr 724	. . . . . . . 8 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
106		f1of1 6837	. . . . . . . 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 767	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝑖 ∈ dom 𝐽)
109	29	adantlr 713	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
110		f1fveq 7272	. . . . . . . 8 ⊢ ((𝐽:dom 𝐽–1-1→(Edg‘𝐻) ∧ (𝑖 ∈ dom 𝐽 ∧ (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)) → ((𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) ↔ 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥)))))
111	110	bicomd 222	. . . . . . 7 ⊢ ((𝐽:dom 𝐽–1-1→(Edg‘𝐻) ∧ (𝑖 ∈ dom 𝐽 ∧ (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)) → (𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ↔ (𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥))))))
112	107, 108, 109, 111	syl12anc 835	. . . . . 6 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ↔ (𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥))))))
113	112	reubidva 3379	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ↔ ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥))))))
114	104, 113	mpbird 256	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))))
115	114	ralrimiva 3135	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → ∀𝑖 ∈ dom 𝐽∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))))
116		isuspgrim0lem.n	. . . 4 ⊢ 𝑁 = (𝑥 ∈ dom 𝐼 ↦ (^◡𝐽‘(𝑀‘(𝐼‘𝑥))))
117	116	f1ompt 7120	. . 3 ⊢ (𝑁:dom 𝐼–1-1-onto→dom 𝐽 ↔ (∀𝑥 ∈ dom 𝐼(^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽 ∧ ∀𝑖 ∈ dom 𝐽∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥)))))
118	30, 115, 117	sylanbrc 581	. 2 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑁:dom 𝐼–1-1-onto→dom 𝐽)
119		2fveq3 6901	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑖)))
120	119	fveq2d 6900	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) = (^◡𝐽‘(𝑀‘(𝐼‘𝑖))))
121	120	adantl 480	. . . . . 6 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑥 = 𝑖) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) = (^◡𝐽‘(𝑀‘(𝐼‘𝑖))))
122		simpr 483	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → 𝑖 ∈ dom 𝐼)
123		fvexd 6911	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (^◡𝐽‘(𝑀‘(𝐼‘𝑖))) ∈ V)
124	116, 121, 122, 123	fvmptd2 7012	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑁‘𝑖) = (^◡𝐽‘(𝑀‘(𝐼‘𝑖))))
125	124	fveq2d 6900	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐽‘(𝑁‘𝑖)) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑖)))))
126	6	adantr 479	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → 𝑀:𝐸⟶𝐷)
127	23	ffvelcdmda 7093	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) ∈ 𝐸)
128	126, 127	ffvelcdmd 7094	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) ∈ 𝐷)
129	128, 26	eleqtrdi 2835	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) ∈ (Edg‘𝐻))
130		f1ocnvfv2 7286	. . . . 5 ⊢ ((𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑖)) ∈ (Edg‘𝐻)) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑖)))) = (𝑀‘(𝐼‘𝑖)))
131	4, 129, 130	syl2an2r 683	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑖)))) = (𝑀‘(𝐼‘𝑖)))
132		isuspgrim0lem.m	. . . . 5 ⊢ 𝑀 = (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))
133		simpr 483	. . . . . 6 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑥 = (𝐼‘𝑖)) → 𝑥 = (𝐼‘𝑖))
134	133	imaeq2d 6064	. . . . 5 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑥 = (𝐼‘𝑖)) → (𝐹 “ 𝑥) = (𝐹 “ (𝐼‘𝑖)))
135		simp3 1135	. . . . . . 7 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐹 ∈ 𝑋)
136	135	ad3antrrr 728	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → 𝐹 ∈ 𝑋)
137	136	imaexd 7924	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐹 “ (𝐼‘𝑖)) ∈ V)
138	132, 134, 127, 137	fvmptd2 7012	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
139	125, 131, 138	3eqtrd 2769	. . 3 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
140	139	ralrimiva 3135	. 2 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → ∀𝑖 ∈ dom 𝐼(𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
141	118, 140	jca 510	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 205 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ∀wral 3050 ∃wrex 3059 ∃!wreu 3361 Vcvv 3461 ↦ cmpt 5232 ^◡ccnv 5677 dom cdm 5678 ran crn 5679 “ cima 5681 Fun wfun 6543 ⟶wf 6545 –1-1→wf1 6546 –1-1-onto→wf1o 6548 ‘cfv 6549 Vtxcvtx 28881 iEdgciedg 28882 Edgcedg 28932 UHGraphcuhgr 28941 USPGraphcuspgr 29033

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 ax-un 7741

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 df-fv 6557 df-edg 28933 df-uhgr 28943 df-upgr 28967 df-uspgr 29035

This theorem is referenced by: isuspgrim0 47356

W3C validator