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 47786

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 6929	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑋 → ((𝐹‘𝑛) = (𝐹‘𝑋) ↔ (𝐹‘𝑋) = (𝐹‘𝑋)))
2		clnbgrgrim.v	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (Vtx‘𝐺)
3	2	clnbgrvtxel 47702	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
4	3	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
5		eqidd 2741	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) = (𝐹‘𝑋))
6	1, 4, 5	rspcedvdw 3638	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋))
7	6	adantr 480	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋))
8		eqeq2 2752	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐹‘𝑋) → ((𝐹‘𝑛) = 𝑥 ↔ (𝐹‘𝑛) = (𝐹‘𝑋)))
9	8	rexbidv 3185	. . . . . . . . . 10 ⊢ (𝑥 = (𝐹‘𝑋) → (∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥 ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋)))
10	7, 9	syl5ibrcom 247	. . . . . . . . 9 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑥 = (𝐹‘𝑋) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
11		simpl2 1192	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph))
12		simpl1 1191	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → 𝐹 ∈ (𝐺 GraphIso 𝐻))
13		simp3 1138	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
14		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) → 𝑥 ∈ (Vtx‘𝐻))
15	13, 14	anim12i 612	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑋 ∈ 𝑉 ∧ 𝑥 ∈ (Vtx‘𝐻)))
16		eqid 2740	. . . . . . . . . . . . 13 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
17		eqid 2740	. . . . . . . . . . . . 13 ⊢ (Edg‘𝐻) = (Edg‘𝐻)
18	2, 16, 17	clnbgrgrimlem 47785	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑥 ∈ (Vtx‘𝐻))) → ((𝑒 ∈ (Edg‘𝐻) ∧ {(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
19	11, 12, 15, 18	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ((𝑒 ∈ (Edg‘𝐻) ∧ {(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
20	19	expd 415	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑒 ∈ (Edg‘𝐻) → ({(𝐹‘𝑋), 𝑥} ⊆ 𝑒 → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥)))
21	20	rexlimdv 3159	. . . . . . . . 9 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒 → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
22	10, 21	jaod 858	. . . . . . . 8 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
23	22	expimpd 453	. . . . . . 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 47753	. . . . . . . 8 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
27		f1of 6862	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉⟶(Vtx‘𝐻))
28	27	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → 𝐹:𝑉⟶(Vtx‘𝐻))
29	28	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝐹:𝑉⟶(Vtx‘𝐻))
30	29	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → 𝐹:𝑉⟶(Vtx‘𝐻))
31	2	clnbgrisvtx 47703	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐺 ClNeighbVtx 𝑋) → 𝑛 ∈ 𝑉)
32	31	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) → 𝑛 ∈ 𝑉)
33	32	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → 𝑛 ∈ 𝑉)
34	30, 33	ffvelcdmd 7119	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → (𝐹‘𝑛) ∈ (Vtx‘𝐻))
35		eleq1 2832	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑛) → (𝑥 ∈ (Vtx‘𝐻) ↔ (𝐹‘𝑛) ∈ (Vtx‘𝐻)))
36	35	eqcoms 2748	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑛) = 𝑥 → (𝑥 ∈ (Vtx‘𝐻) ↔ (𝐹‘𝑛) ∈ (Vtx‘𝐻)))
37	36	adantl 481	. . . . . . . . . . . 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 257	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → 𝑥 ∈ (Vtx‘𝐻))
39		simp3 1138	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
40	29, 39	ffvelcdmd 7119	. . . . . . . . . . . 12 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) ∈ (Vtx‘𝐻))
41	40	ad2antrr 725	. . . . . . . . . . 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 47701	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝑛 = 𝑋 ∨ ∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘)))
44		fveq2 6920	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑋 → (𝐹‘𝑛) = (𝐹‘𝑋))
45	44	orcd 872	. . . . . . . . . . . . . . . . . 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 29161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐺 ∈ UHGraph → (𝑘 ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗)))
48	47	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑘 ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗)))
49	48	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 476	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗))
51		2fveq3 6925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐻)‘(𝑔‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑗)))
52		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑗))
53	52	imaeq2d 6089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = 𝑗 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
54	51, 53	eqeq12d 2756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑖 = 𝑗 → (((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))))
55	54	rspcv 3631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))))
56	55	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 ↔ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗)))
58	57	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)) ∧ 𝑘 = ((iEdg‘𝐺)‘𝑗)) → ({𝑋, 𝑛} ⊆ 𝑘 ↔ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗)))
59		sseq2 4035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑒 = ((iEdg‘𝐻)‘(𝑔‘𝑗)) → ({(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒 ↔ {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ ((iEdg‘𝐻)‘(𝑔‘𝑗))))
60	25	uhgrfun 29101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝐻 ∈ UHGraph → Fun (iEdg‘𝐻))
61	60	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → Fun (iEdg‘𝐻))
62	61	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → Fun (iEdg‘𝐻))
63		f1of 6862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑔:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
64	63	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝑔:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
65	64	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝑔:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
66	65	ffvelcdmda 7118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → (𝑔‘𝑗) ∈ dom (iEdg‘𝐻))
67	25	iedgedg 29085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑔‘𝑗) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
68	62, 66, 67	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
69	68	3adant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
70	69	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
71	70	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
72		f1ofn 6863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹 Fn 𝑉)
73	72	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝐹 Fn 𝑉)
74	73	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝐹 Fn 𝑉)
75	74	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → 𝐹 Fn 𝑉)
76	75	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) → 𝐹 Fn 𝑉)
77		pm3.22 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉))
78	76, 77	anim12i 612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)))
79	78	3adant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)))
80		3anass 1095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ↔ (𝐹 Fn 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)))
81	79, 80	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉))
82		fnimapr 7005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ({𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) → (𝐹 “ {𝑋, 𝑛}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
85	84	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
87		simp1r 1198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)
90	89	3exp 1119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) → ({𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
91	90	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)) ∧ 𝑘 = ((iEdg‘𝐺)‘𝑗)) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
93	92	3exp 1119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 417	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3161	. . . . . . . . . . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . . . . . . . . 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 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ({𝑋, 𝑛} ⊆ 𝑘 → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
109	108	3imp 1111	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) ∧ {𝑋, 𝑛} ⊆ 𝑘 ∧ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉)) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)
110	109	olcd 873	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) ∧ {𝑋, 𝑛} ⊆ 𝑘 ∧ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉)) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
111	110	3exp 1119	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ({𝑋, 𝑛} ⊆ 𝑘 → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
112	111	rexlimdva 3161	. . . . . . . . . . . . . . . . . 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 856	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 = 𝑋 ∨ ∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘) → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
115	114	impcom 407	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝑛 = 𝑋 ∨ ∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘)) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
116	43, 115	sylbi 217	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (𝐺 ClNeighbVtx 𝑋) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
117	116	impcom 407	. . . . . . . . . . . . 13 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
118	117	adantr 480	. . . . . . . . . . . 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 4759	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐹‘𝑛) → {(𝐹‘𝑋), 𝑥} = {(𝐹‘𝑋), (𝐹‘𝑛)})
121	120	sseq1d 4040	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐹‘𝑛) → ({(𝐹‘𝑋), 𝑥} ⊆ 𝑒 ↔ {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
122	121	rexbidv 3185	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑛) → (∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒 ↔ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
123	119, 122	orbi12d 917	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑛) → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) ↔ ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
124	123	eqcoms 2748	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑛) = 𝑥 → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) ↔ ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
125	124	adantl 481	. . . . . . . . . . . 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 257	. . . . . . . . . . 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 514	. . . . . . . . . 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 412	. . . . . . . . 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 3161	. . . . . . . 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 1163	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥 → ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒))))
131	23, 130	impbid 212	. . . . . 6 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
132	131	3exp 1119	. . . . 5 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑋 ∈ 𝑉 → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))))
133	132	impcom 407	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝑋 ∈ 𝑉 → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥)))
134	133	imp 406	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
135	16, 17	clnbgrel 47701	. . . 4 ⊢ (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)))
136	135	a1i 11	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒))))
137	2, 16	grimf1o 47754	. . . . . 6 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→(Vtx‘𝐻))
138	137, 72	syl 17	. . . . 5 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹 Fn 𝑉)
139	138	adantl 481	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → 𝐹 Fn 𝑉)
140	2	clnbgrssvtx 47704	. . . . 5 ⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉
141	140	a1i 11	. . . 4 ⊢ (𝑋 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉)
142		fvelimab 6994	. . . 4 ⊢ ((𝐹 Fn 𝑉 ∧ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉) → (𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
143	139, 141, 142	syl2an 595	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
144	134, 136, 143	3bitr4d 311	. 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 206 ∧ wa 395 ∨ wo 846 ∧ w3a 1087 = wceq 1537 ∃wex 1777 ∈ wcel 2108 ∀wral 3067 ∃wrex 3076 ⊆ wss 3976 {cpr 4650 dom cdm 5700 “ cima 5703 Fun wfun 6567 Fn wfn 6568 ⟶wf 6569 –1-1-onto→wf1o 6572 ‘cfv 6573 (class class class)co 7448 Vtxcvtx 29031 iEdgciedg 29032 Edgcedg 29082 UHGraphcuhgr 29091 ClNeighbVtx cclnbgr 47692 GraphIso cgrim 47745

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-ov 7451 df-oprab 7452 df-mpo 7453 df-1st 8030 df-2nd 8031 df-map 8886 df-edg 29083 df-uhgr 29093 df-clnbgr 47693 df-grim 47748

This theorem is referenced by: uhgrimgrlim 47811

W3C validator