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 47785

Description: Lemma for clnbgrgrim 47786: 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 2836	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ 𝐸 ↔ 𝐾 ∈ (Edg‘𝐻))
3		eqid 2740	. . . . . . . . . . . . . . 15 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
4	3	uhgredgiedgb 29161	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ UHGraph → (𝐾 ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
5	2, 4	bitrid 283	. . . . . . . . . . . . 13 ⊢ (𝐻 ∈ UHGraph → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
6	5	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
7	6	3ad2ant3 1135	. . . . . . . . . . 11 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
8	7	adantr 480	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
9		sseq2 4035	. . . . . . . . . . . . . 14 ⊢ (𝐾 = ((iEdg‘𝐻)‘𝑘) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 ↔ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)))
10	9	adantl 481	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝐾 = ((iEdg‘𝐻)‘𝑘)) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 ↔ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)))
11		simp1 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝐹:𝑉–1-1-onto→𝑊)
12		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑌 ∈ 𝑊)
13	11, 12	anim12i 612	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
14		f1ocnvdm 7321	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊) → (^◡𝐹‘𝑌) ∈ 𝑉)
15	13, 14	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (^◡𝐹‘𝑌) ∈ 𝑉)
16		simpl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑋 ∈ 𝑉)
17	16	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → 𝑋 ∈ 𝑉)
18	15, 17	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((^◡𝐹‘𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉))
19	18	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((^◡𝐹‘𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉))
20		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
21	20	uhgrfun 29101	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
22	21	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → Fun (iEdg‘𝐺))
23	22	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → Fun (iEdg‘𝐺))
24	23	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → Fun (iEdg‘𝐺))
25		simpl2l 1226	. . . . . . . . . . . . . . . . . . . . . 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 7321	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺))
27	25, 26	sylan 579	. . . . . . . . . . . . . . . . . . . . 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 511	. . . . . . . . . . . . . . . . . . . 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 29085	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Fun (iEdg‘𝐺) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ∈ (Edg‘𝐺))
30	28, 29	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ∈ (Edg‘𝐺))
31	30	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ∈ (Edg‘𝐺))
32		sseq2 4035	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) → ({𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒 ↔ {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
33	32	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) ∧ 𝑒 = ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → ({𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒 ↔ {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
34		2fveq3 6925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (^◡𝑗‘𝑘) → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))))
35		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = (^◡𝑗‘𝑘) → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))
36	35	imaeq2d 6089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (^◡𝑗‘𝑘) → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
37	34, 36	eqeq12d 2756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = (^◡𝑗‘𝑘) → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
38	37	rspcv 3631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
39	38	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))
41		simp1 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → 𝑘 ∈ dom (iEdg‘𝐻))
42	40, 41	anim12i 612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑗‘(^◡𝑗‘𝑘)) = 𝑘)
45	43, 44	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝑗‘(^◡𝑗‘𝑘)) = 𝑘)
46	45	fveqeq2d 6928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
47		sseq2 4035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) ↔ {(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
48	47	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) ↔ {(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
49		f1ofn 6863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹 Fn 𝑉)
50	49	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → 𝐹 Fn 𝑉)
51		simpr3l 1234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → 𝑋 ∈ 𝑉)
52		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝐹:𝑉–1-1-onto→𝑊)
53	12	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → 𝑌 ∈ 𝑊)
54	52, 53	anim12i 612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
55	54, 14	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → (^◡𝐹‘𝑌) ∈ 𝑉)
56	50, 51, 55	3jca 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → (𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑌) ∈ 𝑉))
57	56	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑌) ∈ 𝑉))
58		fnimapr 7005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑌) ∈ 𝑉) → (𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) = {(𝐹‘𝑋), (𝐹‘(^◡𝐹‘𝑌))})
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) = {(𝐹‘𝑋), (𝐹‘(^◡𝐹‘𝑌))})
60	54	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
61		f1ocnvfv2 7313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊) → (𝐹‘(^◡𝐹‘𝑌)) = 𝑌)
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹‘(^◡𝐹‘𝑌)) = 𝑌)
63	62	preq2d 4765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {(𝐹‘𝑋), (𝐹‘(^◡𝐹‘𝑌))} = {(𝐹‘𝑋), 𝑌})
64	59, 63	eqtr2d 2781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {(𝐹‘𝑋), 𝑌} = (𝐹 “ {𝑋, (^◡𝐹‘𝑌)}))
65	64	sseq1d 4040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ({(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ (𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
66		f1of1 6861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–1-1→𝑊)
67	66	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝐹:𝑉–1-1→𝑊)
68	67	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → 𝐹:𝑉–1-1→𝑊)
69	51, 55	prssd 4847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → {𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑉)
70	69	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑉)
71		simpr2l 1232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 29099	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐺 ∈ UHGraph ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ⊆ 𝑉)
74	71, 73	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ⊆ 𝑉)
75		f1imass 7301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐹:𝑉–1-1→𝑊 ∧ ({𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑉 ∧ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ⊆ 𝑉)) → ((𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
76	68, 70, 74, 75	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
77	76	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
78	65, 77	sylbid 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ({(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
79	78	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
81	80	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 47	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . . . . . . . . . . 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 86	. . . . . . . . . . . . . . . . . . . . . . . . 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 1354	. . . . . . . . . . . . . . . . . . . . . . . 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 99	. . . . . . . . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . . . . . . . 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 1347	. . . . . . . . . . . . . . . . . . . . 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 406	. . . . . . . . . . . . . . . . . . . 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 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
92	91	imp 406	. . . . . . . . . . . . . . . . . 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 3637	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ∃𝑒 ∈ (Edg‘𝐺){𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒)
94	93	olcd 873	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((^◡𝐹‘𝑌) = 𝑋 ∨ ∃𝑒 ∈ (Edg‘𝐺){𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒))
95		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
96	72, 95	clnbgrel 47701	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋) ↔ (((^◡𝐹‘𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ ((^◡𝐹‘𝑌) = 𝑋 ∨ ∃𝑒 ∈ (Edg‘𝐺){𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒)))
97	19, 94, 96	sylanbrc 582	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))
98	97	ex 412	. . . . . . . . . . . . . 14 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
99	98	adantr 480	. . . . . . . . . . . . 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 240	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝐾 = ((iEdg‘𝐻)‘𝑘)) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
101	100	ex 412	. . . . . . . . . . 11 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝐾 = ((iEdg‘𝐻)‘𝑘) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))
102	101	rexlimdva 3161	. . . . . . . . . 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 240	. . . . . . . . 9 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐾 ∈ 𝐸 → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))
104	103	impd 410	. . . . . . . 8 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
105	104	3exp1 1352	. . . . . . 7 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))))
106	105	exlimdv 1932	. . . . . 6 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))))
107	106	imp 406	. . . . 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 47753	. . . . 5 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
110	107, 109	syl11 33	. . . 4 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐹 ∈ (𝐺 GraphIso 𝐻) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))))
111	110	3imp1 1347	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))
112		fveqeq2 6929	. . . 4 ⊢ (𝑛 = (^◡𝐹‘𝑌) → ((𝐹‘𝑛) = 𝑌 ↔ (𝐹‘(^◡𝐹‘𝑌)) = 𝑌))
113	112	adantl 481	. . 3 ⊢ (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) ∧ 𝑛 = (^◡𝐹‘𝑌)) → ((𝐹‘𝑛) = 𝑌 ↔ (𝐹‘(^◡𝐹‘𝑌)) = 𝑌))
114	72, 108	grimf1o 47754	. . . . . . 7 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊)
115	114, 12	anim12i 612	. . . . . 6 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
116	115	3adant1 1130	. . . . 5 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
117	116	adantr 480	. . . 4 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
118	117, 61	syl 17	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → (𝐹‘(^◡𝐹‘𝑌)) = 𝑌)
119	111, 113, 118	rspcedvd 3637	. 2 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑌)
120	119	ex 412	1 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑌))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 846 ∧ w3a 1087 = wceq 1537 ∃wex 1777 ∈ wcel 2108 ∀wral 3067 ∃wrex 3076 ⊆ wss 3976 {cpr 4650 ^◡ccnv 5699 dom cdm 5700 “ cima 5703 Fun wfun 6567 Fn wfn 6568 –1-1→wf1 6570 –1-1-onto→wf1o 6572 ‘cfv 6573 (class class class)co 7448 Vtxcvtx 29031 iEdgciedg 29032 Edgcedg 29082 UHGraphcuhgr 29091 ClNeighbVtx cclnbgr 47692 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-csb 3922 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-iun 5017 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-1st 8030 df-2nd 8031 df-map 8886 df-edg 29083 df-uhgr 29093 df-clnbgr 47693 df-grim 47748

This theorem is referenced by: clnbgrgrim 47786

W3C validator