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 48645

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 2761	. . . . . 6 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
3		eqid 2761	. . . . . 6 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
4		eqid 2761	. . . . . 6 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
5	1, 2, 3, 4	grimprop 48593	. . . . 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 2853	. . . . . . . . . . 11 ⊢ (𝐾 ∈ 𝐼 ↔ 𝐾 ∈ (Edg‘𝐺))
8	3	uhgredgiedgb 29442	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ UHGraph → (𝐾 ∈ (Edg‘𝐺) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘)))
9	8	ad2antll 741	. . . . . . . . . . 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 286	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (𝐾 ∈ 𝐼 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝐾 = ((iEdg‘𝐺)‘𝑘)))
11		2fveq3 6886	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑘 → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘𝑘)))
12		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑘 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑘))
13	12	imaeq2d 6062	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑘 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))
14	11, 13	eqeq12d 2777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑘 → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
15	14	rspcv 3576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
16	15	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
17	4	uhgrfun 29382	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐻 ∈ UHGraph → Fun (iEdg‘𝐻))
18	17	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → Fun (iEdg‘𝐻))
19		f1of 6820	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
20	19	ad2antll 741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → 𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
21		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → 𝑘 ∈ dom (iEdg‘𝐺))
22	20, 21	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → (𝑗‘𝑘) ∈ dom (iEdg‘𝐻))
23	4	iedgedg 29366	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑗‘𝑘) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ (Edg‘𝐻))
24		grimedg.e	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐸 = (Edg‘𝐻)
25	23, 24	eleqtrrdi 2872	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑗‘𝑘) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸)
26	18, 22, 25	syl2an2r 697	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸)
27		eleq1 2849	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) = ((iEdg‘𝐻)‘(𝑗‘𝑘)) → ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸 ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸))
28	27	eqcoms 2769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → ((𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸 ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐸))
29	26, 28	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) → (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸))
30	29	ex 417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)))
31	30	com23 87	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)))
32	16, 31	syld 48	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)))
33	32	com13 89	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)))
34	33	impr 459	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸))
35	34	impl 460	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)
36	35	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸)
37		imaeq2 6058	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑘) → (𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))
38	37	eleq1d 2846	. . . . . . . . . . . . . . 15 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑘) → ((𝐹 “ 𝐾) ∈ 𝐸 ↔ (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐸))
39	38	adantl 486	. . . . . . . . . . . . . 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 260	. . . . . . . . . . . . 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 29380	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ UHGraph ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉)
42	41	ex 417	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ UHGraph → (𝑘 ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉))
43	42	ad2antll 741	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (𝑘 ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉))
44	43	imp 411	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉)
45	44	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉)
46		sseq1 3961	. . . . . . . . . . . . . . 15 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑘) → (𝐾 ⊆ 𝑉 ↔ ((iEdg‘𝐺)‘𝑘) ⊆ 𝑉))
47	46	adantl 486	. . . . . . . . . . . . . 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 260	. . . . . . . . . . . . 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 520	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) ∧ 𝐾 = ((iEdg‘𝐺)‘𝑘)) → ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉))
50	49	ex 417	. . . . . . . . . . 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 243	. . . . . . . . 9 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (𝐾 ∈ 𝐼 → ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))
53	24	eleq2i 2853	. . . . . . . . . . . 12 ⊢ ((𝐹 “ 𝐾) ∈ 𝐸 ↔ (𝐹 “ 𝐾) ∈ (Edg‘𝐻))
54	4	uhgredgiedgb 29442	. . . . . . . . . . . . 13 ⊢ (𝐻 ∈ UHGraph → ((𝐹 “ 𝐾) ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)(𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘)))
55	54	ad2antrl 740	. . . . . . . . . . . 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 286	. . . . . . . . . . 11 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → ((𝐹 “ 𝐾) ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)(𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘)))
57		f1ofo 6828	. . . . . . . . . . . . . . . 16 ⊢ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑗:dom (iEdg‘𝐺)–onto→dom (iEdg‘𝐻))
58	57	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → 𝑗:dom (iEdg‘𝐺)–onto→dom (iEdg‘𝐻))
59	58	ad2antlr 739	. . . . . . . . . . . . . 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 7102	. . . . . . . . . . . . . 14 ⊢ ((𝑗:dom (iEdg‘𝐺)–onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃𝑙 ∈ dom (iEdg‘𝐺)𝑘 = (𝑗‘𝑙))
61	59, 60	sylan 591	. . . . . . . . . . . . 13 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃𝑙 ∈ dom (iEdg‘𝐺)𝑘 = (𝑗‘𝑙))
62		2fveq3 6886	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑙 → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘𝑙)))
63		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑙 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑙))
64	63	imaeq2d 6062	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑙 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)))
65	62, 64	eqeq12d 2777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑙 → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
66	65	rspcv 3576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
67	66	adantl 486	. . . . . . . . . . . . . . . . . . 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 6881	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = (𝑗‘𝑙) → ((iEdg‘𝐻)‘𝑘) = ((iEdg‘𝐻)‘(𝑗‘𝑙)))
69	68	eqeq2d 2772	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = (𝑗‘𝑙) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ↔ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))))
70	69	ad2antll 741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ↔ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))))
71		simpl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) → 𝐻 ∈ UHGraph)
72	71	ad2antrl 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → 𝐻 ∈ UHGraph)
73		simplrr 789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → 𝑘 ∈ dom (iEdg‘𝐻))
74		eleq1 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = (𝑗‘𝑙) → (𝑘 ∈ dom (iEdg‘𝐻) ↔ (𝑗‘𝑙) ∈ dom (iEdg‘𝐻)))
75	74	ad2antll 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → (𝑗‘𝑙) ∈ dom (iEdg‘𝐻))
77	2, 4	uhgrss 29380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐻 ∈ UHGraph ∧ (𝑗‘𝑙) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑙)) ⊆ (Vtx‘𝐻))
78	72, 76, 77	syl2an2r 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐻)‘(𝑗‘𝑙)) ⊆ (Vtx‘𝐻))
79	78	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙)) → ((𝐹 “ 𝐾) ⊆ (Vtx‘𝐻) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑙)) ⊆ (Vtx‘𝐻)))
81	80	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))) → (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻))
83		eqeq2 2773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙)) ↔ (𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
84	83	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙)) ↔ (𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))))
85		f1of1 6819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
86	85	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
87	86	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → 𝐺 ∈ UHGraph)
89	88	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → 𝐺 ∈ UHGraph)
90		simpl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙)) → 𝑙 ∈ dom (iEdg‘𝐺))
91	1, 3	uhgrss 29380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐺 ∈ UHGraph ∧ 𝑙 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉)
92	89, 90, 91	syl2an 607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉)
93	92	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) ⊆ (Vtx‘𝐻)) ∧ 𝐾 ⊆ 𝑉) → (𝐾 ⊆ 𝑉 ∧ ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉))
95		f1imaeq 7263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐹:𝑉–1-1→(Vtx‘𝐻) ∧ (𝐾 ⊆ 𝑉 ∧ ((iEdg‘𝐺)‘𝑙) ⊆ 𝑉)) → ((𝐹 “ 𝐾) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) ↔ 𝐾 = ((iEdg‘𝐺)‘𝑙)))
96	87, 94, 95	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 29382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
98	97	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → Fun (iEdg‘𝐺))
99	98	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → Fun (iEdg‘𝐺))
100	3	iedgedg 29366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((Fun (iEdg‘𝐺) ∧ 𝑙 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑙) ∈ (Edg‘𝐺))
101	99, 90, 100	syl2an 607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐺)‘𝑙) ∈ (Edg‘𝐺))
102	101, 6	eleqtrrdi 2872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((iEdg‘𝐺)‘𝑙) ∈ 𝐼)
103		eleq1 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝐾 = ((iEdg‘𝐺)‘𝑙) → (𝐾 ∈ 𝐼 ↔ ((iEdg‘𝐺)‘𝑙) ∈ 𝐼))
104	102, 103	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → (𝐾 = ((iEdg‘𝐺)‘𝑙) → 𝐾 ∈ 𝐼))
105	104	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) ∧ ((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙))) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙))) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))
114	113	exp31 424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘(𝑗‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
115	114	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . 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 243	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) ∧ (𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙))) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
117	116	exp31 424	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙)) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))))
118	117	com23 87	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → ((𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙)) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))))
119	118	com24 96	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → ((𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) → (((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙)) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))))
120	119	3imp 1126	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝐹 “ 𝐾) = ((iEdg‘𝐻)‘𝑘) ∧ ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) ∧ 𝑘 ∈ dom (iEdg‘𝐻))) → ((𝑙 ∈ dom (iEdg‘𝐺) ∧ 𝑘 = (𝑗‘𝑙)) → (((iEdg‘𝐻)‘(𝑗‘𝑙)) = (𝐹 “ ((iEdg‘𝐺)‘𝑙)) → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼))))
121	120	expdimp 457	. . . . . . . . . . . . . . . . . . 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 74	. . . . . . . . . . . . . . . . . 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 1135	. . . . . . . . . . . . . . . 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 100	. . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . 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 460	. . . . . . . . . . . . 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 16	. . . . . . . . . . . 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 243	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → ((𝐹 “ 𝐾) ∈ 𝐸 → (𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼)))
131	130	impd 415	. . . . . . . . 9 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉) → 𝐾 ∈ 𝐼))
132	52, 131	impbid 215	. . . . . . . 8 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph)) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))
133	132	exp31 424	. . . . . . 7 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))))
134	133	exlimdv 1961	. . . . . 6 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))))
135	134	imp 411	. . . . 5 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉))))
136	5, 135	syl 18	. . . 4 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → ((𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉))))
137	136	expd 420	. . 3 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐻 ∈ UHGraph → (𝐺 ∈ UHGraph → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))))
138	137	com13 89	. 2 ⊢ (𝐺 ∈ UHGraph → (𝐻 ∈ UHGraph → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))))
139	138	3imp 1126	1 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1568 ∃wex 1807 ∈ wcel 2141 ∀wral 3077 ∃wrex 3087 ⊆ wss 3904 dom cdm 5661 “ cima 5664 Fun wfun 6530 ⟶wf 6532 –1-1→wf1 6533 –onto→wfo 6534 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7410 Vtxcvtx 29312 iEdgciedg 29313 Edgcedg 29363 UHGraphcuhgr 29372 GraphIso cgrim 48585

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rab 3415 df-v 3455 df-sbc 3744 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-br 5109 df-opab 5173 df-mpt 5192 df-id 5556 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-map 8825 df-edg 29364 df-uhgr 29374 df-grim 48588

This theorem is referenced by: grimedgi 48646 grimgrtri 48659

W3C validator