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 48516

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 6870	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑋 → ((𝐹‘𝑛) = (𝐹‘𝑋) ↔ (𝐹‘𝑋) = (𝐹‘𝑋)))
2		clnbgrgrim.v	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (Vtx‘𝐺)
3	2	clnbgrvtxel 48411	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
4	3	3ad2ant3 1147	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
5		eqidd 2762	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) = (𝐹‘𝑋))
6	1, 4, 5	rspcedvdw 3583	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋))
7	6	adantr 484	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋))
8		eqeq2 2773	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐹‘𝑋) → ((𝐹‘𝑛) = 𝑥 ↔ (𝐹‘𝑛) = (𝐹‘𝑋)))
9	8	rexbidv 3185	. . . . . . . . . 10 ⊢ (𝑥 = (𝐹‘𝑋) → (∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥 ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋)))
10	7, 9	syl5ibrcom 249	. . . . . . . . 9 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑥 = (𝐹‘𝑋) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
11		simpl2 1205	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph))
12		simpl1 1204	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → 𝐹 ∈ (𝐺 GraphIso 𝐻))
13		simp3 1150	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
14		simpl 486	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) → 𝑥 ∈ (Vtx‘𝐻))
15	13, 14	anim12i 622	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑋 ∈ 𝑉 ∧ 𝑥 ∈ (Vtx‘𝐻)))
16		eqid 2761	. . . . . . . . . . . . 13 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
17		eqid 2761	. . . . . . . . . . . . 13 ⊢ (Edg‘𝐻) = (Edg‘𝐻)
18	2, 16, 17	clnbgrgrimlem 48515	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑥 ∈ (Vtx‘𝐻))) → ((𝑒 ∈ (Edg‘𝐻) ∧ {(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
19	11, 12, 15, 18	syl3anc 1389	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ((𝑒 ∈ (Edg‘𝐻) ∧ {(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
20	19	expd 419	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑒 ∈ (Edg‘𝐻) → ({(𝐹‘𝑋), 𝑥} ⊆ 𝑒 → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥)))
21	20	rexlimdv 3160	. . . . . . . . 9 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒 → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
22	10, 21	jaod 870	. . . . . . . 8 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
23	22	expimpd 457	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
24		eqid 2761	. . . . . . . . 9 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
25		eqid 2761	. . . . . . . . 9 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
26	2, 16, 24, 25	grimprop 48465	. . . . . . . 8 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
27		f1of 6800	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉⟶(Vtx‘𝐻))
28	27	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → 𝐹:𝑉⟶(Vtx‘𝐻))
29	28	3ad2ant1 1145	. . . . . . . . . . . . . 14 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝐹:𝑉⟶(Vtx‘𝐻))
30	29	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → 𝐹:𝑉⟶(Vtx‘𝐻))
31	2	clnbgrisvtx 48412	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐺 ClNeighbVtx 𝑋) → 𝑛 ∈ 𝑉)
32	31	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) → 𝑛 ∈ 𝑉)
33	32	adantr 484	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → 𝑛 ∈ 𝑉)
34	30, 33	ffvelcdmd 7060	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → (𝐹‘𝑛) ∈ (Vtx‘𝐻))
35		eleq1 2849	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑛) → (𝑥 ∈ (Vtx‘𝐻) ↔ (𝐹‘𝑛) ∈ (Vtx‘𝐻)))
36	35	eqcoms 2769	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑛) = 𝑥 → (𝑥 ∈ (Vtx‘𝐻) ↔ (𝐹‘𝑛) ∈ (Vtx‘𝐻)))
37	36	adantl 485	. . . . . . . . . . . 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 259	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → 𝑥 ∈ (Vtx‘𝐻))
39		simp3 1150	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
40	29, 39	ffvelcdmd 7060	. . . . . . . . . . . 12 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) ∈ (Vtx‘𝐻))
41	40	ad2antrr 736	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → (𝐹‘𝑋) ∈ (Vtx‘𝐻))
42		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
43	2, 42	clnbgrel 48410	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝑛 = 𝑋 ∨ ∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘)))
44		fveq2 6861	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑋 → (𝐹‘𝑛) = (𝐹‘𝑋))
45	44	orcd 884	. . . . . . . . . . . . . . . . . 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 29283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐺 ∈ UHGraph → (𝑘 ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗)))
48	47	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑘 ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗)))
49	48	3ad2ant2 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗))
51		2fveq3 6866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐻)‘(𝑔‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑗)))
52		fveq2 6861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑗))
53	52	imaeq2d 6044	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = 𝑗 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
54	51, 53	eqeq12d 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑖 = 𝑗 → (((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))))
55	54	rspcv 3576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))))
56	55	3ad2ant3 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 ↔ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗)))
58	57	3ad2ant3 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)) ∧ 𝑘 = ((iEdg‘𝐺)‘𝑗)) → ({𝑋, 𝑛} ⊆ 𝑘 ↔ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗)))
59		sseq2 3960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑒 = ((iEdg‘𝐻)‘(𝑔‘𝑗)) → ({(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒 ↔ {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ ((iEdg‘𝐻)‘(𝑔‘𝑗))))
60	25	uhgrfun 29223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝐻 ∈ UHGraph → Fun (iEdg‘𝐻))
61	60	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → Fun (iEdg‘𝐻))
62	61	3ad2ant3 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → Fun (iEdg‘𝐻))
63		f1of 6800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑔:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
64	63	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝑔:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
65	64	3ad2ant1 1145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝑔:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
66	65	ffvelcdmda 7059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → (𝑔‘𝑗) ∈ dom (iEdg‘𝐻))
67	25	iedgedg 29207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑔‘𝑗) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
68	62, 66, 67	syl2an2r 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
69	68	3adant2 1143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
70	69	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
71	70	3ad2ant1 1145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
72		f1ofn 6801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹 Fn 𝑉)
73	72	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝐹 Fn 𝑉)
74	73	3ad2ant1 1145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝐹 Fn 𝑉)
75	74	3ad2ant1 1145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → 𝐹 Fn 𝑉)
76	75	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) → 𝐹 Fn 𝑉)
77		pm3.22 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉))
78	76, 77	anim12i 622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)))
79	78	3adant2 1143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)))
80		3anass 1105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ↔ (𝐹 Fn 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)))
81	79, 80	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉))
82		fnimapr 6944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6086	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ({𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) → (𝐹 “ {𝑋, 𝑛}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
85	84	3ad2ant2 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
87		simp1r 1211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)
90	89	3exp 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) → ({𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
91	90	3adant3 1144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)) ∧ 𝑘 = ((iEdg‘𝐺)‘𝑗)) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
93	92	3exp 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1122	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 421	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3162	. . . . . . . . . . . . . . . . . . . . . . . . . 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 416	. . . . . . . . . . . . . . . . . . . . . . . 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 410	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ({𝑋, 𝑛} ⊆ 𝑘 → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
109	108	3imp 1122	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) ∧ {𝑋, 𝑛} ⊆ 𝑘 ∧ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉)) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)
110	109	olcd 885	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) ∧ {𝑋, 𝑛} ⊆ 𝑘 ∧ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉)) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
111	110	3exp 1131	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ({𝑋, 𝑛} ⊆ 𝑘 → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
112	111	rexlimdva 3162	. . . . . . . . . . . . . . . . . 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 868	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 = 𝑋 ∨ ∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘) → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
115	114	impcom 411	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝑛 = 𝑋 ∨ ∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘)) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
116	43, 115	sylbi 219	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (𝐺 ClNeighbVtx 𝑋) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
117	116	impcom 411	. . . . . . . . . . . . 13 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
118	117	adantr 484	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
119		eqeq1 2765	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑛) → (𝑥 = (𝐹‘𝑋) ↔ (𝐹‘𝑛) = (𝐹‘𝑋)))
120		preq2 4690	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐹‘𝑛) → {(𝐹‘𝑋), 𝑥} = {(𝐹‘𝑋), (𝐹‘𝑛)})
121	120	sseq1d 3965	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐹‘𝑛) → ({(𝐹‘𝑋), 𝑥} ⊆ 𝑒 ↔ {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
122	121	rexbidv 3185	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑛) → (∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒 ↔ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
123	119, 122	orbi12d 929	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑛) → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) ↔ ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
124	123	eqcoms 2769	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑛) = 𝑥 → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) ↔ ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
125	124	adantl 485	. . . . . . . . . . . 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 259	. . . . . . . . . . 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 522	. . . . . . . . . 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 416	. . . . . . . . 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 3162	. . . . . . . 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 1175	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥 → ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒))))
131	23, 130	impbid 214	. . . . . 6 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
132	131	3exp 1131	. . . . 5 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑋 ∈ 𝑉 → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))))
133	132	impcom 411	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝑋 ∈ 𝑉 → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥)))
134	133	imp 410	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
135	16, 17	clnbgrel 48410	. . . 4 ⊢ (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)))
136	135	a1i 11	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒))))
137	2, 16	grimf1o 48466	. . . . . 6 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→(Vtx‘𝐻))
138	137, 72	syl 17	. . . . 5 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹 Fn 𝑉)
139	138	adantl 485	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → 𝐹 Fn 𝑉)
140	2	clnbgrssvtx 48413	. . . . 5 ⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉
141	140	a1i 11	. . . 4 ⊢ (𝑋 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉)
142		fvelimab 6933	. . . 4 ⊢ ((𝐹 Fn 𝑉 ∧ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉) → (𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
143	139, 141, 142	syl2an 605	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
144	134, 136, 143	3bitr4d 313	. 2 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ 𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋))))
145	144	eqrdv 2759	1 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝐻 ClNeighbVtx (𝐹‘𝑋)) = (𝐹 “ (𝐺 ClNeighbVtx 𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 ∧ w3a 1097 = wceq 1559 ∃wex 1798 ∈ wcel 2141 ∀wral 3075 ∃wrex 3085 ⊆ wss 3902 {cpr 4581 dom cdm 5643 “ cima 5646 Fun wfun 6509 Fn wfn 6510 ⟶wf 6511 –1-1-onto→wf1o 6514 ‘cfv 6515 (class class class)co 7390 Vtxcvtx 29153 iEdgciedg 29154 Edgcedg 29204 UHGraphcuhgr 29213 ClNeighbVtx cclnbgr 48400 GraphIso cgrim 48457

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7712

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3076 df-rex 3086 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-id 5538 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-ov 7393 df-oprab 7394 df-mpo 7395 df-1st 7964 df-2nd 7965 df-map 8803 df-edg 29205 df-uhgr 29215 df-clnbgr 48401 df-grim 48460

This theorem is referenced by: uhgrimgrlim 48569

W3C validator