Theorem mosubopt

Description: "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007)

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

Proof

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