clnbgrgrim - Mathbox for Alexander van der Vekens

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

Theorem clnbgrgrim 48432

Description: Graph isomorphisms between hypergraphs map closed neighborhoods onto closed neighborhoods. (Contributed by AV, 2-Jun-2025.)

**Hypothesis**
Ref	Expression
clnbgrgrim.v	⊢ 𝑉 = (Vtx‘𝐺)

**Assertion**
Ref	Expression
clnbgrgrim	⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝐻 ClNeighbVtx (𝐹‘𝑋)) = (𝐹 “ (𝐺 ClNeighbVtx 𝑋)))

Proof of Theorem clnbgrgrim Dummy variables 𝑒 𝑔 𝑖 𝑗 𝑘 𝑛 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveqeq2 6843	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑋 → ((𝐹‘𝑛) = (𝐹‘𝑋) ↔ (𝐹‘𝑋) = (𝐹‘𝑋)))
2		clnbgrgrim.v	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (Vtx‘𝐺)
3	2	clnbgrvtxel 48327	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
4	3	3ad2ant3 1141	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
5		eqidd 2741	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) = (𝐹‘𝑋))
6	1, 4, 5	rspcedvdw 3570	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋))
7	6	adantr 481	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋))
8		eqeq2 2752	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐹‘𝑋) → ((𝐹‘𝑛) = 𝑥 ↔ (𝐹‘𝑛) = (𝐹‘𝑋)))
9	8	rexbidv 3164	. . . . . . . . . 10 ⊢ (𝑥 = (𝐹‘𝑋) → (∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥 ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋)))
10	7, 9	syl5ibrcom 248	. . . . . . . . 9 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑥 = (𝐹‘𝑋) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
11		simpl2 1199	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph))
12		simpl1 1198	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → 𝐹 ∈ (𝐺 GraphIso 𝐻))
13		simp3 1144	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
14		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) → 𝑥 ∈ (Vtx‘𝐻))
15	13, 14	anim12i 619	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑋 ∈ 𝑉 ∧ 𝑥 ∈ (Vtx‘𝐻)))
16		eqid 2740	. . . . . . . . . . . . 13 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
17		eqid 2740	. . . . . . . . . . . . 13 ⊢ (Edg‘𝐻) = (Edg‘𝐻)
18	2, 16, 17	clnbgrgrimlem 48431	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑥 ∈ (Vtx‘𝐻))) → ((𝑒 ∈ (Edg‘𝐻) ∧ {(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
19	11, 12, 15, 18	syl3anc 1379	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ((𝑒 ∈ (Edg‘𝐻) ∧ {(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
20	19	expd 416	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑒 ∈ (Edg‘𝐻) → ({(𝐹‘𝑋), 𝑥} ⊆ 𝑒 → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥)))
21	20	rexlimdv 3139	. . . . . . . . 9 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒 → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
22	10, 21	jaod 865	. . . . . . . 8 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
23	22	expimpd 454	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
24		eqid 2740	. . . . . . . . 9 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
25		eqid 2740	. . . . . . . . 9 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
26	2, 16, 24, 25	grimprop 48381	. . . . . . . 8 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
27		f1of 6774	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉⟶(Vtx‘𝐻))
28	27	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → 𝐹:𝑉⟶(Vtx‘𝐻))
29	28	3ad2ant1 1139	. . . . . . . . . . . . . 14 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝐹:𝑉⟶(Vtx‘𝐻))
30	29	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → 𝐹:𝑉⟶(Vtx‘𝐻))
31	2	clnbgrisvtx 48328	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐺 ClNeighbVtx 𝑋) → 𝑛 ∈ 𝑉)
32	31	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) → 𝑛 ∈ 𝑉)
33	32	adantr 481	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → 𝑛 ∈ 𝑉)
34	30, 33	ffvelcdmd 7033	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → (𝐹‘𝑛) ∈ (Vtx‘𝐻))
35		eleq1 2828	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑛) → (𝑥 ∈ (Vtx‘𝐻) ↔ (𝐹‘𝑛) ∈ (Vtx‘𝐻)))
36	35	eqcoms 2748	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑛) = 𝑥 → (𝑥 ∈ (Vtx‘𝐻) ↔ (𝐹‘𝑛) ∈ (Vtx‘𝐻)))
37	36	adantl 482	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → (𝑥 ∈ (Vtx‘𝐻) ↔ (𝐹‘𝑛) ∈ (Vtx‘𝐻)))
38	34, 37	mpbird 258	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → 𝑥 ∈ (Vtx‘𝐻))
39		simp3 1144	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
40	29, 39	ffvelcdmd 7033	. . . . . . . . . . . 12 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) ∈ (Vtx‘𝐻))
41	40	ad2antrr 732	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → (𝐹‘𝑋) ∈ (Vtx‘𝐻))
42		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
43	2, 42	clnbgrel 48326	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝑛 = 𝑋 ∨ ∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘)))
44		fveq2 6834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑋 → (𝐹‘𝑛) = (𝐹‘𝑋))
45	44	orcd 879	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑋 → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
46	45	2a1d 26	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑋 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
47	24	uhgredgiedgb 29220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐺 ∈ UHGraph → (𝑘 ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗)))
48	47	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑘 ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗)))
49	48	3ad2ant2 1140	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝑘 ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗)))
50	49	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗))
51		2fveq3 6839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐻)‘(𝑔‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑗)))
52		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑗))
53	52	imaeq2d 6019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = 𝑗 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
54	51, 53	eqeq12d 2756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑖 = 𝑗 → (((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))))
55	54	rspcv 3563	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))))
56	55	3ad2ant3 1141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))))
57		sseq2 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 ↔ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗)))
58	57	3ad2ant3 1141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)) ∧ 𝑘 = ((iEdg‘𝐺)‘𝑗)) → ({𝑋, 𝑛} ⊆ 𝑘 ↔ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗)))
59		sseq2 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑒 = ((iEdg‘𝐻)‘(𝑔‘𝑗)) → ({(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒 ↔ {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ ((iEdg‘𝐻)‘(𝑔‘𝑗))))
60	25	uhgrfun 29160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝐻 ∈ UHGraph → Fun (iEdg‘𝐻))
61	60	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → Fun (iEdg‘𝐻))
62	61	3ad2ant3 1141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → Fun (iEdg‘𝐻))
63		f1of 6774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑔:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
64	63	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝑔:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
65	64	3ad2ant1 1139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝑔:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
66	65	ffvelcdmda 7032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → (𝑔‘𝑗) ∈ dom (iEdg‘𝐻))
67	25	iedgedg 29144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑔‘𝑗) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
68	62, 66, 67	syl2an2r 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
69	68	3adant2 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
70	69	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
71	70	3ad2ant1 1139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
72		f1ofn 6775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹 Fn 𝑉)
73	72	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝐹 Fn 𝑉)
74	73	3ad2ant1 1139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝐹 Fn 𝑉)
75	74	3ad2ant1 1139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → 𝐹 Fn 𝑉)
76	75	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) → 𝐹 Fn 𝑉)
77		pm3.22 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉))
78	76, 77	anim12i 619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)))
79	78	3adant2 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)))
80		3anass 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ↔ (𝐹 Fn 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)))
81	79, 80	sylibr 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉))
82		fnimapr 6917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → (𝐹 “ {𝑋, 𝑛}) = {(𝐹‘𝑋), (𝐹‘𝑛)})
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 “ {𝑋, 𝑛}) = {(𝐹‘𝑋), (𝐹‘𝑛)})
84		imass2 6061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ({𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) → (𝐹 “ {𝑋, 𝑛}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
85	84	3ad2ant2 1140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 “ {𝑋, 𝑛}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
86	83, 85	eqsstrrd 3957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
87		simp1r 1205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
88	86, 87	sseqtrrd 3959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ ((iEdg‘𝐻)‘(𝑔‘𝑗)))
89	59, 71, 88	rspcedvdw 3570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)
90	89	3exp 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) → ({𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
91	90	3adant3 1138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)) ∧ 𝑘 = ((iEdg‘𝐺)‘𝑗)) → ({𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
92	58, 91	sylbid 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)) ∧ 𝑘 = ((iEdg‘𝐺)‘𝑗)) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
93	92	3exp 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)) → (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))))
94	56, 93	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))))
95	94	3exp 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → (𝑋 ∈ 𝑉 → (𝑗 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))))))
96	95	com34 91	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → (𝑋 ∈ 𝑉 → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝑗 ∈ dom (iEdg‘𝐺) → (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))))))
97	96	3exp 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (𝑘 ∈ (Edg‘𝐺) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑋 ∈ 𝑉 → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝑗 ∈ dom (iEdg‘𝐺) → (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))))))))
98	97	com25 99	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑋 ∈ 𝑉 → (𝑘 ∈ (Edg‘𝐺) → (𝑗 ∈ dom (iEdg‘𝐺) → (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))))))))
99	98	expimpd 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑋 ∈ 𝑉 → (𝑘 ∈ (Edg‘𝐺) → (𝑗 ∈ dom (iEdg‘𝐺) → (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))))))))
100	99	exlimdv 1940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑋 ∈ 𝑉 → (𝑘 ∈ (Edg‘𝐺) → (𝑗 ∈ dom (iEdg‘𝐺) → (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))))))))
101	100	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑋 ∈ 𝑉 → (𝑘 ∈ (Edg‘𝐺) → (𝑗 ∈ dom (iEdg‘𝐺) → (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))))))
102	101	3imp 1116	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝑘 ∈ (Edg‘𝐺) → (𝑗 ∈ dom (iEdg‘𝐺) → (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))))
103	102	imp31 418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
104	103	rexlimdva 3141	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → (∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
105	50, 104	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
106	105	ex 413	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝑘 ∈ (Edg‘𝐺) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
107	106	com14 96	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑘 ∈ (Edg‘𝐺) → ({𝑋, 𝑛} ⊆ 𝑘 → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
108	107	imp 407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ({𝑋, 𝑛} ⊆ 𝑘 → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
109	108	3imp 1116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) ∧ {𝑋, 𝑛} ⊆ 𝑘 ∧ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉)) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)
110	109	olcd 880	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) ∧ {𝑋, 𝑛} ⊆ 𝑘 ∧ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉)) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
111	110	3exp 1125	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ({𝑋, 𝑛} ⊆ 𝑘 → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
112	111	rexlimdva 3141	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘 → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
113	112	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
114	46, 113	jaoi 863	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 = 𝑋 ∨ ∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘) → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
115	114	impcom 408	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝑛 = 𝑋 ∨ ∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘)) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
116	43, 115	sylbi 218	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (𝐺 ClNeighbVtx 𝑋) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
117	116	impcom 408	. . . . . . . . . . . . 13 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
118	117	adantr 481	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
119		eqeq1 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑛) → (𝑥 = (𝐹‘𝑋) ↔ (𝐹‘𝑛) = (𝐹‘𝑋)))
120		preq2 4673	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐹‘𝑛) → {(𝐹‘𝑋), 𝑥} = {(𝐹‘𝑋), (𝐹‘𝑛)})
121	120	sseq1d 3953	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐹‘𝑛) → ({(𝐹‘𝑋), 𝑥} ⊆ 𝑒 ↔ {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
122	121	rexbidv 3164	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑛) → (∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒 ↔ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
123	119, 122	orbi12d 924	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑛) → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) ↔ ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
124	123	eqcoms 2748	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑛) = 𝑥 → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) ↔ ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
125	124	adantl 482	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) ↔ ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
126	118, 125	mpbird 258	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒))
127	38, 41, 126	jca31 519	. . . . . . . . . 10 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)))
128	127	ex 413	. . . . . . . . 9 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) → ((𝐹‘𝑛) = 𝑥 → ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒))))
129	128	rexlimdva 3141	. . . . . . . 8 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥 → ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒))))
130	26, 129	syl3an1 1169	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥 → ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒))))
131	23, 130	impbid 213	. . . . . 6 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
132	131	3exp 1125	. . . . 5 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑋 ∈ 𝑉 → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))))
133	132	impcom 408	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝑋 ∈ 𝑉 → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥)))
134	133	imp 407	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
135	16, 17	clnbgrel 48326	. . . 4 ⊢ (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)))
136	135	a1i 11	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒))))
137	2, 16	grimf1o 48382	. . . . . 6 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→(Vtx‘𝐻))
138	137, 72	syl 17	. . . . 5 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹 Fn 𝑉)
139	138	adantl 482	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → 𝐹 Fn 𝑉)
140	2	clnbgrssvtx 48329	. . . . 5 ⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉
141	140	a1i 11	. . . 4 ⊢ (𝑋 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉)
142		fvelimab 6906	. . . 4 ⊢ ((𝐹 Fn 𝑉 ∧ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉) → (𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
143	139, 141, 142	syl2an 602	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
144	134, 136, 143	3bitr4d 312	. 2 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ 𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋))))
145	144	eqrdv 2738	1 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝐻 ClNeighbVtx (𝐹‘𝑋)) = (𝐹 “ (𝐺 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 dom cdm 5625 “ cima 5628 Fun wfun 6486 Fn wfn 6487 ⟶wf 6488 –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: uhgrimgrlim 48485

W3C validator