Theorem pmtrsn

Description: The value of the transposition generator function for a singleton is empty, i.e. there is no transposition for a singleton. This also holds for A e/ _V , i.e. for the empty set { A } = (/) resulting in ( pmTrsp(/) ) = (/) . (Contributed by AV, 6-Aug-2019)

	Ref	Expression
Assertion	pmtrsn	$$⊢\mathrm{pmTrsp}\left(\left\{A\right\}\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
2		eqid	$$⊢\mathrm{pmTrsp}\left(\left\{A\right\}\right)=\mathrm{pmTrsp}\left(\left\{A\right\}\right)$$
3	2	pmtrfval	$$⊢\left\{A\right\}\in \mathrm{V}\to \mathrm{pmTrsp}\left(\left\{A\right\}\right)=\left(p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}⟼\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)$$
4	1 3	ax-mp	$$⊢\mathrm{pmTrsp}\left(\left\{A\right\}\right)=\left(p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}⟼\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)$$
5		eqid	$$⊢\left(p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}⟼\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)=\left(p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}⟼\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)$$
6	5	dmmpt	$$⊢\mathrm{dom}\left(p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}⟼\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)=\left\{p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}|\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\in \mathrm{V}\right\}$$
7		2on0	$$⊢2_{𝑜}\ne \varnothing$$
8		ensymb	$$⊢\varnothing \approx 2_{𝑜}\leftrightarrow 2_{𝑜}\approx \varnothing$$
9		en0	$$⊢2_{𝑜}\approx \varnothing \leftrightarrow 2_{𝑜}=\varnothing$$
10	8 9	bitri	$$⊢\varnothing \approx 2_{𝑜}\leftrightarrow 2_{𝑜}=\varnothing$$
11	7 10	nemtbir	$$⊢\neg \varnothing \approx 2_{𝑜}$$
12		snnen2o	$$⊢\neg \left\{A\right\}\approx 2_{𝑜}$$
13		0ex	$$⊢\varnothing \in \mathrm{V}$$
14		breq1	$$⊢y=\varnothing \to \left(y\approx 2_{𝑜}\leftrightarrow \varnothing \approx 2_{𝑜}\right)$$
15	14	notbid	$$⊢y=\varnothing \to \left(\neg y\approx 2_{𝑜}\leftrightarrow \neg \varnothing \approx 2_{𝑜}\right)$$
16		breq1	$$⊢y=\left\{A\right\}\to \left(y\approx 2_{𝑜}\leftrightarrow \left\{A\right\}\approx 2_{𝑜}\right)$$
17	16	notbid	$$⊢y=\left\{A\right\}\to \left(\neg y\approx 2_{𝑜}\leftrightarrow \neg \left\{A\right\}\approx 2_{𝑜}\right)$$
18	13 1 15 17	ralpr	$$⊢\forall y\in \left\{\varnothing ,\left\{A\right\}\right\}\neg y\approx 2_{𝑜}\leftrightarrow \left(\neg \varnothing \approx 2_{𝑜}\wedge \neg \left\{A\right\}\approx 2_{𝑜}\right)$$
19	11 12 18	mpbir2an	$$⊢\forall y\in \left\{\varnothing ,\left\{A\right\}\right\}\neg y\approx 2_{𝑜}$$
20		pwsn	$$⊢𝒫\left\{A\right\}=\left\{\varnothing ,\left\{A\right\}\right\}$$
21	20	raleqi	$$⊢\forall y\in 𝒫\left\{A\right\}\neg y\approx 2_{𝑜}\leftrightarrow \forall y\in \left\{\varnothing ,\left\{A\right\}\right\}\neg y\approx 2_{𝑜}$$
22	19 21	mpbir	$$⊢\forall y\in 𝒫\left\{A\right\}\neg y\approx 2_{𝑜}$$
23		rabeq0	$$⊢\left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}=\varnothing \leftrightarrow \forall y\in 𝒫\left\{A\right\}\neg y\approx 2_{𝑜}$$
24	22 23	mpbir	$$⊢\left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}=\varnothing$$
25	24	rabeqi	$$⊢\left\{p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}|\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\in \mathrm{V}\right\}=\left\{p\in \varnothing |\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\in \mathrm{V}\right\}$$
26		rab0	$$⊢\left\{p\in \varnothing |\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\in \mathrm{V}\right\}=\varnothing$$
27	6 25 26	3eqtri	$$⊢\mathrm{dom}\left(p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}⟼\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)=\varnothing$$
28		mptrel	$$⊢\mathrm{Rel}\left(p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}⟼\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)$$
29		reldm0	$$⊢\mathrm{Rel}\left(p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}⟼\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)\to \left(\left(p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}⟼\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)=\varnothing \leftrightarrow \mathrm{dom}\left(p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}⟼\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)=\varnothing \right)$$
30	28 29	ax-mp	$$⊢\left(p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}⟼\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)=\varnothing \leftrightarrow \mathrm{dom}\left(p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}⟼\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)=\varnothing$$
31	27 30	mpbir	$$⊢\left(p\in \left\{y\in 𝒫\left\{A\right\}|y\approx 2_{𝑜}\right\}⟼\left(z\in \left\{A\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)=\varnothing$$
32	4 31	eqtri	$$⊢\mathrm{pmTrsp}\left(\left\{A\right\}\right)=\varnothing$$