Theorem iedgval3sn

Description: Degenerated case 3 for edges: The set of indexed edges of a singleton containing a singleton containing a singleton is the innermost singleton. (Contributed by AV, 24-Sep-2020) (Avoid depending on this detail.)

	Ref	Expression
Hypothesis	vtxval3sn.a	$$⊢A\in \mathrm{V}$$
Assertion	iedgval3sn	$$⊢\mathrm{iEdg}\left(\left\{\left\{\left\{A\right\}\right\}\right\}\right)=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		vtxval3sn.a	$$⊢A\in \mathrm{V}$$
2	1	opid	$$⊢⟨A,A⟩=\left\{\left\{A\right\}\right\}$$
3	2	eqcomi	$$⊢\left\{\left\{A\right\}\right\}=⟨A,A⟩$$
4	3	sneqi	$$⊢\left\{\left\{\left\{A\right\}\right\}\right\}=\left\{⟨A,A⟩\right\}$$
5	1 4	iedgvalsnop	$$⊢\mathrm{iEdg}\left(\left\{\left\{\left\{A\right\}\right\}\right\}\right)=\left\{A\right\}$$