Theorem strle1

Description: Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015)

	Ref	Expression
Hypotheses	strle1.i	$$⊢I\in \mathbb{N}$$
	strle1.a	$$⊢A=I$$
Assertion	strle1	$$⊢\left\{⟨A,X⟩\right\}\mathrm{Struct}⟨I,I⟩$$

Proof

Step	Hyp	Ref	Expression
1		strle1.i	$$⊢I\in \mathbb{N}$$
2		strle1.a	$$⊢A=I$$
3	1	nnrei	$$⊢I\in ℝ$$
4	3	leidi	$$⊢I\le I$$
5	1 1 4	3pm3.2i	$$⊢\left(I\in \mathbb{N}\wedge I\in \mathbb{N}\wedge I\le I\right)$$
6		difss	$$⊢\left\{⟨A,X⟩\right\}\setminus \left\{\varnothing \right\}\subseteq \left\{⟨A,X⟩\right\}$$
7	2 1	eqeltri	$$⊢A\in \mathbb{N}$$
8		funsng	$$⊢\left(A\in \mathbb{N}\wedge X\in \mathrm{V}\right)\to \mathrm{Fun}\left\{⟨A,X⟩\right\}$$
9	7 8	mpan	$$⊢X\in \mathrm{V}\to \mathrm{Fun}\left\{⟨A,X⟩\right\}$$
10		funss	$$⊢\left\{⟨A,X⟩\right\}\setminus \left\{\varnothing \right\}\subseteq \left\{⟨A,X⟩\right\}\to \left(\mathrm{Fun}\left\{⟨A,X⟩\right\}\to \mathrm{Fun}\left(\left\{⟨A,X⟩\right\}\setminus \left\{\varnothing \right\}\right)\right)$$
11	6 9 10	mpsyl	$$⊢X\in \mathrm{V}\to \mathrm{Fun}\left(\left\{⟨A,X⟩\right\}\setminus \left\{\varnothing \right\}\right)$$
12		fun0	$$⊢\mathrm{Fun}\varnothing$$
13		opprc2	$$⊢\neg X\in \mathrm{V}\to ⟨A,X⟩=\varnothing$$
14	13	sneqd	$$⊢\neg X\in \mathrm{V}\to \left\{⟨A,X⟩\right\}=\left\{\varnothing \right\}$$
15	14	difeq1d	$$⊢\neg X\in \mathrm{V}\to \left\{⟨A,X⟩\right\}\setminus \left\{\varnothing \right\}=\left\{\varnothing \right\}\setminus \left\{\varnothing \right\}$$
16		difid	$$⊢\left\{\varnothing \right\}\setminus \left\{\varnothing \right\}=\varnothing$$
17	15 16	eqtrdi	$$⊢\neg X\in \mathrm{V}\to \left\{⟨A,X⟩\right\}\setminus \left\{\varnothing \right\}=\varnothing$$
18	17	funeqd	$$⊢\neg X\in \mathrm{V}\to \left(\mathrm{Fun}\left(\left\{⟨A,X⟩\right\}\setminus \left\{\varnothing \right\}\right)\leftrightarrow \mathrm{Fun}\varnothing \right)$$
19	12 18	mpbiri	$$⊢\neg X\in \mathrm{V}\to \mathrm{Fun}\left(\left\{⟨A,X⟩\right\}\setminus \left\{\varnothing \right\}\right)$$
20	11 19	pm2.61i	$$⊢\mathrm{Fun}\left(\left\{⟨A,X⟩\right\}\setminus \left\{\varnothing \right\}\right)$$
21		dmsnopss	$$⊢\mathrm{dom}\left\{⟨A,X⟩\right\}\subseteq \left\{A\right\}$$
22	2	sneqi	$$⊢\left\{A\right\}=\left\{I\right\}$$
23	1	nnzi	$$⊢I\in \mathbb{Z}$$
24		fzsn	$$⊢I\in \mathbb{Z}\to \left(I\dots I\right)=\left\{I\right\}$$
25	23 24	ax-mp	$$⊢\left(I\dots I\right)=\left\{I\right\}$$
26	22 25	eqtr4i	$$⊢\left\{A\right\}=\left(I\dots I\right)$$
27	21 26	sseqtri	$$⊢\mathrm{dom}\left\{⟨A,X⟩\right\}\subseteq \left(I\dots I\right)$$
28		isstruct	$$⊢\left\{⟨A,X⟩\right\}\mathrm{Struct}⟨I,I⟩\leftrightarrow \left(\left(I\in \mathbb{N}\wedge I\in \mathbb{N}\wedge I\le I\right)\wedge \mathrm{Fun}\left(\left\{⟨A,X⟩\right\}\setminus \left\{\varnothing \right\}\right)\wedge \mathrm{dom}\left\{⟨A,X⟩\right\}\subseteq \left(I\dots I\right)\right)$$
29	5 20 27 28	mpbir3an	$$⊢\left\{⟨A,X⟩\right\}\mathrm{Struct}⟨I,I⟩$$