Theorem reusv2lem2

Description: Lemma for reusv2 . (Contributed by NM, 27-Oct-2010) (Proof shortened by Mario Carneiro, 19-Nov-2016) (Proof shortened by JJ, 7-Aug-2021)

	Ref	Expression
Assertion	reusv2lem2	$$⊢\exists !x\forall y\in Ax=B\to \exists !x\exists y\in Ax=B$$

Proof

Step	Hyp	Ref	Expression
1		eunex	$$⊢\exists !x\forall y\in Ax=B\to \exists x\neg \forall y\in Ax=B$$
2		exnal	$$⊢\exists x\neg \forall y\in Ax=B\leftrightarrow \neg \forall x\forall y\in Ax=B$$
3	1 2	sylib	$$⊢\exists !x\forall y\in Ax=B\to \neg \forall x\forall y\in Ax=B$$
4		rzal	$$⊢A=\varnothing \to \forall y\in Ax=B$$
5	4	alrimiv	$$⊢A=\varnothing \to \forall x\forall y\in Ax=B$$
6	3 5	nsyl3	$$⊢A=\varnothing \to \neg \exists !x\forall y\in Ax=B$$
7	6	pm2.21d	$$⊢A=\varnothing \to \left(\exists !x\forall y\in Ax=B\to \exists !x\exists y\in Ax=B\right)$$
8		simpr	$$⊢\left(A\ne \varnothing \wedge \exists !x\forall y\in Ax=B\right)\to \exists !x\forall y\in Ax=B$$
9		nfra1	$$⊢Ⅎy\forall y\in Az=B$$
10		nfra1	$$⊢Ⅎy\forall y\in Ax=B$$
11		simpr	$$⊢\left(\left(\forall y\in Az=B\wedge y\in A\right)\wedge x=B\right)\to x=B$$
12		rspa	$$⊢\left(\forall y\in Az=B\wedge y\in A\right)\to z=B$$
13	12	adantr	$$⊢\left(\left(\forall y\in Az=B\wedge y\in A\right)\wedge x=B\right)\to z=B$$
14	11 13	eqtr4d	$$⊢\left(\left(\forall y\in Az=B\wedge y\in A\right)\wedge x=B\right)\to x=z$$
15		eqeq1	$$⊢x=z\to \left(x=B\leftrightarrow z=B\right)$$
16	15	ralbidv	$$⊢x=z\to \left(\forall y\in Ax=B\leftrightarrow \forall y\in Az=B\right)$$
17	16	biimprcd	$$⊢\forall y\in Az=B\to \left(x=z\to \forall y\in Ax=B\right)$$
18	17	ad2antrr	$$⊢\left(\left(\forall y\in Az=B\wedge y\in A\right)\wedge x=B\right)\to \left(x=z\to \forall y\in Ax=B\right)$$
19	14 18	mpd	$$⊢\left(\left(\forall y\in Az=B\wedge y\in A\right)\wedge x=B\right)\to \forall y\in Ax=B$$
20	19	exp31	$$⊢\forall y\in Az=B\to \left(y\in A\to \left(x=B\to \forall y\in Ax=B\right)\right)$$
21	9 10 20	rexlimd	$$⊢\forall y\in Az=B\to \left(\exists y\in Ax=B\to \forall y\in Ax=B\right)$$
22	21	adantl	$$⊢\left(A\ne \varnothing \wedge \forall y\in Az=B\right)\to \left(\exists y\in Ax=B\to \forall y\in Ax=B\right)$$
23		r19.2z	$$⊢\left(A\ne \varnothing \wedge \forall y\in Ax=B\right)\to \exists y\in Ax=B$$
24	23	ex	$$⊢A\ne \varnothing \to \left(\forall y\in Ax=B\to \exists y\in Ax=B\right)$$
25	24	adantr	$$⊢\left(A\ne \varnothing \wedge \forall y\in Az=B\right)\to \left(\forall y\in Ax=B\to \exists y\in Ax=B\right)$$
26	22 25	impbid	$$⊢\left(A\ne \varnothing \wedge \forall y\in Az=B\right)\to \left(\exists y\in Ax=B\leftrightarrow \forall y\in Ax=B\right)$$
27	26	eubidv	$$⊢\left(A\ne \varnothing \wedge \forall y\in Az=B\right)\to \left(\exists !x\exists y\in Ax=B\leftrightarrow \exists !x\forall y\in Ax=B\right)$$
28	27	ex	$$⊢A\ne \varnothing \to \left(\forall y\in Az=B\to \left(\exists !x\exists y\in Ax=B\leftrightarrow \exists !x\forall y\in Ax=B\right)\right)$$
29	28	exlimdv	$$⊢A\ne \varnothing \to \left(\exists z\forall y\in Az=B\to \left(\exists !x\exists y\in Ax=B\leftrightarrow \exists !x\forall y\in Ax=B\right)\right)$$
30		euex	$$⊢\exists !x\forall y\in Ax=B\to \exists x\forall y\in Ax=B$$
31	16	cbvexvw	$$⊢\exists x\forall y\in Ax=B\leftrightarrow \exists z\forall y\in Az=B$$
32	30 31	sylib	$$⊢\exists !x\forall y\in Ax=B\to \exists z\forall y\in Az=B$$
33	29 32	impel	$$⊢\left(A\ne \varnothing \wedge \exists !x\forall y\in Ax=B\right)\to \left(\exists !x\exists y\in Ax=B\leftrightarrow \exists !x\forall y\in Ax=B\right)$$
34	8 33	mpbird	$$⊢\left(A\ne \varnothing \wedge \exists !x\forall y\in Ax=B\right)\to \exists !x\exists y\in Ax=B$$
35	34	ex	$$⊢A\ne \varnothing \to \left(\exists !x\forall y\in Ax=B\to \exists !x\exists y\in Ax=B\right)$$
36	7 35	pm2.61ine	$$⊢\exists !x\forall y\in Ax=B\to \exists !x\exists y\in Ax=B$$