grimedg - Mathbox for Alexander van der Vekens

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

Theorem grimedg 48548

Description: For two isomorphic graphs, a set of vertices is an edge in one graph iff its image by a graph isomorphism is an edge of the other graph. (Contributed by AV, 7-Jun-2025.)

**Hypotheses**
Ref	Expression
grimedg.v	⊢ 𝑉 = (Vtx‘𝐺)
grimedg.i	⊢ 𝐼 = (Edg‘𝐺)
grimedg.e	⊢ 𝐸 = (Edg‘𝐻)

**Assertion**
Ref	Expression
grimedg	⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))

Proof of Theorem grimedg Dummy variables 𝑗 𝑘 𝑖 𝑙 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		grimedg.v	. . . . . 6 ⊢ 𝑉 = (Vtx‘𝐺)
2		eqid 2763	. . . . . 6 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
3		eqid 2763	. . . . . 6 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
4		eqid 2763	. . . . . 6 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
5	1, 2, 3, 4	grimprop 48496	. . . . 5 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
6		grimedg.i	. . . . . . . . . . . 12 ⊢ 𝐼 = (Edg‘𝐺)
7	6	eleq2i 2855	. . . . . . . . . . 11 ⊢ (𝐾 ∈ 𝐼 ↔ 𝐾 ∈ (Edg‘𝐺))
8	3	uhgredgiedgb 29334	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ UHGraph → (𝐾 ∈ (Edg‘𝐺) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘)))
9	8	ad2antll 739	. . . . . . . . . . 11 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (𝐾 ∈ (Edg‘𝐺) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘)))
10	7, 9	bitrid 285	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (𝐾 ∈ 𝐼 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘)))
11		2fveq3 6872	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑘 → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘𝑘)))
12		fveq2 6867	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑘 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑘))
13	12	imaeq2d 6049	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑘 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))
14	11, 13	eqeq12d 2779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑘 → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
15	14	rspcv 3578	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
16	15	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
17	4	uhgrfun 29274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐻 ∈ UHGraph → Fun (iEdg‘𝐻))
18	17	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → Fun (iEdg‘𝐻))
19		f1of 6806	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
20	19	ad2antll 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → 𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
21		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → 𝑘 ∈ dom (iEdg‘𝐺))
22	20, 21	ffvelcdmd 7066	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → (𝑗‘𝑘) ∈ dom (iEdg‘𝐻))
23	4	iedgedg 29258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑗‘𝑘) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ (Edg‘𝐻))
24		grimedg.e	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐸 = (Edg‘𝐻)
25	23, 24	eleqtrrdi 2874	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑗‘𝑘) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸)
26	18, 22, 25	syl2an2r 695	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸)
27		eleq1 2851	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) = ((iEdg‘𝐻)‘(𝑗‘𝑘)) → ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸 ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸))
28	27	eqcoms 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸 ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸))
29	26, 28	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸))
30	29	ex 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)))
31	30	com23 86	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)))
32	16, 31	syld 47	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)))
33	32	com13 88	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)))
34	33	impr 458	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸))
35	34	impl 459	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)
36	35	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)
37		imaeq2 6045	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑘) → (𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))
38	37	eleq1d 2848	. . . . . . . . . . . . . . 15 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑘) → ((𝐹 “ 𝐾) ∈ 𝐸 ↔ (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸))
39	38	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → ((𝐹 “ 𝐾) ∈ 𝐸 ↔ (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸))
40	36, 39	mpbird 259	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → (𝐹 “ 𝐾) ∈ 𝐸)
41	1, 3	uhgrss 29272	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ UHGraph ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉)
42	41	ex 416	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ UHGraph → (𝑘 ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉))
43	42	ad2antll 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (𝑘 ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉))
44	43	imp 410	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉)
45	44	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉)
46		sseq1 3962	. . . . . . . . . . . . . . 15 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑘) → (𝐾 ⊆ 𝑉 ↔ ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉))
47	46	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → (𝐾 ⊆ 𝑉 ↔ ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉))
48	45, 47	mpbird 259	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → 𝐾 ⊆ 𝑉)
49	40, 48	jca 519	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉))
50	49	ex 416	. . . . . . . . . . 11 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐾 = ((iEdg‘𝐺)‘𝑘) → ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))
51	50	rexlimdva 3164	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘) → ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))
52	10, 51	sylbid 242	. . . . . . . . 9 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (𝐾 ∈ 𝐼 → ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))
53	24	eleq2i 2855	. . . . . . . . . . . 12 ⊢ ((𝐹 “ 𝐾) ∈ 𝐸 ↔ (𝐹 “ 𝐾) ∈ (Edg‘𝐻))
54	4	uhgredgiedgb 29334	. . . . . . . . . . . . 13 ⊢ (𝐻 ∈ UHGraph → ((𝐹 “ 𝐾) ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)(𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘)))
55	54	ad2antrl 738	. . . . . . . . . . . 12 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → ((𝐹 “ 𝐾) ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)(𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘)))
56	53, 55	bitrid 285	. . . . . . . . . . 11 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → ((𝐹 “ 𝐾) ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)(𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘)))
57		f1ofo 6814	. . . . . . . . . . . . . . . 16 ⊢ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑗:dom (iEdg‘𝐺)–onto→dom (iEdg‘𝐻))
58	57	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → 𝑗:dom (iEdg‘𝐺)–onto→dom (iEdg‘𝐻))
59	58	ad2antlr 737	. . . . . . . . . . . . . 14 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → 𝑗:dom (iEdg‘𝐺)–onto→dom (iEdg‘𝐻))
60		foelrn 7088	. . . . . . . . . . . . . 14 ⊢ ((𝑗:dom (iEdg‘𝐺)–onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃𝑙 ∈ dom (iEdg‘𝐺)𝑘 = (𝑗‘𝑙))
61	59, 60	sylan 589	. . . . . . . . . . . . 13 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃𝑙 ∈ dom (iEdg‘𝐺)𝑘 = (𝑗‘𝑙))
62		2fveq3 6872	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑙 → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘𝑙)))
63		fveq2 6867	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑙 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑙))
64	63	imaeq2d 6049	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑙 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)))
65	62, 64	eqeq12d 2779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑙 → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
66	65	rspcv 3578	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
67	66	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ 𝑙 ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
68		fveq2 6867	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = (𝑗‘𝑙) → ((iEdg‘𝐻)‘𝑘) = ((iEdg‘𝐻)‘(𝑗‘𝑙)))
69	68	eqeq2d 2774	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = (𝑗‘𝑙) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ↔ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))))
70	69	ad2antll 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ↔ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))))
71		simpl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) → 𝐻 ∈ UHGraph)
72	71	ad2antrl 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → 𝐻 ∈ UHGraph)
73		simplrr 787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → 𝑘 ∈ dom (iEdg‘𝐻))
74		eleq1 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = (𝑗‘𝑙) → (𝑘 ∈ dom (iEdg‘𝐻) ↔ (𝑗‘𝑙) ∈ dom (iEdg‘𝐻)))
75	74	ad2antll 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → (𝑘 ∈ dom (iEdg‘𝐻) ↔ (𝑗‘𝑙) ∈ dom (iEdg‘𝐻)))
76	73, 75	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → (𝑗‘𝑙) ∈ dom (iEdg‘𝐻))
77	2, 4	uhgrss 29272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐻 ∈ UHGraph ∧ (𝑗‘𝑙) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑙)) ⊆ (Vtx‘𝐻))
78	72, 76, 77	syl2an2r 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐻)‘(𝑗‘𝑙)) ⊆ (Vtx‘𝐻))
79	78	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))) → ((iEdg‘𝐻)‘(𝑗‘𝑙)) ⊆ (Vtx‘𝐻))
80		sseq1 3962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙)) → ((𝐹 “ 𝐾) ⊆ (Vtx‘𝐻) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑙)) ⊆ (Vtx‘𝐻)))
81	80	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))) → ((𝐹 “ 𝐾) ⊆ (Vtx‘𝐻) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑙)) ⊆ (Vtx‘𝐻)))
82	79, 81	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))) → (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻))
83		eqeq2 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙)) ↔ (𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
84	83	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙)) ↔ (𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
85		f1of1 6805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
86	85	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
87	86	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻)) ∧ 𝐾 ⊆ 𝑉) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
88		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → 𝐺 ∈ UHGraph)
89	88	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → 𝐺 ∈ UHGraph)
90		simpl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙)) → 𝑙 ∈ dom (iEdg‘𝐺))
91	1, 3	uhgrss 29272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐺 ∈ UHGraph ∧ 𝑙 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉)
92	89, 90, 91	syl2an 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉)
93	92	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻)) → ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉)
94	93	anim1ci 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻)) ∧ 𝐾 ⊆ 𝑉) → (𝐾 ⊆ 𝑉 ∧ ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉))
95		f1imaeq 7249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐹:𝑉–1-1→(Vtx‘𝐻) ∧ (𝐾 ⊆ 𝑉 ∧ ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉)) → ((𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) ↔ 𝐾 = ((iEdg‘𝐺)‘𝑙)))
96	87, 94, 95	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻)) ∧ 𝐾 ⊆ 𝑉) → ((𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) ↔ 𝐾 = ((iEdg‘𝐺)‘𝑙)))
97	3	uhgrfun 29274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
98	97	ad2antlr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → Fun (iEdg‘𝐺))
99	98	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → Fun (iEdg‘𝐺))
100	3	iedgedg 29258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((Fun (iEdg‘𝐺) ∧ 𝑙 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑙) ∈ (Edg‘𝐺))
101	99, 90, 100	syl2an 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐺)‘𝑙) ∈ (Edg‘𝐺))
102	101, 6	eleqtrrdi 2874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐺)‘𝑙) ∈ 𝐼)
103		eleq1 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑙) → (𝐾 ∈ 𝐼 ↔ ((iEdg‘𝐺)‘𝑙) ∈ 𝐼))
104	102, 103	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → (𝐾 = ((iEdg‘𝐺)‘𝑙) → 𝐾 ∈ 𝐼))
105	104	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻)) ∧ 𝐾 ⊆ 𝑉) → (𝐾 = ((iEdg‘𝐺)‘𝑙) → 𝐾 ∈ 𝐼))
106	96, 105	sylbid 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻)) ∧ 𝐾 ⊆ 𝑉) → ((𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → 𝐾 ∈ 𝐼))
107	106	ex 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻)) → (𝐾 ⊆ 𝑉 → ((𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → 𝐾 ∈ 𝐼)))
108	107	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻)) → ((𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼)))
109	108	ex 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) → ((𝐹 “ 𝐾) ⊆ (Vtx‘𝐻) → ((𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
110	109	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) → ((𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → ((𝐹 “ 𝐾) ⊆ (Vtx‘𝐻) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
111	84, 110	sylbid 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙)) → ((𝐹 “ 𝐾) ⊆ (Vtx‘𝐻) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
112	111	imp 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))) → ((𝐹 “ 𝐾) ⊆ (Vtx‘𝐻) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼)))
113	82, 112	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))
114	113	exp31 423	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
115	114	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙)) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
116	70, 115	sylbid 242	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
117	116	exp31 423	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙)) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))))
118	117	com23 86	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → ((𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙)) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))))
119	118	com24 95	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙)) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))))
120	119	3imp 1124	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → ((𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙)) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
121	120	expdimp 456	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ 𝑙 ∈ dom (iEdg‘𝐺)) → (𝑘 = (𝑗‘𝑙) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
122	67, 121	syl5d 73	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ 𝑙 ∈ dom (iEdg‘𝐺)) → (𝑘 = (𝑗‘𝑙) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
123	122	rexlimdva 3164	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → (∃𝑙 ∈ dom (iEdg‘𝐺)𝑘 = (𝑗‘𝑙) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
124	123	3exp 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (∃𝑙 ∈ dom (iEdg‘𝐺)𝑘 = (𝑗‘𝑙) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))))
125	124	com25 99	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (∃𝑙 ∈ dom (iEdg‘𝐺)𝑘 = (𝑗‘𝑙) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))))
126	125	impr 458	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (∃𝑙 ∈ dom (iEdg‘𝐺)𝑘 = (𝑗‘𝑙) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼)))))
127	126	impl 459	. . . . . . . . . . . . 13 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (∃𝑙 ∈ dom (iEdg‘𝐺)𝑘 = (𝑗‘𝑙) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
128	61, 127	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼)))
129	128	rexlimdva 3164	. . . . . . . . . . 11 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (∃𝑘 ∈ dom (iEdg‘𝐻)(𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼)))
130	56, 129	sylbid 242	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → ((𝐹 “ 𝐾) ∈ 𝐸 → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼)))
131	130	impd 414	. . . . . . . . 9 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉) → 𝐾 ∈ 𝐼))
132	52, 131	impbid 214	. . . . . . . 8 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))
133	132	exp31 423	. . . . . . 7 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))))
134	133	exlimdv 1954	. . . . . 6 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))))
135	134	imp 410	. . . . 5 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉))))
136	5, 135	syl 17	. . . 4 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉))))
137	136	expd 419	. . 3 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐻 ∈ UHGraph → (𝐺 ∈ UHGraph → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))))
138	137	com13 88	. 2 ⊢ (𝐺 ∈ UHGraph → (𝐻 ∈ UHGraph → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))))
139	138	3imp 1124	1 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1099 = wceq 1561 ∃wex 1800 ∈ wcel 2143 ∀wral 3077 ∃wrex 3087 ⊆ wss 3905 dom cdm 5648 “ cima 5651 Fun wfun 6515 ⟶wf 6517 –1-1→wf1 6518 –onto→wfo 6519 –1-1-onto→wf1o 6520 ‘cfv 6521 (class class class)co 7396 Vtxcvtx 29204 iEdgciedg 29205 Edgcedg 29255 UHGraphcuhgr 29264 GraphIso cgrim 48488

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1816 ax-4 1830 ax-5 1931 ax-6 1988 ax-7 2029 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5247 ax-nul 5257 ax-pow 5323 ax-pr 5391 ax-un 7718

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1101 df-tru 1564 df-fal 1574 df-ex 1801 df-nf 1805 df-sb 2092 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3078 df-rex 3088 df-rab 3416 df-v 3457 df-sbc 3746 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-br 5102 df-opab 5164 df-mpt 5183 df-id 5543 df-xp 5654 df-rel 5655 df-cnv 5656 df-co 5657 df-dm 5658 df-rn 5659 df-res 5660 df-ima 5661 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-ov 7399 df-oprab 7400 df-mpo 7401 df-map 8810 df-edg 29256 df-uhgr 29266 df-grim 48491

This theorem is referenced by: grimedgi 48549 grimgrtri 48562

W3C validator