Theorem setsexstruct2

Description: An extensible structure with a replaced slot is an extensible structure. (Contributed by AV, 14-Nov-2021)

	Ref	Expression
Assertion	setsexstruct2	$$⊢\left(G\mathrm{Struct}X\wedge E\in V\wedge I\in \mathbb{N}\right)\to \exists y\left(G\mathrm{sSet}⟨I,E⟩\right)\mathrm{Struct}y$$

Proof

Step	Hyp	Ref	Expression
1		opex	$$⊢⟨if\left(I\le 1^{st}\left(X\right),I,1^{st}\left(X\right)\right),if\left(I\le 2^{nd}\left(X\right),2^{nd}\left(X\right),I\right)⟩\in \mathrm{V}$$
2	1	a1i	$$⊢\left(G\mathrm{Struct}X\wedge E\in V\wedge I\in \mathbb{N}\right)\to ⟨if\left(I\le 1^{st}\left(X\right),I,1^{st}\left(X\right)\right),if\left(I\le 2^{nd}\left(X\right),2^{nd}\left(X\right),I\right)⟩\in \mathrm{V}$$
3		eqidd	$$⊢\left(G\mathrm{Struct}X\wedge E\in V\wedge I\in \mathbb{N}\right)\to ⟨if\left(I\le 1^{st}\left(X\right),I,1^{st}\left(X\right)\right),if\left(I\le 2^{nd}\left(X\right),2^{nd}\left(X\right),I\right)⟩=⟨if\left(I\le 1^{st}\left(X\right),I,1^{st}\left(X\right)\right),if\left(I\le 2^{nd}\left(X\right),2^{nd}\left(X\right),I\right)⟩$$
4		setsstruct2	$$⊢\left(\left(G\mathrm{Struct}X\wedge E\in V\wedge I\in \mathbb{N}\right)\wedge ⟨if\left(I\le 1^{st}\left(X\right),I,1^{st}\left(X\right)\right),if\left(I\le 2^{nd}\left(X\right),2^{nd}\left(X\right),I\right)⟩=⟨if\left(I\le 1^{st}\left(X\right),I,1^{st}\left(X\right)\right),if\left(I\le 2^{nd}\left(X\right),2^{nd}\left(X\right),I\right)⟩\right)\to \left(G\mathrm{sSet}⟨I,E⟩\right)\mathrm{Struct}⟨if\left(I\le 1^{st}\left(X\right),I,1^{st}\left(X\right)\right),if\left(I\le 2^{nd}\left(X\right),2^{nd}\left(X\right),I\right)⟩$$
5	3 4	mpdan	$$⊢\left(G\mathrm{Struct}X\wedge E\in V\wedge I\in \mathbb{N}\right)\to \left(G\mathrm{sSet}⟨I,E⟩\right)\mathrm{Struct}⟨if\left(I\le 1^{st}\left(X\right),I,1^{st}\left(X\right)\right),if\left(I\le 2^{nd}\left(X\right),2^{nd}\left(X\right),I\right)⟩$$
6		breq2	$$⊢y=⟨if\left(I\le 1^{st}\left(X\right),I,1^{st}\left(X\right)\right),if\left(I\le 2^{nd}\left(X\right),2^{nd}\left(X\right),I\right)⟩\to \left(\left(G\mathrm{sSet}⟨I,E⟩\right)\mathrm{Struct}y\leftrightarrow \left(G\mathrm{sSet}⟨I,E⟩\right)\mathrm{Struct}⟨if\left(I\le 1^{st}\left(X\right),I,1^{st}\left(X\right)\right),if\left(I\le 2^{nd}\left(X\right),2^{nd}\left(X\right),I\right)⟩\right)$$
7	2 5 6	spcedv	$$⊢\left(G\mathrm{Struct}X\wedge E\in V\wedge I\in \mathbb{N}\right)\to \exists y\left(G\mathrm{sSet}⟨I,E⟩\right)\mathrm{Struct}y$$