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 φ \to \exists^{} x \exists y \exists z (A = ⟨y, z⟩ \land φ)$

Proof

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

Metamath Proof Explorer

Theorem mosubopt

Proof