Theorem mosubott

Description: "At most one" remains true inside ordered triple quantification, analogous to mosubopt . (Contributed by BTernaryTau, 8-Sep-2026)

	Ref	Expression
Assertion	mosubott	$$⊢\forall x\forall y\forall z{\exists }^{*}w\phi \to {\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfa1	$$⊢Ⅎx\forall x\forall y\forall z{\exists }^{*}w\phi$$
2		nfe1	$$⊢Ⅎx\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)$$
3	2	nfmov	$$⊢Ⅎx{\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)$$
4		nfa1	$$⊢Ⅎy\forall y\forall z{\exists }^{*}w\phi$$
5		nfe1	$$⊢Ⅎy\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)$$
6	5	nfex	$$⊢Ⅎy\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)$$
7	6	nfmov	$$⊢Ⅎy{\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)$$
8		nfa1	$$⊢Ⅎz\forall z{\exists }^{*}w\phi$$
9		nfe1	$$⊢Ⅎz\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)$$
10	9	nfex	$$⊢Ⅎz\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)$$
11	10	nfex	$$⊢Ⅎz\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)$$
12	11	nfmov	$$⊢Ⅎz{\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)$$
13		cotsexgw	$$⊢A=⟨x,y,z⟩\to \left(\phi \leftrightarrow \exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)\right)$$
14	13	mobidv	$$⊢A=⟨x,y,z⟩\to \left({\exists }^{*}w\phi \leftrightarrow {\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)\right)$$
15	14	biimpcd	$$⊢{\exists }^{*}w\phi \to \left(A=⟨x,y,z⟩\to {\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)\right)$$
16	15	sps	$$⊢\forall z{\exists }^{*}w\phi \to \left(A=⟨x,y,z⟩\to {\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)\right)$$
17	8 12 16	exlimd	$$⊢\forall z{\exists }^{*}w\phi \to \left(\exists zA=⟨x,y,z⟩\to {\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)\right)$$
18	17	sps	$$⊢\forall y\forall z{\exists }^{*}w\phi \to \left(\exists zA=⟨x,y,z⟩\to {\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)\right)$$
19	4 7 18	exlimd	$$⊢\forall y\forall z{\exists }^{*}w\phi \to \left(\exists y\exists zA=⟨x,y,z⟩\to {\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)\right)$$
20	19	sps	$$⊢\forall x\forall y\forall z{\exists }^{*}w\phi \to \left(\exists y\exists zA=⟨x,y,z⟩\to {\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)\right)$$
21	1 3 20	exlimd	$$⊢\forall x\forall y\forall z{\exists }^{*}w\phi \to \left(\exists x\exists y\exists zA=⟨x,y,z⟩\to {\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)\right)$$
22		exsimpl	$$⊢\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)\to \exists zA=⟨x,y,z⟩$$
23	22	2eximi	$$⊢\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)\to \exists x\exists y\exists zA=⟨x,y,z⟩$$
24	23	exlimiv	$$⊢\exists w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)\to \exists x\exists y\exists zA=⟨x,y,z⟩$$
25		nexmo	$$⊢\neg \exists w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)\to {\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)$$
26	24 25	nsyl5	$$⊢\neg \exists x\exists y\exists zA=⟨x,y,z⟩\to {\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)$$
27	21 26	pm2.61d1	$$⊢\forall x\forall y\forall z{\exists }^{*}w\phi \to {\exists }^{*}w\exists x\exists y\exists z\left(A=⟨x,y,z⟩\wedge \phi \right)$$