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 47902

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 6915	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑋 → ((𝐹‘𝑛) = (𝐹‘𝑋) ↔ (𝐹‘𝑋) = (𝐹‘𝑋)))
2		clnbgrgrim.v	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (Vtx‘𝐺)
3	2	clnbgrvtxel 47816	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
4	3	3ad2ant3 1136	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
5		eqidd 2738	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) = (𝐹‘𝑋))
6	1, 4, 5	rspcedvdw 3625	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋))
7	6	adantr 480	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋))
8		eqeq2 2749	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐹‘𝑋) → ((𝐹‘𝑛) = 𝑥 ↔ (𝐹‘𝑛) = (𝐹‘𝑋)))
9	8	rexbidv 3179	. . . . . . . . . 10 ⊢ (𝑥 = (𝐹‘𝑋) → (∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥 ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = (𝐹‘𝑋)))
10	7, 9	syl5ibrcom 247	. . . . . . . . 9 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑥 = (𝐹‘𝑋) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
11		simpl2 1193	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph))
12		simpl1 1192	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → 𝐹 ∈ (𝐺 GraphIso 𝐻))
13		simp3 1139	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
14		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) → 𝑥 ∈ (Vtx‘𝐻))
15	13, 14	anim12i 613	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑋 ∈ 𝑉 ∧ 𝑥 ∈ (Vtx‘𝐻)))
16		eqid 2737	. . . . . . . . . . . . 13 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
17		eqid 2737	. . . . . . . . . . . . 13 ⊢ (Edg‘𝐻) = (Edg‘𝐻)
18	2, 16, 17	clnbgrgrimlem 47901	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑥 ∈ (Vtx‘𝐻))) → ((𝑒 ∈ (Edg‘𝐻) ∧ {(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
19	11, 12, 15, 18	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ((𝑒 ∈ (Edg‘𝐻) ∧ {(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
20	19	expd 415	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (𝑒 ∈ (Edg‘𝐻) → ({(𝐹‘𝑋), 𝑥} ⊆ 𝑒 → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥)))
21	20	rexlimdv 3153	. . . . . . . . 9 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → (∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒 → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
22	10, 21	jaod 860	. . . . . . . 8 ⊢ (((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻))) → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
23	22	expimpd 453	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
24		eqid 2737	. . . . . . . . 9 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
25		eqid 2737	. . . . . . . . 9 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
26	2, 16, 24, 25	grimprop 47869	. . . . . . . 8 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
27		f1of 6848	. . . . . . . . . . . . . . . 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 1134	. . . . . . . . . . . . . 14 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝐹:𝑉⟶(Vtx‘𝐻))
30	29	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → 𝐹:𝑉⟶(Vtx‘𝐻))
31	2	clnbgrisvtx 47817	. . . . . . . . . . . . . . 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 7105	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → (𝐹‘𝑛) ∈ (Vtx‘𝐻))
35		eleq1 2829	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑛) → (𝑥 ∈ (Vtx‘𝐻) ↔ (𝐹‘𝑛) ∈ (Vtx‘𝐻)))
36	35	eqcoms 2745	. . . . . . . . . . . . 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 1139	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
40	29, 39	ffvelcdmd 7105	. . . . . . . . . . . 12 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) ∈ (Vtx‘𝐻))
41	40	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) ∧ 𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)) ∧ (𝐹‘𝑛) = 𝑥) → (𝐹‘𝑋) ∈ (Vtx‘𝐻))
42		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
43	2, 42	clnbgrel 47815	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝑛 = 𝑋 ∨ ∃𝑘 ∈ (Edg‘𝐺){𝑋, 𝑛} ⊆ 𝑘)))
44		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑋 → (𝐹‘𝑛) = (𝐹‘𝑋))
45	44	orcd 874	. . . . . . . . . . . . . . . . . 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 29143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐺 ∈ UHGraph → (𝑘 ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗)))
48	47	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝑘 ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)𝑘 = ((iEdg‘𝐺)‘𝑗)))
49	48	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 6911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐻)‘(𝑔‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑗)))
52		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑗))
53	52	imaeq2d 6078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑖 = 𝑗 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
54	51, 53	eqeq12d 2753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑖 = 𝑗 → (((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))))
55	54	rspcv 3618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))))
56	55	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4010	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑘 = ((iEdg‘𝐺)‘𝑗) → ({𝑋, 𝑛} ⊆ 𝑘 ↔ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗)))
58	57	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗)) ∧ 𝑘 = ((iEdg‘𝐺)‘𝑗)) → ({𝑋, 𝑛} ⊆ 𝑘 ↔ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗)))
59		sseq2 4010	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑒 = ((iEdg‘𝐻)‘(𝑔‘𝑗)) → ({(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒 ↔ {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ ((iEdg‘𝐻)‘(𝑔‘𝑗))))
60	25	uhgrfun 29083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝐻 ∈ UHGraph → Fun (iEdg‘𝐻))
61	60	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → Fun (iEdg‘𝐻))
62	61	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → Fun (iEdg‘𝐻))
63		f1of 6848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝑔:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
66	65	ffvelcdmda 7104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → (𝑔‘𝑗) ∈ dom (iEdg‘𝐻))
67	25	iedgedg 29067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((Fun (iEdg‘𝐻) ∧ (𝑔‘𝑗) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
68	62, 66, 67	syl2an2r 685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑗 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
69	68	3adant2 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((iEdg‘𝐻)‘(𝑔‘𝑗)) ∈ (Edg‘𝐻))
72		f1ofn 6849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝐹 Fn 𝑉)
75	74	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)))
79	78	3adant2 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ({𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) → (𝐹 “ {𝑋, 𝑛}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
85	84	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ (𝐹 “ ((iEdg‘𝐺)‘𝑗)))
87		simp1r 1199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) ∧ {𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)
90	89	3exp 1120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ (Edg‘𝐺) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑗)) = (𝐹 “ ((iEdg‘𝐺)‘𝑗))) → ({𝑋, 𝑛} ⊆ ((iEdg‘𝐺)‘𝑗) → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
91	90	3adant3 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3155	. . . . . . . . . . . . . . . . . . . . . . . . . 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 875	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) ∧ {𝑋, 𝑛} ⊆ 𝑘 ∧ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉)) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
111	110	3exp 1120	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ (Edg‘𝐺)) → ({𝑋, 𝑛} ⊆ 𝑘 → (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))))
112	111	rexlimdva 3155	. . . . . . . . . . . . . . . . . 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 858	. . . . . . . . . . . . . . . 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 2741	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑛) → (𝑥 = (𝐹‘𝑋) ↔ (𝐹‘𝑛) = (𝐹‘𝑋)))
120		preq2 4734	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐹‘𝑛) → {(𝐹‘𝑋), 𝑥} = {(𝐹‘𝑋), (𝐹‘𝑛)})
121	120	sseq1d 4015	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐹‘𝑛) → ({(𝐹‘𝑋), 𝑥} ⊆ 𝑒 ↔ {(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
122	121	rexbidv 3179	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑛) → (∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒 ↔ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒))
123	119, 122	orbi12d 919	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑛) → ((𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒) ↔ ((𝐹‘𝑛) = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), (𝐹‘𝑛)} ⊆ 𝑒)))
124	123	eqcoms 2745	. . . . . . . . . . . . 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 3155	. . . . . . . 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 1164	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥 → ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒))))
131	23, 130	impbid 212	. . . . . 6 ⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝑋 ∈ 𝑉) → (((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
132	131	3exp 1120	. . . . 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 47815	. . . 4 ⊢ (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒)))
136	135	a1i 11	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ ((𝑥 ∈ (Vtx‘𝐻) ∧ (𝐹‘𝑋) ∈ (Vtx‘𝐻)) ∧ (𝑥 = (𝐹‘𝑋) ∨ ∃𝑒 ∈ (Edg‘𝐻){(𝐹‘𝑋), 𝑥} ⊆ 𝑒))))
137	2, 16	grimf1o 47870	. . . . . 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 47818	. . . . 5 ⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉
141	140	a1i 11	. . . 4 ⊢ (𝑋 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉)
142		fvelimab 6981	. . . 4 ⊢ ((𝐹 Fn 𝑉 ∧ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉) → (𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
143	139, 141, 142	syl2an 596	. . 3 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋)) ↔ ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑥))
144	134, 136, 143	3bitr4d 311	. 2 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ (𝐻 ClNeighbVtx (𝐹‘𝑋)) ↔ 𝑥 ∈ (𝐹 “ (𝐺 ClNeighbVtx 𝑋))))
145	144	eqrdv 2735	1 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝐻 ClNeighbVtx (𝐹‘𝑋)) = (𝐹 “ (𝐺 ClNeighbVtx 𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1540 ∃wex 1779 ∈ wcel 2108 ∀wral 3061 ∃wrex 3070 ⊆ wss 3951 {cpr 4628 dom cdm 5685 “ cima 5688 Fun wfun 6555 Fn wfn 6556 ⟶wf 6557 –1-1-onto→wf1o 6560 ‘cfv 6561 (class class class)co 7431 Vtxcvtx 29013 iEdgciedg 29014 Edgcedg 29064 UHGraphcuhgr 29073 ClNeighbVtx cclnbgr 47805 GraphIso cgrim 47861

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-ov 7434 df-oprab 7435 df-mpo 7436 df-1st 8014 df-2nd 8015 df-map 8868 df-edg 29065 df-uhgr 29075 df-clnbgr 47806 df-grim 47864

This theorem is referenced by: uhgrimgrlim 47954

W3C validator