clnbgrgrimlem - Mathbox for Alexander van der Vekens

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

Theorem clnbgrgrimlem 49124

Description: Lemma for clnbgrgrim 49125: For two isomorphic hypergraphs, if there is an edge connecting the image of a vertex of the first graph with a vertex of the second graph, the vertex of the second graph is the image of a neighbor of the vertex of the first graph. (Contributed by AV, 2-Jun-2025.)

**Hypotheses**
Ref	Expression
clnbgrgrim.v	⊢ 𝑉 = (Vtx‘𝐺)
clnbgrgrimlem.w	⊢ 𝑊 = (Vtx‘𝐻)
clnbgrgrimlem.e	⊢ 𝐸 = (Edg‘𝐻)

**Assertion**
Ref	Expression
clnbgrgrimlem	⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑌))

Distinct variable groups: 𝑛,𝐹 𝑛,𝐺 𝑛,𝐻 𝑛,𝑉 𝑛,𝑋 𝑛,𝐸 𝑛,𝐾 𝑛,𝑊 𝑛,𝑌

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

Step	Hyp	Ref	Expression
1		clnbgrgrimlem.e	. . . . . . . . . . . . . . 15 ⊢ 𝐸 = (Edg‘𝐻)
2	1	eleq2i 2852	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ 𝐸 ↔ 𝐾 ∈ (Edg‘𝐻))
3		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
4	3	uhgredgiedgb 29709	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ UHGraph → (𝐾 ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
5	2, 4	bitrid 286	. . . . . . . . . . . . 13 ⊢ (𝐻 ∈ UHGraph → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
6	5	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
7	6	3ad2ant3 1153	. . . . . . . . . . 11 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
8	7	adantr 486	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
9		sseq2 3934	. . . . . . . . . . . . . 14 ⊢ (𝐾 = ((iEdg‘𝐻)‘𝑘) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 ↔ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)))
10	9	adantl 487	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝐾 = ((iEdg‘𝐻)‘𝑘)) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 ↔ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)))
11		simp1 1154	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝐹:𝑉–1-1-onto→𝑊)
12		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑌 ∈ 𝑊)
13	11, 12	anim12i 625	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
14		f1ocnvdm 7293	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊) → (^◡𝐹‘𝑌) ∈ 𝑉)
15	13, 14	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (^◡𝐹‘𝑌) ∈ 𝑉)
16		simpl 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑋 ∈ 𝑉)
17	16	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → 𝑋 ∈ 𝑉)
18	15, 17	jca 521	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((^◡𝐹‘𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉))
19	18	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((^◡𝐹‘𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉))
20		eqid 2760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
21	20	uhgrfun 29649	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
22	21	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → Fun (iEdg‘𝐺))
23	22	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → Fun (iEdg‘𝐺))
24	23	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → Fun (iEdg‘𝐺))
25		simpl2l 1245	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))
26		f1ocnvdm 7293	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺))
27	25, 26	sylan 592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺))
28	24, 27	jca 521	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (Fun (iEdg‘𝐺) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)))
29	20	iedgedg 29633	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Fun (iEdg‘𝐺) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ∈ (Edg‘𝐺))
30	28, 29	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ∈ (Edg‘𝐺))
31	30	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ∈ (Edg‘𝐺))
32		sseq2 3934	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) → ({𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒 ↔ {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
33	32	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) ∧ 𝑒 = ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → ({𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒 ↔ {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
34		2fveq3 6890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (^◡𝑗‘𝑘) → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))))
35		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = (^◡𝑗‘𝑘) → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))
36	35	imaeq2d 6051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (^◡𝑗‘𝑘) → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
37	34, 36	eqeq12d 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = (^◡𝑗‘𝑘) → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
38	37	rspcv 3572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
39	38	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
40		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))
41		simp1 1154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → 𝑘 ∈ dom (iEdg‘𝐻))
42	40, 41	anim12i 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)))
43	42	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)))
44		f1ocnvfv2 7285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑗‘(^◡𝑗‘𝑘)) = 𝑘)
45	43, 44	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝑗‘(^◡𝑗‘𝑘)) = 𝑘)
46	45	fveqeq2d 6893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
47		sseq2 3934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) ↔ {(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
48	47	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) ↔ {(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
49		f1ofn 6825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹 Fn 𝑉)
50	49	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → 𝐹 Fn 𝑉)
51		simpr3l 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → 𝑋 ∈ 𝑉)
52		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝐹:𝑉–1-1-onto→𝑊)
53	12	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → 𝑌 ∈ 𝑊)
54	52, 53	anim12i 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
55	54, 14	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → (^◡𝐹‘𝑌) ∈ 𝑉)
56	50, 51, 55	3jca 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → (𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑌) ∈ 𝑉))
57	56	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑌) ∈ 𝑉))
58		fnimapr 6968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑌) ∈ 𝑉) → (𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) = {(𝐹‘𝑋), (𝐹‘(^◡𝐹‘𝑌))})
59	57, 58	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) = {(𝐹‘𝑋), (𝐹‘(^◡𝐹‘𝑌))})
60	54	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
61		f1ocnvfv2 7285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊) → (𝐹‘(^◡𝐹‘𝑌)) = 𝑌)
62	60, 61	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹‘(^◡𝐹‘𝑌)) = 𝑌)
63	62	preq2d 4697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {(𝐹‘𝑋), (𝐹‘(^◡𝐹‘𝑌))} = {(𝐹‘𝑋), 𝑌})
64	59, 63	eqtr2d 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {(𝐹‘𝑋), 𝑌} = (𝐹 “ {𝑋, (^◡𝐹‘𝑌)}))
65	64	sseq1d 3939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ({(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ (𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
66		f1of1 6823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–1-1→𝑊)
67	66	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝐹:𝑉–1-1→𝑊)
68	67	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → 𝐹:𝑉–1-1→𝑊)
69	51, 55	prssd 4777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → {𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑉)
70	69	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑉)
71		simpr2l 1251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → 𝐺 ∈ UHGraph)
72		clnbgrgrim.v	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ 𝑉 = (Vtx‘𝐺)
73	72, 20	uhgrss 29647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐺 ∈ UHGraph ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ⊆ 𝑉)
74	71, 73	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ⊆ 𝑉)
75		f1imass 7268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐹:𝑉–1-1→𝑊 ∧ ({𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑉 ∧ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ⊆ 𝑉)) → ((𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
76	68, 70, 74, 75	syl12anc 850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
77	76	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
78	65, 77	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ({(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
79	78	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))) → ({(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
80	48, 79	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
81	80	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
82	46, 81	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
83	39, 82	syld 48	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
84	83	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → ((^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))))
85	84	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))))
86	85	3exp2 1373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (𝑘 ∈ dom (iEdg‘𝐻) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))))))
87	86	com25 100	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝑘 ∈ dom (iEdg‘𝐻) → ((^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))))))
88	87	expimpd 459	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝑘 ∈ dom (iEdg‘𝐻) → ((^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))))))
89	88	3imp1 1366	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝑘 ∈ dom (iEdg‘𝐻) → ((^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))))
90	89	imp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
91	27, 90	mpd 16	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
92	91	imp 412	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))
93	31, 33, 92	rspcedvd 3578	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ∃𝑒 ∈ (Edg‘𝐺){𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒)
94	93	olcd 888	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((^◡𝐹‘𝑌) = 𝑋 ∨ ∃𝑒 ∈ (Edg‘𝐺){𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒))
95		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
96	72, 95	clnbgrel 49019	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋) ↔ (((^◡𝐹‘𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ ((^◡𝐹‘𝑌) = 𝑋 ∨ ∃𝑒 ∈ (Edg‘𝐺){𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒)))
97	19, 94, 96	sylanbrc 595	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))
98	97	ex 418	. . . . . . . . . . . . . 14 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
99	98	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝐾 = ((iEdg‘𝐻)‘𝑘)) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
100	10, 99	sylbid 243	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝐾 = ((iEdg‘𝐻)‘𝑘)) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
101	100	ex 418	. . . . . . . . . . 11 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝐾 = ((iEdg‘𝐻)‘𝑘) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))
102	101	rexlimdva 3163	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))
103	8, 102	sylbid 243	. . . . . . . . 9 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐾 ∈ 𝐸 → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))
104	103	impd 416	. . . . . . . 8 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
105	104	3exp1 1371	. . . . . . 7 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))))
106	105	exlimdv 1965	. . . . . 6 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))))
107	106	imp 412	. . . . 5 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))))
108		clnbgrgrimlem.w	. . . . . 6 ⊢ 𝑊 = (Vtx‘𝐻)
109	72, 108, 20, 3	grimprop 49074	. . . . 5 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
110	107, 109	syl11 34	. . . 4 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐹 ∈ (𝐺 GraphIso 𝐻) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))))
111	110	3imp1 1366	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))
112		fveqeq2 6894	. . . 4 ⊢ (𝑛 = (^◡𝐹‘𝑌) → ((𝐹‘𝑛) = 𝑌 ↔ (𝐹‘(^◡𝐹‘𝑌)) = 𝑌))
113	112	adantl 487	. . 3 ⊢ (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) ∧ 𝑛 = (^◡𝐹‘𝑌)) → ((𝐹‘𝑛) = 𝑌 ↔ (𝐹‘(^◡𝐹‘𝑌)) = 𝑌))
114	72, 108	grimf1o 49075	. . . . . . 7 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊)
115	114, 12	anim12i 625	. . . . . 6 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
116	115	3adant1 1148	. . . . 5 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
117	116	adantr 486	. . . 4 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
118	117, 61	syl 18	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → (𝐹‘(^◡𝐹‘𝑌)) = 𝑌)
119	111, 113, 118	rspcedvd 3578	. 2 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑌)
120	119	ex 418	1 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑌))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∃wex 1811 ∈ wcel 2144 ∀wral 3076 ∃wrex 3086 ⊆ wss 3895 {cpr 4586 ^◡ccnv 5649 dom cdm 5650 “ cima 5653 Fun wfun 6532 Fn wfn 6533 –1-1→wf1 6535 –1-1-onto→wf1o 6537 ‘cfv 6538 (class class class)co 7420 Vtxcvtx 29579 iEdgciedg 29580 Edgcedg 29630 UHGraphcuhgr 29639 ClNeighbVtx cclnbgr 49009 GraphIso cgrim 49066

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-ov 7423 df-oprab 7424 df-mpo 7425 df-1st 8001 df-2nd 8002 df-map 8852 df-edg 29631 df-uhgr 29641 df-clnbgr 49010 df-grim 49069

This theorem is used by: clnbgrgrim 49125

W3C validator