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 47755

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 29208	. . . . . . 7 ⊢ (𝐻 ∈ USPGraph → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
3	2	3ad2ant2 1134	. . . . . 6 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
4	3	ad2antrr 725	. . . . 5 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
5		f1of 6862	. . . . . . . . 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 29219	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
9		isuspgrim0lem.i	. . . . . . . . . . . . 13 ⊢ 𝐼 = (iEdg‘𝐺)
10	9	uhgrfun 29101	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ UHGraph → Fun 𝐼)
11	8, 10	syl 17	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USPGraph → Fun 𝐼)
12		isusgrim.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (Edg‘𝐺)
13		edgval 29084	. . . . . . . . . . . . . 14 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
14	9	eqcomi 2749	. . . . . . . . . . . . . . 15 ⊢ (iEdg‘𝐺) = 𝐼
15	14	rneqi 5962	. . . . . . . . . . . . . 14 ⊢ ran (iEdg‘𝐺) = ran 𝐼
16	12, 13, 15	3eqtri 2772	. . . . . . . . . . . . 13 ⊢ 𝐸 = ran 𝐼
17		feq3 6730	. . . . . . . . . . . . 13 ⊢ (𝐸 = ran 𝐼 → (𝐼:dom 𝐼⟶𝐸 ↔ 𝐼:dom 𝐼⟶ran 𝐼))
18	16, 17	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝐼:dom 𝐼⟶𝐸 ↔ 𝐼:dom 𝐼⟶ran 𝐼)
19		fdmrn 6779	. . . . . . . . . . . 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 725	. . . . . . . 8 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐼:dom 𝐼⟶𝐸)
24	23	ffvelcdmda 7118	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
25	7, 24	ffvelcdmd 7119	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ 𝐷)
26		isusgrim.d	. . . . . 6 ⊢ 𝐷 = (Edg‘𝐻)
27	25, 26	eleqtrdi 2854	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻))
28		f1ocnvdm 7321	. . . . 5 ⊢ ((𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻)) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
29	4, 27, 28	syl2an2r 684	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑥 ∈ dom 𝐼) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
30	29	ralrimiva 3152	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → ∀𝑥 ∈ dom 𝐼(^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
31		2fveq3 6925	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))))))
32	31	eqeq2d 2751	. . . . . . . 8 ⊢ (𝑥 = (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) → ((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖)))))))
33	9	uspgrf1oedg 29208	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USPGraph → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
34	33	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
35	34	ad2antrr 725	. . . . . . . . 9 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺))
36		f1oeq2 6851	. . . . . . . . . . . . 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 6852	. . . . . . . . . . . . . 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 6862	. . . . . . . . . . . 12 ⊢ (𝐽:dom 𝐽–1-1-onto→𝐷 → 𝐽:dom 𝐽⟶𝐷)
44	42, 43	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝐽:dom 𝐽⟶𝐷)
45	44	ffvelcdmda 7118	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐽‘𝑖) ∈ 𝐷)
46		f1ocnvdm 7321	. . . . . . . . . 10 ⊢ ((𝑀:(Edg‘𝐺)–1-1-onto→𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
47	39, 45, 46	syl2an2r 684	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
48		f1ocnvdm 7321	. . . . . . . . 9 ⊢ ((𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺) ∧ (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺)) → (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) ∈ dom 𝐼)
49	35, 47, 48	syl2an2r 684	. . . . . . . 8 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))) ∈ dom 𝐼)
50		simpll1 1212	. . . . . . . . . . . 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 7321	. . . . . . . . . . . . 13 ⊢ ((𝑀:𝐸–1-1-onto→𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (^◡𝑀‘(𝐽‘𝑖)) ∈ 𝐸)
54	52, 45, 53	syl2an2r 684	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝑀‘(𝐽‘𝑖)) ∈ 𝐸)
55	54, 12	eleqtrdi 2854	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺))
56		f1ocnvfv2 7313	. . . . . . . . . . 11 ⊢ ((𝐼:dom 𝐼–1-1-onto→(Edg‘𝐺) ∧ (^◡𝑀‘(𝐽‘𝑖)) ∈ (Edg‘𝐺)) → (𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖)))) = (^◡𝑀‘(𝐽‘𝑖)))
57	51, 55, 56	syl2an2r 684	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖)))) = (^◡𝑀‘(𝐽‘𝑖)))
58	57	fveq2d 6924	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))))) = (𝑀‘(^◡𝑀‘(𝐽‘𝑖))))
59		f1ocnvfv2 7313	. . . . . . . . . 10 ⊢ ((𝑀:𝐸–1-1-onto→𝐷 ∧ (𝐽‘𝑖) ∈ 𝐷) → (𝑀‘(^◡𝑀‘(𝐽‘𝑖))) = (𝐽‘𝑖))
60	52, 45, 59	syl2an2r 684	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝑀‘(^◡𝑀‘(𝐽‘𝑖))) = (𝐽‘𝑖))
61	58, 60	eqtr2d 2781	. . . . . . . 8 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → (𝐽‘𝑖) = (𝑀‘(𝐼‘(^◡𝐼‘(^◡𝑀‘(𝐽‘𝑖))))))
62	32, 49, 61	rspcedvdw 3638	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)))
63		eqtr2 2764	. . . . . . . . 9 ⊢ (((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)))
64		f1of1 6861	. . . . . . . . . . . . 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 29085	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐼 ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ (Edg‘𝐺))
68	11, 67	sylan 579	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ (Edg‘𝐺))
69	68, 12	eleqtrrdi 2855	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
70	69	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (𝑥 ∈ dom 𝐼 → (𝐼‘𝑥) ∈ 𝐸))
71	9	iedgedg 29085	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐼 ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ (Edg‘𝐺))
72	11, 71	sylan 579	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ (Edg‘𝐺))
73	72, 12	eleqtrrdi 2855	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑦 ∈ dom 𝐼) → (𝐼‘𝑦) ∈ 𝐸)
74	73	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USPGraph → (𝑦 ∈ dom 𝐼 → (𝐼‘𝑦) ∈ 𝐸))
75	70, 74	anim12d 608	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ USPGraph → ((𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)))
76	75	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → ((𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼) → ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)))
77	76	ad3antrrr 729	. . . . . . . . . . . 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 7299	. . . . . . . . . . 11 ⊢ ((𝑀:𝐸–1-1→𝐷 ∧ ((𝐼‘𝑥) ∈ 𝐸 ∧ (𝐼‘𝑦) ∈ 𝐸)) → ((𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)) ↔ (𝐼‘𝑥) = (𝐼‘𝑦)))
80	66, 78, 79	syl2an2r 684	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)) ↔ (𝐼‘𝑥) = (𝐼‘𝑦)))
81		f1of1 6861	. . . . . . . . . . . . . 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 729	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐼:dom 𝐼–1-1→(Edg‘𝐺))
85		f1veqaeq 7294	. . . . . . . . . . 11 ⊢ ((𝐼:dom 𝐼–1-1→(Edg‘𝐺) ∧ (𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼)) → ((𝐼‘𝑥) = (𝐼‘𝑦) → 𝑥 = 𝑦))
86	84, 85	sylan 579	. . . . . . . . . 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 3208	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∀𝑥 ∈ dom 𝐼∀𝑦 ∈ dom 𝐼(((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → 𝑥 = 𝑦))
90		2fveq3 6925	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑦)))
91	90	eqeq2d 2751	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))))
92	91	reu4 3753	. . . . . . 7 ⊢ (∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ↔ (∃𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ ∀𝑥 ∈ dom 𝐼∀𝑦 ∈ dom 𝐼(((𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)) ∧ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑦))) → 𝑥 = 𝑦)))
93	62, 89, 92	sylanbrc 582	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → ∃!𝑥 ∈ dom 𝐼(𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥)))
94	3	ad3antrrr 729	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
95	6	ad2antrr 725	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝑀:𝐸⟶𝐷)
96	22	ad3antrrr 729	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) → 𝐼:dom 𝐼⟶𝐸)
97	96	ffvelcdmda 7118	. . . . . . . . . . 11 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝐼‘𝑥) ∈ 𝐸)
98	95, 97	ffvelcdmd 7119	. . . . . . . . . 10 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ 𝐷)
99	98, 26	eleqtrdi 2854	. . . . . . . . 9 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻))
100		f1ocnvfv2 7313	. . . . . . . . 9 ⊢ ((𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑥)) ∈ (Edg‘𝐻)) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) = (𝑀‘(𝐼‘𝑥)))
101	94, 99, 100	syl2an2r 684	. . . . . . . 8 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) = (𝑀‘(𝐼‘𝑥)))
102	101	eqeq2d 2751	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → ((𝐽‘𝑖) = (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑥)))) ↔ (𝐽‘𝑖) = (𝑀‘(𝐼‘𝑥))))
103	102	reubidva 3404	. . . . . 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 725	. . . . . . . 8 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → 𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻))
106		f1of1 6861	. . . . . . . 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 714	. . . . . . 7 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐽) ∧ 𝑥 ∈ dom 𝐼) → (^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽)
110		f1fveq 7299	. . . . . . . 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 3404	. . . . 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 3152	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → ∀𝑖 ∈ dom 𝐽∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥))))
116		isuspgrim0lem.n	. . . 4 ⊢ 𝑁 = (𝑥 ∈ dom 𝐼 ↦ (^◡𝐽‘(𝑀‘(𝐼‘𝑥))))
117	116	f1ompt 7145	. . 3 ⊢ (𝑁:dom 𝐼–1-1-onto→dom 𝐽 ↔ (∀𝑥 ∈ dom 𝐼(^◡𝐽‘(𝑀‘(𝐼‘𝑥))) ∈ dom 𝐽 ∧ ∀𝑖 ∈ dom 𝐽∃!𝑥 ∈ dom 𝐼 𝑖 = (^◡𝐽‘(𝑀‘(𝐼‘𝑥)))))
118	30, 115, 117	sylanbrc 582	. 2 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → 𝑁:dom 𝐼–1-1-onto→dom 𝐽)
119		2fveq3 6925	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → (𝑀‘(𝐼‘𝑥)) = (𝑀‘(𝐼‘𝑖)))
120	119	fveq2d 6924	. . . . . . 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 6935	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (^◡𝐽‘(𝑀‘(𝐼‘𝑖))) ∈ V)
124	116, 121, 122, 123	fvmptd2 7037	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑁‘𝑖) = (^◡𝐽‘(𝑀‘(𝐼‘𝑖))))
125	124	fveq2d 6924	. . . 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 7118	. . . . . . 7 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) ∈ 𝐸)
128	126, 127	ffvelcdmd 7119	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) ∈ 𝐷)
129	128, 26	eleqtrdi 2854	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) ∈ (Edg‘𝐻))
130		f1ocnvfv2 7313	. . . . 5 ⊢ ((𝐽:dom 𝐽–1-1-onto→(Edg‘𝐻) ∧ (𝑀‘(𝐼‘𝑖)) ∈ (Edg‘𝐻)) → (𝐽‘(^◡𝐽‘(𝑀‘(𝐼‘𝑖)))) = (𝑀‘(𝐼‘𝑖)))
131	4, 129, 130	syl2an2r 684	. . . 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 6089	. . . . 5 ⊢ ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑥 = (𝐼‘𝑖)) → (𝐹 “ 𝑥) = (𝐹 “ (𝐼‘𝑖)))
135		simp3 1138	. . . . . . 7 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐹 ∈ 𝑋)
136	135	ad3antrrr 729	. . . . . 6 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → 𝐹 ∈ 𝑋)
137	136	imaexd 7956	. . . . 5 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐹 “ (𝐼‘𝑖)) ∈ V)
138	132, 134, 127, 137	fvmptd2 7037	. . . 4 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝑀‘(𝐼‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
139	125, 131, 138	3eqtrd 2784	. . 3 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) ∧ 𝑖 ∈ dom 𝐼) → (𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))
140	139	ralrimiva 3152	. 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 1087 = wceq 1537 ∈ wcel 2108 ∀wral 3067 ∃wrex 3076 ∃!wreu 3386 Vcvv 3488 ↦ cmpt 5249 ^◡ccnv 5699 dom cdm 5700 ran crn 5701 “ cima 5703 Fun wfun 6567 ⟶wf 6569 –1-1→wf1 6570 –1-1-onto→wf1o 6572 ‘cfv 6573 Vtxcvtx 29031 iEdgciedg 29032 Edgcedg 29082 UHGraphcuhgr 29091 USPGraphcuspgr 29183

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-edg 29083 df-uhgr 29093 df-upgr 29117 df-uspgr 29185

This theorem is referenced by: isuspgrim0 47756

W3C validator