Theorem 2reu3

Description: Double restricted existential uniqueness, analogous to 2eu3 . (Contributed by Alexander van der Vekens, 29-Jun-2017)

	Ref	Expression
Assertion	2reu3	$$⊢\forall x\in A\forall y\in B\left({\exists }^{*}x\in A\phi \vee {\exists }^{*}y\in B\phi \right)\to \left(\left(\exists !x\in A\exists !y\in B\phi \wedge \exists !y\in B\exists !x\in A\phi \right)\leftrightarrow \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		orcom	$$⊢\left({\exists }^{*}x\in A\phi \vee {\exists }^{*}y\in B\phi \right)\leftrightarrow \left({\exists }^{*}y\in B\phi \vee {\exists }^{*}x\in A\phi \right)$$
2	1	ralbii	$$⊢\forall y\in B\left({\exists }^{*}x\in A\phi \vee {\exists }^{*}y\in B\phi \right)\leftrightarrow \forall y\in B\left({\exists }^{*}y\in B\phi \vee {\exists }^{*}x\in A\phi \right)$$
3		nfrmo1	$$⊢Ⅎy{\exists }^{*}y\in B\phi$$
4	3	r19.32	$$⊢\forall y\in B\left({\exists }^{*}y\in B\phi \vee {\exists }^{*}x\in A\phi \right)\leftrightarrow \left({\exists }^{*}y\in B\phi \vee \forall y\in B{\exists }^{*}x\in A\phi \right)$$
5	2 4	bitri	$$⊢\forall y\in B\left({\exists }^{*}x\in A\phi \vee {\exists }^{*}y\in B\phi \right)\leftrightarrow \left({\exists }^{*}y\in B\phi \vee \forall y\in B{\exists }^{*}x\in A\phi \right)$$
6		orcom	$$⊢\left({\exists }^{*}y\in B\phi \vee \forall y\in B{\exists }^{*}x\in A\phi \right)\leftrightarrow \left(\forall y\in B{\exists }^{*}x\in A\phi \vee {\exists }^{*}y\in B\phi \right)$$
7	5 6	bitri	$$⊢\forall y\in B\left({\exists }^{*}x\in A\phi \vee {\exists }^{*}y\in B\phi \right)\leftrightarrow \left(\forall y\in B{\exists }^{*}x\in A\phi \vee {\exists }^{*}y\in B\phi \right)$$
8	7	ralbii	$$⊢\forall x\in A\forall y\in B\left({\exists }^{*}x\in A\phi \vee {\exists }^{*}y\in B\phi \right)\leftrightarrow \forall x\in A\left(\forall y\in B{\exists }^{*}x\in A\phi \vee {\exists }^{*}y\in B\phi \right)$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
10		nfrmo1	$$⊢Ⅎx{\exists }^{*}x\in A\phi$$
11	9 10	nfralw	$$⊢Ⅎx\forall y\in B{\exists }^{*}x\in A\phi$$
12	11	r19.32	$$⊢\forall x\in A\left(\forall y\in B{\exists }^{*}x\in A\phi \vee {\exists }^{*}y\in B\phi \right)\leftrightarrow \left(\forall y\in B{\exists }^{*}x\in A\phi \vee \forall x\in A{\exists }^{*}y\in B\phi \right)$$
13	8 12	bitri	$$⊢\forall x\in A\forall y\in B\left({\exists }^{*}x\in A\phi \vee {\exists }^{*}y\in B\phi \right)\leftrightarrow \left(\forall y\in B{\exists }^{*}x\in A\phi \vee \forall x\in A{\exists }^{*}y\in B\phi \right)$$
14		2reu1	$$⊢\forall y\in B{\exists }^{*}x\in A\phi \to \left(\exists !y\in B\exists !x\in A\phi \leftrightarrow \left(\exists !y\in B\exists x\in A\phi \wedge \exists !x\in A\exists y\in B\phi \right)\right)$$
15	14	biimpd	$$⊢\forall y\in B{\exists }^{*}x\in A\phi \to \left(\exists !y\in B\exists !x\in A\phi \to \left(\exists !y\in B\exists x\in A\phi \wedge \exists !x\in A\exists y\in B\phi \right)\right)$$
16		ancom	$$⊢\left(\exists !y\in B\exists x\in A\phi \wedge \exists !x\in A\exists y\in B\phi \right)\leftrightarrow \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)$$
17	15 16	syl6ib	$$⊢\forall y\in B{\exists }^{*}x\in A\phi \to \left(\exists !y\in B\exists !x\in A\phi \to \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\right)$$
18	17	adantld	$$⊢\forall y\in B{\exists }^{*}x\in A\phi \to \left(\left(\exists !x\in A\exists !y\in B\phi \wedge \exists !y\in B\exists !x\in A\phi \right)\to \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\right)$$
19		2reu1	$$⊢\forall x\in A{\exists }^{*}y\in B\phi \to \left(\exists !x\in A\exists !y\in B\phi \leftrightarrow \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\right)$$
20	19	biimpd	$$⊢\forall x\in A{\exists }^{*}y\in B\phi \to \left(\exists !x\in A\exists !y\in B\phi \to \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\right)$$
21	20	adantrd	$$⊢\forall x\in A{\exists }^{*}y\in B\phi \to \left(\left(\exists !x\in A\exists !y\in B\phi \wedge \exists !y\in B\exists !x\in A\phi \right)\to \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\right)$$
22	18 21	jaoi	$$⊢\left(\forall y\in B{\exists }^{*}x\in A\phi \vee \forall x\in A{\exists }^{*}y\in B\phi \right)\to \left(\left(\exists !x\in A\exists !y\in B\phi \wedge \exists !y\in B\exists !x\in A\phi \right)\to \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\right)$$
23		2rexreu	$$⊢\left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\to \exists !x\in A\exists !y\in B\phi$$
24		2rexreu	$$⊢\left(\exists !y\in B\exists x\in A\phi \wedge \exists !x\in A\exists y\in B\phi \right)\to \exists !y\in B\exists !x\in A\phi$$
25	24	ancoms	$$⊢\left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\to \exists !y\in B\exists !x\in A\phi$$
26	23 25	jca	$$⊢\left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\to \left(\exists !x\in A\exists !y\in B\phi \wedge \exists !y\in B\exists !x\in A\phi \right)$$
27	22 26	impbid1	$$⊢\left(\forall y\in B{\exists }^{*}x\in A\phi \vee \forall x\in A{\exists }^{*}y\in B\phi \right)\to \left(\left(\exists !x\in A\exists !y\in B\phi \wedge \exists !y\in B\exists !x\in A\phi \right)\leftrightarrow \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\right)$$
28	13 27	sylbi	$$⊢\forall x\in A\forall y\in B\left({\exists }^{*}x\in A\phi \vee {\exists }^{*}y\in B\phi \right)\to \left(\left(\exists !x\in A\exists !y\in B\phi \wedge \exists !y\in B\exists !x\in A\phi \right)\leftrightarrow \left(\exists !x\in A\exists y\in B\phi \wedge \exists !y\in B\exists x\in A\phi \right)\right)$$