Theorem uhgrimedgi 47894

Description: An isomorphism between graphs preserves edges, i.e. if there is an edge in one graph connecting vertices then there is an edge in the other graph connecting the corresponding vertices. (Contributed by AV, 25-Oct-2025.)

Hypotheses

Ref	Expression
uhgrimedgi.e	⊢ 𝐸 = (Edg‘𝐺)
uhgrimedgi.d	⊢ 𝐷 = (Edg‘𝐻)

Assertion

Ref	Expression
uhgrimedgi	⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝐾 ∈ 𝐸)) → (𝐹 “ 𝐾) ∈ 𝐷)

Proof of Theorem uhgrimedgi

Dummy variables 𝑗 𝑘 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2730	. . . . . 6 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		eqid 2730	. . . . . 6 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
3		eqid 2730	. . . . . 6 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
4		eqid 2730	. . . . . 6 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
5	1, 2, 3, 4	grimprop 47887	. . . . 5 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
6		uhgrimedgi.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (Edg‘𝐺)
7	6	eleq2i 2821	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ 𝐸 ↔ 𝐾 ∈ (Edg‘𝐺))
8	3	uhgrfun 29000	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
9	3	edgiedgb 28988	. . . . . . . . . . . . 13 ⊢ (Fun (iEdg‘𝐺) → (𝐾 ∈ (Edg‘𝐺) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘)))
10	8, 9	syl 17	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ UHGraph → (𝐾 ∈ (Edg‘𝐺) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘)))
11	7, 10	bitrid 283	. . . . . . . . . . 11 ⊢ (𝐺 ∈ UHGraph → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘)))
12	11	adantr 480	. . . . . . . . . 10 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘)))
13		simplr 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → 𝑘 ∈ dom (iEdg‘𝐺))
14		2fveq3 6866	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑘 → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘𝑘)))
15		fveq2 6861	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑘 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑘))
16	15	imaeq2d 6034	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑘 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))
17	14, 16	eqeq12d 2746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑘 → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
18	17	rspcv 3587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
19	13, 18	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
20	4	uhgrfun 29000	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐻 ∈ UHGraph → Fun (iEdg‘𝐻))
21	20	ad3antlr 731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → Fun (iEdg‘𝐻))
22		f1of 6803	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
23	22	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
24	13	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝑘 ∈ dom (iEdg‘𝐺))
25	23, 24	ffvelcdmd 7060	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (𝑗‘𝑘) ∈ dom (iEdg‘𝐻))
26	4	iedgedg 28984	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑗‘𝑘) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ (Edg‘𝐻))
27	21, 25, 26	syl2an2r 685	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ (Edg‘𝐻))
28		uhgrimedgi.d	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐷 = (Edg‘𝐻)
29	27, 28	eleqtrrdi 2840	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐷)
30		eleq1 2817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) = ((iEdg‘𝐻)‘(𝑗‘𝑘)) → ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷 ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐷))
31	30	eqcoms 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷 ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐷))
32	29, 31	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷))
33	32	ex 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)))
34	19, 33	syl5d 73	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)))
35	34	impd 410	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷))
36	35	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)))
37	36	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)))
38	37	3imp 1110	. . . . . . . . . . . . . 14 ⊢ (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)
39		imaeq2 6030	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑘) → (𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))
40	39	eleq1d 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑘) → ((𝐹 “ 𝐾) ∈ 𝐷 ↔ (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷))
41	40	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → ((𝐹 “ 𝐾) ∈ 𝐷 ↔ (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷))
42	41	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ((𝐹 “ 𝐾) ∈ 𝐷 ↔ (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷))
43	38, 42	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (𝐹 “ 𝐾) ∈ 𝐷)
44	43	3exp 1119	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝐹 “ 𝐾) ∈ 𝐷)))
45	44	ex 412	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐾 = ((iEdg‘𝐺)‘𝑘) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝐹 “ 𝐾) ∈ 𝐷))))
46	45	rexlimdva 3135	. . . . . . . . . 10 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝐹 “ 𝐾) ∈ 𝐷))))
47	12, 46	sylbid 240	. . . . . . . . 9 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐾 ∈ 𝐸 → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝐹 “ 𝐾) ∈ 𝐷))))
48	47	imp 406	. . . . . . . 8 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐾 ∈ 𝐸) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝐹 “ 𝐾) ∈ 𝐷)))
49	48	imp 406	. . . . . . 7 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐾 ∈ 𝐸) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝐹 “ 𝐾) ∈ 𝐷))
50	49	exlimdv 1933	. . . . . 6 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐾 ∈ 𝐸) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝐹 “ 𝐾) ∈ 𝐷))
51	50	expimpd 453	. . . . 5 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐾 ∈ 𝐸) → ((𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (𝐹 “ 𝐾) ∈ 𝐷))
52	5, 51	syl5 34	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐾 ∈ 𝐸) → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹 “ 𝐾) ∈ 𝐷))
53	52	ex 412	. . 3 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐾 ∈ 𝐸 → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹 “ 𝐾) ∈ 𝐷)))
54	53	impcomd 411	. 2 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝐾 ∈ 𝐸) → (𝐹 “ 𝐾) ∈ 𝐷))
55	54	imp 406	1 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝐾 ∈ 𝐸)) → (𝐹 “ 𝐾) ∈ 𝐷)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∀wral 3045  ∃wrex 3054  dom cdm 5641   “ cima 5644  Fun wfun 6508  ⟶wf 6510  –1-1-onto→wf1o 6513  ‘cfv 6514  (class class class)co 7390  Vtxcvtx 28930  iEdgciedg 28931  Edgcedg 28981  UHGraphcuhgr 28990   GraphIso cgrim 47879

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-map 8804  df-edg 28982  df-uhgr 28992  df-grim 47882

This theorem is referenced by:  uhgrimedg  47895  upgrimwlklem2  47902  upgrimwlklem3  47903  upgrimtrlslem1  47908