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 47903

Description: Graph isomorphisms map edges onto the corresponding edges. (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 2737	. . . . . 6 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
3		eqid 2737	. . . . . 6 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
4		eqid 2737	. . . . . 6 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
5	1, 2, 3, 4	grimprop 47869	. . . . 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 2833	. . . . . . . . . . 11 ⊢ (𝐾 ∈ 𝐼 ↔ 𝐾 ∈ (Edg‘𝐺))
8	3	uhgredgiedgb 29143	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ UHGraph → (𝐾 ∈ (Edg‘𝐺) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘)))
9	8	ad2antll 729	. . . . . . . . . . 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 283	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (𝐾 ∈ 𝐼 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘)))
11		2fveq3 6911	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑘 → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘𝑘)))
12		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑘 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑘))
13	12	imaeq2d 6078	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑘 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))
14	11, 13	eqeq12d 2753	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑘 → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
15	14	rspcv 3618	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
16	15	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
17	4	uhgrfun 29083	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐻 ∈ UHGraph → Fun (iEdg‘𝐻))
18	17	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → Fun (iEdg‘𝐻))
19		f1of 6848	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
20	19	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → 𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
21		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → 𝑘 ∈ dom (iEdg‘𝐺))
22	20, 21	ffvelcdmd 7105	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → (𝑗‘𝑘) ∈ dom (iEdg‘𝐻))
23	4	iedgedg 29067	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑗‘𝑘) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ (Edg‘𝐻))
24		grimedg.e	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐸 = (Edg‘𝐻)
25	23, 24	eleqtrrdi 2852	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑗‘𝑘) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸)
26	18, 22, 25	syl2an2r 685	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸)
27		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) = ((iEdg‘𝐻)‘(𝑗‘𝑘)) → ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸 ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸))
28	27	eqcoms 2745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸 ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸))
29	26, 28	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸))
30	29	ex 412	. . . . . . . . . . . . . . . . . . . 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 454	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸))
35	34	impl 455	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)
36	35	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)
37		imaeq2 6074	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑘) → (𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))
38	37	eleq1d 2826	. . . . . . . . . . . . . . 15 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑘) → ((𝐹 “ 𝐾) ∈ 𝐸 ↔ (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸))
39	38	adantl 481	. . . . . . . . . . . . . 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 257	. . . . . . . . . . . . 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 29081	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ UHGraph ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉)
42	41	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ UHGraph → (𝑘 ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉))
43	42	ad2antll 729	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (𝑘 ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉))
44	43	imp 406	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉)
45	44	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉)
46		sseq1 4009	. . . . . . . . . . . . . . 15 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑘) → (𝐾 ⊆ 𝑉 ↔ ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉))
47	46	adantl 481	. . . . . . . . . . . . . 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 257	. . . . . . . . . . . . 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 511	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉))
50	49	ex 412	. . . . . . . . . . 11 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐾 = ((iEdg‘𝐺)‘𝑘) → ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))
51	50	rexlimdva 3155	. . . . . . . . . 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 240	. . . . . . . . 9 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (𝐾 ∈ 𝐼 → ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))
53	24	eleq2i 2833	. . . . . . . . . . . 12 ⊢ ((𝐹 “ 𝐾) ∈ 𝐸 ↔ (𝐹 “ 𝐾) ∈ (Edg‘𝐻))
54	4	uhgredgiedgb 29143	. . . . . . . . . . . . 13 ⊢ (𝐻 ∈ UHGraph → ((𝐹 “ 𝐾) ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)(𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘)))
55	54	ad2antrl 728	. . . . . . . . . . . 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 283	. . . . . . . . . . 11 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → ((𝐹 “ 𝐾) ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)(𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘)))
57		f1ofo 6855	. . . . . . . . . . . . . . . 16 ⊢ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑗:dom (iEdg‘𝐺)–onto→dom (iEdg‘𝐻))
58	57	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → 𝑗:dom (iEdg‘𝐺)–onto→dom (iEdg‘𝐻))
59	58	ad2antlr 727	. . . . . . . . . . . . . 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 7127	. . . . . . . . . . . . . 14 ⊢ ((𝑗:dom (iEdg‘𝐺)–onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃𝑙 ∈ dom (iEdg‘𝐺)𝑘 = (𝑗‘𝑙))
61	59, 60	sylan 580	. . . . . . . . . . . . 13 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃𝑙 ∈ dom (iEdg‘𝐺)𝑘 = (𝑗‘𝑙))
62		2fveq3 6911	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑙 → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘𝑙)))
63		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑙 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑙))
64	63	imaeq2d 6078	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑙 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)))
65	62, 64	eqeq12d 2753	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑙 → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
66	65	rspcv 3618	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
67	66	adantl 481	. . . . . . . . . . . . . . . . . . 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 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = (𝑗‘𝑙) → ((iEdg‘𝐻)‘𝑘) = ((iEdg‘𝐻)‘(𝑗‘𝑙)))
69	68	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = (𝑗‘𝑙) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ↔ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))))
70	69	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ↔ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))))
71		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) → 𝐻 ∈ UHGraph)
72	71	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → 𝐻 ∈ UHGraph)
73		simplrr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → 𝑘 ∈ dom (iEdg‘𝐻))
74		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = (𝑗‘𝑙) → (𝑘 ∈ dom (iEdg‘𝐻) ↔ (𝑗‘𝑙) ∈ dom (iEdg‘𝐻)))
75	74	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → (𝑗‘𝑙) ∈ dom (iEdg‘𝐻))
77	2, 4	uhgrss 29081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐻 ∈ UHGraph ∧ (𝑗‘𝑙) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑙)) ⊆ (Vtx‘𝐻))
78	72, 76, 77	syl2an2r 685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐻)‘(𝑗‘𝑙)) ⊆ (Vtx‘𝐻))
79	78	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙)) → ((𝐹 “ 𝐾) ⊆ (Vtx‘𝐻) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑙)) ⊆ (Vtx‘𝐻)))
81	80	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))) → (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻))
83		eqeq2 2749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙)) ↔ (𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
84	83	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙)) ↔ (𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
85		f1of1 6847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
86	85	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
87	86	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → 𝐺 ∈ UHGraph)
89	88	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → 𝐺 ∈ UHGraph)
90		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙)) → 𝑙 ∈ dom (iEdg‘𝐺))
91	1, 3	uhgrss 29081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐺 ∈ UHGraph ∧ 𝑙 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉)
92	89, 90, 91	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉)
93	92	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻)) ∧ 𝐾 ⊆ 𝑉) → (𝐾 ⊆ 𝑉 ∧ ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉))
95		f1imaeq 7285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐹:𝑉–1-1→(Vtx‘𝐻) ∧ (𝐾 ⊆ 𝑉 ∧ ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉)) → ((𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) ↔ 𝐾 = ((iEdg‘𝐺)‘𝑙)))
96	87, 94, 95	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 29083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
98	97	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → Fun (iEdg‘𝐺))
99	98	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → Fun (iEdg‘𝐺))
100	3	iedgedg 29067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((Fun (iEdg‘𝐺) ∧ 𝑙 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑙) ∈ (Edg‘𝐺))
101	99, 90, 100	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐺)‘𝑙) ∈ (Edg‘𝐺))
102	101, 6	eleqtrrdi 2852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐺)‘𝑙) ∈ 𝐼)
103		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑙) → (𝐾 ∈ 𝐼 ↔ ((iEdg‘𝐺)‘𝑙) ∈ 𝐼))
104	102, 103	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → (𝐾 = ((iEdg‘𝐺)‘𝑙) → 𝐾 ∈ 𝐼))
105	104	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 419	. . . . . . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
117	116	exp31 419	. . . . . . . . . . . . . . . . . . . . . . 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 1111	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → ((𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙)) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
121	120	expdimp 452	. . . . . . . . . . . . . . . . . . 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 3155	. . . . . . . . . . . . . . . . 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 1120	. . . . . . . . . . . . . . . 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 454	. . . . . . . . . . . . . 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 455	. . . . . . . . . . . . 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 3155	. . . . . . . . . . 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 240	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → ((𝐹 “ 𝐾) ∈ 𝐸 → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼)))
131	130	impd 410	. . . . . . . . 9 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉) → 𝐾 ∈ 𝐼))
132	52, 131	impbid 212	. . . . . . . 8 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))
133	132	exp31 419	. . . . . . 7 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))))
134	133	exlimdv 1933	. . . . . 6 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))))
135	134	imp 406	. . . . 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 415	. . 3 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐻 ∈ UHGraph → (𝐺 ∈ UHGraph → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))))
138	137	com13 88	. 2 ⊢ (𝐺 ∈ UHGraph → (𝐻 ∈ UHGraph → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))))
139	138	3imp 1111	1 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∃wex 1779 ∈ wcel 2108 ∀wral 3061 ∃wrex 3070 ⊆ wss 3951 dom cdm 5685 “ cima 5688 Fun wfun 6555 ⟶wf 6557 –1-1→wf1 6558 –onto→wfo 6559 –1-1-onto→wf1o 6560 ‘cfv 6561 (class class class)co 7431 Vtxcvtx 29013 iEdgciedg 29014 Edgcedg 29064 UHGraphcuhgr 29073 GraphIso cgrim 47861

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-sbc 3789 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-ov 7434 df-oprab 7435 df-mpo 7436 df-map 8868 df-edg 29065 df-uhgr 29075 df-grim 47864

This theorem is referenced by: grimgrtri 47916

W3C validator