2reu1

Description: Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 . (Contributed by Alexander van der Vekens, 25-Jun-2017)

		Ref	Expression
	Assertion	2reu1	$⊢ \forall x \in A \exists^{*} y \in B φ \to (\exists! x \in A \exists! y \in B φ \leftrightarrow (\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ))$

Proof

Step	Hyp	Ref	Expression
1		2reu5a	$⊢ \exists! x \in A \exists! y \in B φ \leftrightarrow (\exists x \in A (\exists y \in B φ \land \exists^{} y \in B φ) \land \exists^{} x \in A (\exists y \in B φ \land \exists^{*} y \in B φ))$
2		simprr	$⊢ (x \in A \land (\forall x \in A \exists^{*} y \in B φ \land \exists y \in B φ)) \to \exists y \in B φ$
3		rsp	$⊢ \forall x \in A \exists^{} y \in B φ \to (x \in A \to \exists^{} y \in B φ)$
4	3	adantr	$⊢ (\forall x \in A \exists^{} y \in B φ \land \exists y \in B φ) \to (x \in A \to \exists^{} y \in B φ)$
5	4	impcom	$⊢ (x \in A \land (\forall x \in A \exists^{} y \in B φ \land \exists y \in B φ)) \to \exists^{} y \in B φ$
6	2 5	jca	$⊢ (x \in A \land (\forall x \in A \exists^{} y \in B φ \land \exists y \in B φ)) \to (\exists y \in B φ \land \exists^{} y \in B φ)$
7	6	ex	$⊢ x \in A \to ((\forall x \in A \exists^{} y \in B φ \land \exists y \in B φ) \to (\exists y \in B φ \land \exists^{} y \in B φ))$
8	7	rmoimia	$⊢ \exists^{} x \in A (\exists y \in B φ \land \exists^{} y \in B φ) \to \exists^{} x \in A (\forall x \in A \exists^{} y \in B φ \land \exists y \in B φ)$
9		nfra1	$⊢ Ⅎ x \forall x \in A \exists^{*} y \in B φ$
10	9	rmoanim	$⊢ \exists^{} x \in A (\forall x \in A \exists^{} y \in B φ \land \exists y \in B φ) \leftrightarrow (\forall x \in A \exists^{} y \in B φ \to \exists^{} x \in A \exists y \in B φ)$
11	8 10	sylib	$⊢ \exists^{} x \in A (\exists y \in B φ \land \exists^{} y \in B φ) \to (\forall x \in A \exists^{} y \in B φ \to \exists^{} x \in A \exists y \in B φ)$
12	11	ancrd	$⊢ \exists^{} x \in A (\exists y \in B φ \land \exists^{} y \in B φ) \to (\forall x \in A \exists^{} y \in B φ \to (\exists^{} x \in A \exists y \in B φ \land \forall x \in A \exists^{*} y \in B φ))$
13		2rmoswap	$⊢ \forall x \in A \exists^{} y \in B φ \to (\exists^{} x \in A \exists y \in B φ \to \exists^{*} y \in B \exists x \in A φ)$
14	13	com12	$⊢ \exists^{} x \in A \exists y \in B φ \to (\forall x \in A \exists^{} y \in B φ \to \exists^{*} y \in B \exists x \in A φ)$
15	14	imdistani	$⊢ (\exists^{} x \in A \exists y \in B φ \land \forall x \in A \exists^{} y \in B φ) \to (\exists^{} x \in A \exists y \in B φ \land \exists^{} y \in B \exists x \in A φ)$
16	12 15	syl6	$⊢ \exists^{} x \in A (\exists y \in B φ \land \exists^{} y \in B φ) \to (\forall x \in A \exists^{} y \in B φ \to (\exists^{} x \in A \exists y \in B φ \land \exists^{*} y \in B \exists x \in A φ))$
17	1 16	simplbiim	$⊢ \exists! x \in A \exists! y \in B φ \to (\forall x \in A \exists^{} y \in B φ \to (\exists^{} x \in A \exists y \in B φ \land \exists^{*} y \in B \exists x \in A φ))$
18		2reu2rex	$⊢ \exists! x \in A \exists! y \in B φ \to \exists x \in A \exists y \in B φ$
19		rexcom	$⊢ \exists x \in A \exists y \in B φ \leftrightarrow \exists y \in B \exists x \in A φ$
20	18 19	sylib	$⊢ \exists! x \in A \exists! y \in B φ \to \exists y \in B \exists x \in A φ$
21	18 20	jca	$⊢ \exists! x \in A \exists! y \in B φ \to (\exists x \in A \exists y \in B φ \land \exists y \in B \exists x \in A φ)$
22	17 21	jctild	$⊢ \exists! x \in A \exists! y \in B φ \to (\forall x \in A \exists^{} y \in B φ \to ((\exists x \in A \exists y \in B φ \land \exists y \in B \exists x \in A φ) \land (\exists^{} x \in A \exists y \in B φ \land \exists^{*} y \in B \exists x \in A φ)))$
23		reu5	$⊢ \exists! x \in A \exists y \in B φ \leftrightarrow (\exists x \in A \exists y \in B φ \land \exists^{*} x \in A \exists y \in B φ)$
24		reu5	$⊢ \exists! y \in B \exists x \in A φ \leftrightarrow (\exists y \in B \exists x \in A φ \land \exists^{*} y \in B \exists x \in A φ)$
25	23 24	anbi12i	$⊢ (\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ) \leftrightarrow ((\exists x \in A \exists y \in B φ \land \exists^{} x \in A \exists y \in B φ) \land (\exists y \in B \exists x \in A φ \land \exists^{} y \in B \exists x \in A φ))$
26		an4	$⊢ ((\exists x \in A \exists y \in B φ \land \exists^{} x \in A \exists y \in B φ) \land (\exists y \in B \exists x \in A φ \land \exists^{} y \in B \exists x \in A φ)) \leftrightarrow ((\exists x \in A \exists y \in B φ \land \exists y \in B \exists x \in A φ) \land (\exists^{} x \in A \exists y \in B φ \land \exists^{} y \in B \exists x \in A φ))$
27	25 26	bitri	$⊢ (\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ) \leftrightarrow ((\exists x \in A \exists y \in B φ \land \exists y \in B \exists x \in A φ) \land (\exists^{} x \in A \exists y \in B φ \land \exists^{} y \in B \exists x \in A φ))$
28	22 27	imbitrrdi	$⊢ \exists! x \in A \exists! y \in B φ \to (\forall x \in A \exists^{*} y \in B φ \to (\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ))$
29	28	com12	$⊢ \forall x \in A \exists^{*} y \in B φ \to (\exists! x \in A \exists! y \in B φ \to (\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ))$
30		2rexreu	$⊢ (\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ) \to \exists! x \in A \exists! y \in B φ$
31	29 30	impbid1	$⊢ \forall x \in A \exists^{*} y \in B φ \to (\exists! x \in A \exists! y \in B φ \leftrightarrow (\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ))$

Metamath Proof Explorer

Theorem 2reu1

Proof