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 48740

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 6897	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑋 → ((𝐹‘𝑛) = (𝐹‘𝑋) ↔ (𝐹‘𝑋) = (𝐹‘𝑋)))
2		clnbgrgrim.v	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (Vtx‘𝐺)
3	2	clnbgrvtxel 48635	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
4	3	3ad2ant3 1153	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
5		eqidd 2767	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) = (𝐹‘𝑋))
6	1, 4, 5	rspcedvdw 3587	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋))
7	6	adantr 486	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋))
8		eqeq2 2778	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐹‘𝑋) → ((𝐹‘𝑛) = 𝑥 ↔ (𝐹‘𝑛) = (𝐹‘𝑋)))
9	8	rexbidv 3192	. . . . . . . . . 10 ⊢ (𝑥 = (𝐹‘𝑋) → (∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥 ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋)))
10	7, 9	syl5ibrcom 250	. . . . . . . . 9 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑥 = (𝐹‘𝑋) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
11		simpl2 1211	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph))
12		simpl1 1210	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → 𝐹 ∈ (𝐺 GraphIso 𝐻))
13		simp3 1156	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
14		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) → 𝑥 ∈ (Vtx‘𝐻))
15	13, 14	anim12i 625	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑋 ∈ 𝑉 ∧ 𝑥 ∈ (Vtx‘𝐻)))
16		eqid 2766	. . . . . . . . . . . . 13 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
17		eqid 2766	. . . . . . . . . . . . 13 ⊢ (Edg‘𝐻) = (Edg‘𝐻)
18	2, 16, 17	clnbgrgrimlem 48739	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑥 ∈ (Vtx‘𝐻))) → ((𝑒 ∈ (Edg‘𝐻) ∧ {(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
19	11, 12, 15, 18	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ((𝑒 ∈ (Edg‘𝐻) ∧ {(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
20	19	expd 421	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑒 ∈ (Edg‘𝐻) → ({(𝐹‘𝑋), 𝑥} ⊆ 𝑒 → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥)))
21	20	rexlimdv 3167	. . . . . . . . 9 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒 → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
22	10, 21	jaod 873	. . . . . . . 8 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
23	22	expimpd 459	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
24		eqid 2766	. . . . . . . . 9 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
25		eqid 2766	. . . . . . . . 9 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
26	2, 16, 24, 25	grimprop 48689	. . . . . . . 8 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
27		f1of 6827	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉⟶(Vtx‘𝐻))
28	27	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → 𝐹:𝑉⟶(Vtx‘𝐻))
29	28	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝐹:𝑉⟶(Vtx‘𝐻))
30	29	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → 𝐹:𝑉⟶(Vtx‘𝐻))
31	2	clnbgrisvtx 48636	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐺 ClNeighbVtx 𝑋) → 𝑛 ∈ 𝑉)
32	31	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) → 𝑛 ∈ 𝑉)
33	32	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → 𝑛 ∈ 𝑉)
34	30, 33	ffvelcdmd 7087	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → (𝐹‘𝑛) ∈ (Vtx‘𝐻))
35		eleq1 2854	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑛) → (𝑥 ∈ (Vtx‘𝐻) ↔ (𝐹‘𝑛) ∈ (Vtx‘𝐻)))
36	35	eqcoms 2774	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑛) = 𝑥 → (𝑥 ∈ (Vtx‘𝐻) ↔ (𝐹‘𝑛) ∈ (Vtx‘𝐻)))
37	36	adantl 487	. . . . . . . . . . . 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 260	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → 𝑥 ∈ (Vtx‘𝐻))
39		simp3 1156	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
40	29, 39	ffvelcdmd 7087	. . . . . . . . . . . 12 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) ∈ (Vtx‘𝐻))
41	40	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → (𝐹‘𝑋) ∈ (Vtx‘𝐻))
42		eqid 2766	. . . . . . . . . . . . . . . 16 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
43	2, 42	clnbgrel 48634	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝑛 = 𝑋 ∨ ∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘)))
44		fveq2 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑋 → (𝐹‘𝑛) = (𝐹‘𝑋))
45	44	orcd 887	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑋 → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
46	45	2a1d 27	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑋 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
47	24	uhgredgiedgb 29513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐺 ∈ UHGraph → (𝑘 ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗)))
48	47	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑘 ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗)))
49	48	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗))
51		2fveq3 6893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐻)‘(𝑔‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑗)))
52		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑗))
53	52	imaeq2d 6067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = 𝑗 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
54	51, 53	eqeq12d 2782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑖 = 𝑗 → (((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))))
55	54	rspcv 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))))
56	55	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 ↔ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗)))
58	57	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)) ∧ 𝑘 = ((iEdg‘𝐺)‘𝑗)) → ({𝑋, 𝑛} ⊆ 𝑘 ↔ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗)))
59		sseq2 3966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑒 = ((iEdg‘𝐻)‘(𝑔‘𝑗)) → ({(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒 ↔ {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ ((iEdg‘𝐻)‘(𝑔‘𝑗))))
60	25	uhgrfun 29453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝐻 ∈ UHGraph → Fun (iEdg‘𝐻))
61	60	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → Fun (iEdg‘𝐻))
62	61	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → Fun (iEdg‘𝐻))
63		f1of 6827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑔:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
64	63	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝑔:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
65	64	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝑔:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
66	65	ffvelcdmda 7086	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → (𝑔‘𝑗) ∈ dom (iEdg‘𝐻))
67	25	iedgedg 29437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑔‘𝑗) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
68	62, 66, 67	syl2an2r 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
69	68	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
70	69	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
71	70	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
72		f1ofn 6828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹 Fn 𝑉)
73	72	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝐹 Fn 𝑉)
74	73	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝐹 Fn 𝑉)
75	74	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → 𝐹 Fn 𝑉)
76	75	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) → 𝐹 Fn 𝑉)
77		pm3.22 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉))
78	76, 77	anim12i 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)))
79	78	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)))
80		3anass 1111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ↔ (𝐹 Fn 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)))
81	79, 80	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉))
82		fnimapr 6971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → (𝐹 “ {𝑋, 𝑛}) = {(𝐹‘𝑋), (𝐹‘𝑛)})
83	81, 82	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 “ {𝑋, 𝑛}) = {(𝐹‘𝑋), (𝐹‘𝑛)})
84		imass2 6109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ({𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) → (𝐹 “ {𝑋, 𝑛}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
85	84	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
87		simp1r 1217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)
90	89	3exp 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) → ({𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
91	90	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)) ∧ 𝑘 = ((iEdg‘𝐺)‘𝑗)) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
93	92	3exp 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 48	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 92	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 423	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3169	. . . . . . . . . . . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
106	105	ex 418	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝑘 ∈ (Edg‘𝐺) → ({𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
107	106	com14 97	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑘 ∈ (Edg‘𝐺) → ({𝑋, 𝑛} ⊆ 𝑘 → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
108	107	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ({𝑋, 𝑛} ⊆ 𝑘 → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
109	108	3imp 1128	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) ∧ {𝑋, 𝑛} ⊆ 𝑘 ∧ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉)) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)
110	109	olcd 888	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) ∧ {𝑋, 𝑛} ⊆ 𝑘 ∧ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉)) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
111	110	3exp 1137	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ({𝑋, 𝑛} ⊆ 𝑘 → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
112	111	rexlimdva 3169	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘 → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
113	112	com12 33	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
114	46, 113	jaoi 871	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 = 𝑋 ∨ ∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘) → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
115	114	impcom 413	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝑛 = 𝑋 ∨ ∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘)) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
116	43, 115	sylbi 220	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (𝐺 ClNeighbVtx 𝑋) → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
117	116	impcom 413	. . . . . . . . . . . . 13 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
118	117	adantr 486	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
119		eqeq1 2770	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑛) → (𝑥 = (𝐹‘𝑋) ↔ (𝐹‘𝑛) = (𝐹‘𝑋)))
120		preq2 4705	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐹‘𝑛) → {(𝐹‘𝑋), 𝑥} = {(𝐹‘𝑋), (𝐹‘𝑛)})
121	120	sseq1d 3971	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐹‘𝑛) → ({(𝐹‘𝑋), 𝑥} ⊆ 𝑒 ↔ {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
122	121	rexbidv 3192	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑛) → (∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒 ↔ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
123	119, 122	orbi12d 932	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑛) → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) ↔ ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
124	123	eqcoms 2774	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑛) = 𝑥 → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) ↔ ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
125	124	adantl 487	. . . . . . . . . . . 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 260	. . . . . . . . . . 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 524	. . . . . . . . . 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 418	. . . . . . . . 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 3169	. . . . . . . 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 1181	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥 → ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒))))
131	23, 130	impbid 215	. . . . . 6 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
132	131	3exp 1137	. . . . 5 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑋 ∈ 𝑉 → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))))
133	132	impcom 413	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝑋 ∈ 𝑉 → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥)))
134	133	imp 412	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
135	16, 17	clnbgrel 48634	. . . 4 ⊢ (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)))
136	135	a1i 11	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒))))
137	2, 16	grimf1o 48690	. . . . . 6 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→(Vtx‘𝐻))
138	137, 72	syl 18	. . . . 5 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹 Fn 𝑉)
139	138	adantl 487	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → 𝐹 Fn 𝑉)
140	2	clnbgrssvtx 48637	. . . . 5 ⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉
141	140	a1i 11	. . . 4 ⊢ (𝑋 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉)
142		fvelimab 6960	. . . 4 ⊢ ((𝐹 Fn 𝑉 ∧ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉) → (𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
143	139, 141, 142	syl2an 608	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
144	134, 136, 143	3bitr4d 314	. 2 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ 𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋))))
145	144	eqrdv 2764	1 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝐻 ClNeighbVtx (𝐹‘𝑋)) = (𝐹 “ (𝐺 ClNeighbVtx 𝑋)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2146 ∀wral 3082 ∃wrex 3092 ⊆ wss 3908 {cpr 4596 dom cdm 5666 “ cima 5669 Fun wfun 6537 Fn wfn 6538 ⟶wf 6539 –1-1-onto→wf1o 6542 ‘cfv 6543 (class class class)co 7423 Vtxcvtx 29383 iEdgciedg 29384 Edgcedg 29434 UHGraphcuhgr 29443 ClNeighbVtx cclnbgr 48624 GraphIso cgrim 48681

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-ral 3083 df-rex 3093 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-id 5561 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-ov 7426 df-oprab 7427 df-mpo 7428 df-1st 7995 df-2nd 7996 df-map 8835 df-edg 29435 df-uhgr 29445 df-clnbgr 48625 df-grim 48684

This theorem is used by: uhgrimgrlim 48793

W3C validator