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 47913

Description: Lemma for clnbgrgrim 47914: 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 2827	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ 𝐸 ↔ 𝐾 ∈ (Edg‘𝐻))
3		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
4	3	uhgredgiedgb 29110	. . . . . . . . . . . . . 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 3990	. . . . . . . . . . . . . 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 613	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊))
14		f1ocnvdm 7283	. . . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((^◡𝐹‘𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉))
20		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
21	20	uhgrfun 29050	. . . . . . . . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → Fun (iEdg‘𝐺))
25		simpl2l 1227	. . . . . . . . . . . . . . . . . . . . . 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 7283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺))
27	25, 26	sylan 580	. . . . . . . . . . . . . . . . . . . . 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 29034	. . . . . . . . . . . . . . . . . . . 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 3990	. . . . . . . . . . . . . . . . . . 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 6886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (^◡𝑗‘𝑘) → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))))
35		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = (^◡𝑗‘𝑘) → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))
36	35	imaeq2d 6052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (^◡𝑗‘𝑘) → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))))
37	34, 36	eqeq12d 2752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = (^◡𝑗‘𝑘) → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
38	37	rspcv 3602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑗‘(^◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
47		sseq2 3990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹 Fn 𝑉)
50	49	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → 𝐹 Fn 𝑉)
51		simpr3l 1235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {(𝐹‘𝑋), (𝐹‘(^◡𝐹‘𝑌))} = {(𝐹‘𝑋), 𝑌})
64	59, 63	eqtr2d 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {(𝐹‘𝑋), 𝑌} = (𝐹 “ {𝑋, (^◡𝐹‘𝑌)}))
65	64	sseq1d 3995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ({(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘))) ↔ (𝐹 “ {𝑋, (^◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)))))
66		f1of1 6822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → 𝐹:𝑉–1-1→𝑊)
69	51, 55	prssd 4803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 29048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐺 ∈ UHGraph ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ⊆ 𝑉)
74	71, 73	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (^◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(^◡𝑗‘𝑘)) ⊆ 𝑉)
75		f1imass 7262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1355	. . . . . . . . . . . . . . . . . . . . . . . 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 1348	. . . . . . . . . . . . . . . . . . . . 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 3608	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ∃𝑒 ∈ (Edg‘𝐺){𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒)
94	93	olcd 874	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((^◡𝐹‘𝑌) = 𝑋 ∨ ∃𝑒 ∈ (Edg‘𝐺){𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒))
95		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
96	72, 95	clnbgrel 47809	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋) ↔ (((^◡𝐹‘𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ ((^◡𝐹‘𝑌) = 𝑋 ∨ ∃𝑒 ∈ (Edg‘𝐺){𝑋, (^◡𝐹‘𝑌)} ⊆ 𝑒)))
97	19, 94, 96	sylanbrc 583	. . . . . . . . . . . . . . 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 3142	. . . . . . . . . 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 1353	. . . . . . 7 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))))
106	105	exlimdv 1933	. . . . . 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 47863	. . . . 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 1348	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → (^◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))
112		fveqeq2 6890	. . . 4 ⊢ (𝑛 = (^◡𝐹‘𝑌) → ((𝐹‘𝑛) = 𝑌 ↔ (𝐹‘(^◡𝐹‘𝑌)) = 𝑌))
113	112	adantl 481	. . 3 ⊢ (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) ∧ 𝑛 = (^◡𝐹‘𝑌)) → ((𝐹‘𝑛) = 𝑌 ↔ (𝐹‘(^◡𝐹‘𝑌)) = 𝑌))
114	72, 108	grimf1o 47864	. . . . . . 7 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊)
115	114, 12	anim12i 613	. . . . . 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 3608	. 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 847 ∧ w3a 1086 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ∀wral 3052 ∃wrex 3061 ⊆ wss 3931 {cpr 4608 ^◡ccnv 5658 dom cdm 5659 “ cima 5662 Fun wfun 6530 Fn wfn 6531 –1-1→wf1 6533 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7410 Vtxcvtx 28980 iEdgciedg 28981 Edgcedg 29031 UHGraphcuhgr 29040 ClNeighbVtx cclnbgr 47799 GraphIso cgrim 47855

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-id 5553 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6489 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-1st 7993 df-2nd 7994 df-map 8847 df-edg 29032 df-uhgr 29042 df-clnbgr 47800 df-grim 47858

This theorem is referenced by: clnbgrgrim 47914

W3C validator