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 47787

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 2740	. . . . . 6 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
3		eqid 2740	. . . . . 6 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
4		eqid 2740	. . . . . 6 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
5	1, 2, 3, 4	grimprop 47753	. . . . 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 2836	. . . . . . . . . . 11 ⊢ (𝐾 ∈ 𝐼 ↔ 𝐾 ∈ (Edg‘𝐺))
8	3	uhgredgiedgb 29161	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ UHGraph → (𝐾 ∈ (Edg‘𝐺) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘)))
9	8	ad2antll 728	. . . . . . . . . . 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 6925	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑘 → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘𝑘)))
12		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑘 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑘))
13	12	imaeq2d 6089	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑘 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))
14	11, 13	eqeq12d 2756	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑘 → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
15	14	rspcv 3631	. . . . . . . . . . . . . . . . . . . 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 29101	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐻 ∈ UHGraph → Fun (iEdg‘𝐻))
18	17	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → Fun (iEdg‘𝐻))
19		f1of 6862	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
20	19	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → 𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
21		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → 𝑘 ∈ dom (iEdg‘𝐺))
22	20, 21	ffvelcdmd 7119	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → (𝑗‘𝑘) ∈ dom (iEdg‘𝐻))
23	4	iedgedg 29085	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑗‘𝑘) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ (Edg‘𝐻))
24		grimedg.e	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐸 = (Edg‘𝐻)
25	23, 24	eleqtrrdi 2855	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑗‘𝑘) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸)
26	18, 22, 25	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸)
27		eleq1 2832	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) = ((iEdg‘𝐻)‘(𝑗‘𝑘)) → ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸 ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸))
28	27	eqcoms 2748	. . . . . . . . . . . . . . . . . . . . . 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 6085	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑘) → (𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))
38	37	eleq1d 2829	. . . . . . . . . . . . . . 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 29099	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ UHGraph ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉)
42	41	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ UHGraph → (𝑘 ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉))
43	42	ad2antll 728	. . . . . . . . . . . . . . . 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 4034	. . . . . . . . . . . . . . 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 3161	. . . . . . . . . 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 2836	. . . . . . . . . . . 12 ⊢ ((𝐹 “ 𝐾) ∈ 𝐸 ↔ (𝐹 “ 𝐾) ∈ (Edg‘𝐻))
54	4	uhgredgiedgb 29161	. . . . . . . . . . . . 13 ⊢ (𝐻 ∈ UHGraph → ((𝐹 “ 𝐾) ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)(𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘)))
55	54	ad2antrl 727	. . . . . . . . . . . 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 6869	. . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . 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 7141	. . . . . . . . . . . . . 14 ⊢ ((𝑗:dom (iEdg‘𝐺)–onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃𝑙 ∈ dom (iEdg‘𝐺)𝑘 = (𝑗‘𝑙))
61	59, 60	sylan 579	. . . . . . . . . . . . 13 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃𝑙 ∈ dom (iEdg‘𝐺)𝑘 = (𝑗‘𝑙))
62		2fveq3 6925	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑙 → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘𝑙)))
63		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑙 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑙))
64	63	imaeq2d 6089	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑙 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)))
65	62, 64	eqeq12d 2756	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑙 → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
66	65	rspcv 3631	. . . . . . . . . . . . . . . . . . . 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 6920	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = (𝑗‘𝑙) → ((iEdg‘𝐻)‘𝑘) = ((iEdg‘𝐻)‘(𝑗‘𝑙)))
69	68	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = (𝑗‘𝑙) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ↔ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))))
70	69	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → 𝐻 ∈ UHGraph)
73		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → 𝑘 ∈ dom (iEdg‘𝐻))
74		eleq1 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = (𝑗‘𝑙) → (𝑘 ∈ dom (iEdg‘𝐻) ↔ (𝑗‘𝑙) ∈ dom (iEdg‘𝐻)))
75	74	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 29099	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐻 ∈ UHGraph ∧ (𝑗‘𝑙) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑙)) ⊆ (Vtx‘𝐻))
78	72, 76, 77	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐻)‘(𝑗‘𝑙)) ⊆ (Vtx‘𝐻))
79	78	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
86	85	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
87	86	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 29099	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐺 ∈ UHGraph ∧ 𝑙 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉)
92	89, 90, 91	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉)
93	92	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻)) ∧ 𝐾 ⊆ 𝑉) → (𝐾 ⊆ 𝑉 ∧ ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉))
95		f1imaeq 7302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐹:𝑉–1-1→(Vtx‘𝐻) ∧ (𝐾 ⊆ 𝑉 ∧ ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉)) → ((𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) ↔ 𝐾 = ((iEdg‘𝐺)‘𝑙)))
96	87, 94, 95	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 29101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
98	97	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 29085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((Fun (iEdg‘𝐺) ∧ 𝑙 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑙) ∈ (Edg‘𝐺))
101	99, 90, 100	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐺)‘𝑙) ∈ (Edg‘𝐺))
102	101, 6	eleqtrrdi 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐺)‘𝑙) ∈ 𝐼)
103		eleq1 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3161	. . . . . . . . . . . . . . . . 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 1119	. . . . . . . . . . . . . . . 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 3161	. . . . . . . . . . 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 1932	. . . . . 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 1537 ∃wex 1777 ∈ wcel 2108 ∀wral 3067 ∃wrex 3076 ⊆ wss 3976 dom cdm 5700 “ cima 5703 Fun wfun 6567 ⟶wf 6569 –1-1→wf1 6570 –onto→wfo 6571 –1-1-onto→wf1o 6572 ‘cfv 6573 (class class class)co 7448 Vtxcvtx 29031 iEdgciedg 29032 Edgcedg 29082 UHGraphcuhgr 29091 GraphIso cgrim 47745

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-pow 5383 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-rab 3444 df-v 3490 df-sbc 3805 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-ov 7451 df-oprab 7452 df-mpo 7453 df-map 8886 df-edg 29083 df-uhgr 29093 df-grim 47748

This theorem is referenced by: grimgrtri 47798

W3C validator