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 48431

Description: Lemma for clnbgrgrim 48432: 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 2832	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ 𝐸 ↔ 𝐾 ∈ (Edg‘𝐻))
3		eqid 2740	. . . . . . . . . . . . . . 15 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
4	3	uhgredgiedgb 29220	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ UHGraph → (𝐾 ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
5	2, 4	bitrid 284	. . . . . . . . . . . . 13 ⊢ (𝐻 ∈ UHGraph → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
6	5	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
7	6	3ad2ant3 1141	. . . . . . . . . . 11 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
8	7	adantr 481	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
9		sseq2 3948	. . . . . . . . . . . . . 14 ⊢ (𝐾 = ((iEdg‘𝐻)‘𝑘) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 ↔ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)))
10	9	adantl 482	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝐾 = ((iEdg‘𝐻)‘𝑘)) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 ↔ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)))
11		simp1 1142	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝐹:𝑉–1-1-onto→𝑊)
12		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑌 ∈ 𝑊)
13	11, 12	anim12i 619	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
14		f1ocnvdm 7236	. . . . . . . . . . . . . . . . . . 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 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑋 ∈ 𝑉)
17	16	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → 𝑋 ∈ 𝑉)
18	15, 17	jca 516	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((^◡𝐹‘𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉))
19	18	ad2antrr 732	. . . . . . . . . . . . . . . 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 29160	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
22	21	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → Fun (iEdg‘𝐺))
23	22	3ad2ant3 1141	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → Fun (iEdg‘𝐺))
24	23	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → Fun (iEdg‘𝐺))
25		simpl2l 1233	. . . . . . . . . . . . . . . . . . . . . 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 7236	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺))
27	25, 26	sylan 586	. . . . . . . . . . . . . . . . . . . . 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 516	. . . . . . . . . . . . . . . . . . . 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 29144	. . . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ∈ (Edg‘𝐺))
32		sseq2 3948	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) → ({𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒 ↔ {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
33	32	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) ∧ 𝑒 = ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → ({𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒 ↔ {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
34		2fveq3 6839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (^◡𝑗‘𝑘) → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))))
35		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = (^◡𝑗‘𝑘) → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))
36	35	imaeq2d 6019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (^◡𝑗‘𝑘) → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
37	34, 36	eqeq12d 2756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = (^◡𝑗‘𝑘) → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
38	37	rspcv 3563	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
39	38	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))
41		simp1 1142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → 𝑘 ∈ dom (iEdg‘𝐻))
42	40, 41	anim12i 619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
47		sseq2 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) ↔ {(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
48	47	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) ↔ {(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
49		f1ofn 6775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹 Fn 𝑉)
50	49	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → 𝐹 Fn 𝑉)
51		simpr3l 1241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → 𝑋 ∈ 𝑉)
52		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝐹:𝑉–1-1-onto→𝑊)
53	12	3ad2ant3 1141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → 𝑌 ∈ 𝑊)
54	52, 53	anim12i 619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → (𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑌) ∈ 𝑉))
57	56	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑌) ∈ 𝑉))
58		fnimapr 6917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
61		f1ocnvfv2 7228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {(𝐹‘𝑋), (𝐹‘(^◡𝐹‘𝑌))} = {(𝐹‘𝑋), 𝑌})
64	59, 63	eqtr2d 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {(𝐹‘𝑋), 𝑌} = (𝐹 “ {𝑋, (^◡𝐹‘𝑌)}))
65	64	sseq1d 3953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ({(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ (𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
66		f1of1 6773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–1-1→𝑊)
67	66	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝐹:𝑉–1-1→𝑊)
68	67	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → 𝐹:𝑉–1-1→𝑊)
69	51, 55	prssd 4760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → {𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑉)
70	69	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑉)
71		simpr2l 1239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 29158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐺 ∈ UHGraph ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ⊆ 𝑉)
74	71, 73	sylan 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ⊆ 𝑉)
75		f1imass 7215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐹:𝑉–1-1→𝑊 ∧ ({𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑉 ∧ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ⊆ 𝑉)) → ((𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
76	68, 70, 74, 75	syl12anc 842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
77	76	biimpd 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
78	65, 77	sylbid 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ({(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
79	78	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (^◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
81	80	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 413	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1361	. . . . . . . . . . . . . . . . . . . . . . . 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 454	. . . . . . . . . . . . . . . . . . . . . 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 1354	. . . . . . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . . . . . 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 3569	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ∃𝑒 ∈ (Edg‘𝐺){𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒)
94	93	olcd 880	. . . . . . . . . . . . . . . 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 48326	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋) ↔ (((^◡𝐹‘𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ ((^◡𝐹‘𝑌) = 𝑋 ∨ ∃𝑒 ∈ (Edg‘𝐺){𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒)))
97	19, 94, 96	sylanbrc 589	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))
98	97	ex 413	. . . . . . . . . . . . . 14 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
99	98	adantr 481	. . . . . . . . . . . . 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 241	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝐾 = ((iEdg‘𝐻)‘𝑘)) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
101	100	ex 413	. . . . . . . . . . 11 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝐾 = ((iEdg‘𝐻)‘𝑘) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))
102	101	rexlimdva 3141	. . . . . . . . . 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 241	. . . . . . . . 9 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐾 ∈ 𝐸 → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))
104	103	impd 411	. . . . . . . 8 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
105	104	3exp1 1359	. . . . . . 7 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))))
106	105	exlimdv 1940	. . . . . 6 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))))
107	106	imp 407	. . . . 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 48381	. . . . 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 1354	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))
112		fveqeq2 6843	. . . 4 ⊢ (𝑛 = (^◡𝐹‘𝑌) → ((𝐹‘𝑛) = 𝑌 ↔ (𝐹‘(^◡𝐹‘𝑌)) = 𝑌))
113	112	adantl 482	. . 3 ⊢ (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) ∧ 𝑛 = (^◡𝐹‘𝑌)) → ((𝐹‘𝑛) = 𝑌 ↔ (𝐹‘(^◡𝐹‘𝑌)) = 𝑌))
114	72, 108	grimf1o 48382	. . . . . . 7 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊)
115	114, 12	anim12i 619	. . . . . 6 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
116	115	3adant1 1136	. . . . 5 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
117	116	adantr 481	. . . 4 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
118	117, 61	syl 17	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → (𝐹‘(^◡𝐹‘𝑌)) = 𝑌)
119	111, 113, 118	rspcedvd 3569	. 2 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑌)
120	119	ex 413	1 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑌))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 853 ∧ w3a 1092 = wceq 1547 ∃wex 1786 ∈ wcel 2119 ∀wral 3054 ∃wrex 3064 ⊆ wss 3890 {cpr 4564 ^◡ccnv 5624 dom cdm 5625 “ cima 5628 Fun wfun 6486 Fn wfn 6487 –1-1→wf1 6489 –1-1-onto→wf1o 6491 ‘cfv 6492 (class class class)co 7363 Vtxcvtx 29090 iEdgciedg 29091 Edgcedg 29141 UHGraphcuhgr 29150 ClNeighbVtx cclnbgr 48316 GraphIso cgrim 48373

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-ral 3055 df-rex 3065 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-iun 4930 df-br 5080 df-opab 5142 df-mpt 5161 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7366 df-oprab 7367 df-mpo 7368 df-1st 7938 df-2nd 7939 df-map 8772 df-edg 29142 df-uhgr 29152 df-clnbgr 48317 df-grim 48376

This theorem is referenced by: clnbgrgrim 48432

W3C validator