Theorem structcnvcnv

Description: Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015)

	Ref	Expression
Assertion	structcnvcnv	$$⊢F\mathrm{Struct}X\to {F^{-1}}^{-1}=F\setminus \left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		0nelxp	$$⊢\neg \varnothing \in \left(\mathrm{V}\times \mathrm{V}\right)$$
2		cnvcnv	$$⊢{F^{-1}}^{-1}=F\cap \left(\mathrm{V}\times \mathrm{V}\right)$$
3		inss2	$$⊢F\cap \left(\mathrm{V}\times \mathrm{V}\right)\subseteq \mathrm{V}\times \mathrm{V}$$
4	2 3	eqsstri	$$⊢{F^{-1}}^{-1}\subseteq \mathrm{V}\times \mathrm{V}$$
5	4	sseli	$$⊢\varnothing \in {F^{-1}}^{-1}\to \varnothing \in \left(\mathrm{V}\times \mathrm{V}\right)$$
6	1 5	mto	$$⊢\neg \varnothing \in {F^{-1}}^{-1}$$
7		disjsn	$$⊢{F^{-1}}^{-1}\cap \left\{\varnothing \right\}=\varnothing \leftrightarrow \neg \varnothing \in {F^{-1}}^{-1}$$
8	6 7	mpbir	$$⊢{F^{-1}}^{-1}\cap \left\{\varnothing \right\}=\varnothing$$
9		cnvcnvss	$$⊢{F^{-1}}^{-1}\subseteq F$$
10		reldisj	$$⊢{F^{-1}}^{-1}\subseteq F\to \left({F^{-1}}^{-1}\cap \left\{\varnothing \right\}=\varnothing \leftrightarrow {F^{-1}}^{-1}\subseteq F\setminus \left\{\varnothing \right\}\right)$$
11	9 10	ax-mp	$$⊢{F^{-1}}^{-1}\cap \left\{\varnothing \right\}=\varnothing \leftrightarrow {F^{-1}}^{-1}\subseteq F\setminus \left\{\varnothing \right\}$$
12	8 11	mpbi	$$⊢{F^{-1}}^{-1}\subseteq F\setminus \left\{\varnothing \right\}$$
13	12	a1i	$$⊢F\mathrm{Struct}X\to {F^{-1}}^{-1}\subseteq F\setminus \left\{\varnothing \right\}$$
14		structn0fun	$$⊢F\mathrm{Struct}X\to \mathrm{Fun}\left(F\setminus \left\{\varnothing \right\}\right)$$
15		funrel	$$⊢\mathrm{Fun}\left(F\setminus \left\{\varnothing \right\}\right)\to \mathrm{Rel}\left(F\setminus \left\{\varnothing \right\}\right)$$
16	14 15	syl	$$⊢F\mathrm{Struct}X\to \mathrm{Rel}\left(F\setminus \left\{\varnothing \right\}\right)$$
17		dfrel2	$$⊢\mathrm{Rel}\left(F\setminus \left\{\varnothing \right\}\right)\leftrightarrow {{\left(F\setminus \left\{\varnothing \right\}\right)}^{-1}}^{-1}=F\setminus \left\{\varnothing \right\}$$
18	16 17	sylib	$$⊢F\mathrm{Struct}X\to {{\left(F\setminus \left\{\varnothing \right\}\right)}^{-1}}^{-1}=F\setminus \left\{\varnothing \right\}$$
19		difss	$$⊢F\setminus \left\{\varnothing \right\}\subseteq F$$
20		cnvss	$$⊢F\setminus \left\{\varnothing \right\}\subseteq F\to {\left(F\setminus \left\{\varnothing \right\}\right)}^{-1}\subseteq F^{-1}$$
21		cnvss	$$⊢{\left(F\setminus \left\{\varnothing \right\}\right)}^{-1}\subseteq F^{-1}\to {{\left(F\setminus \left\{\varnothing \right\}\right)}^{-1}}^{-1}\subseteq {F^{-1}}^{-1}$$
22	19 20 21	mp2b	$$⊢{{\left(F\setminus \left\{\varnothing \right\}\right)}^{-1}}^{-1}\subseteq {F^{-1}}^{-1}$$
23	18 22	eqsstrrdi	$$⊢F\mathrm{Struct}X\to F\setminus \left\{\varnothing \right\}\subseteq {F^{-1}}^{-1}$$
24	13 23	eqssd	$$⊢F\mathrm{Struct}X\to {F^{-1}}^{-1}=F\setminus \left\{\varnothing \right\}$$