Theorem ax6e2ndeqALT

Description: "At least two sets exist" expressed in the form of dtru is logically equivalent to the same expressed in a form similar to ax6e if dtru is false implies u = v . Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndeqVD . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ax6e2ndeqALT	$$⊢\left(\neg \forall xx=y\vee u=v\right)\leftrightarrow \exists x\exists y\left(x=u\wedge y=v\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax6e2nd	$$⊢\neg \forall xx=y\to \exists x\exists y\left(x=u\wedge y=v\right)$$
2		ax6e2eq	$$⊢\forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)$$
3	1	a1d	$$⊢\neg \forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)$$
4		exmid	$$⊢\left(\forall xx=y\vee \neg \forall xx=y\right)$$
5		jao	$$⊢\left(\forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)\to \left(\left(\neg \forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)\to \left(\left(\forall xx=y\vee \neg \forall xx=y\right)\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)\right)$$
6	5	3imp	$$⊢\left(\left(\forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)\wedge \left(\neg \forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)\wedge \left(\forall xx=y\vee \neg \forall xx=y\right)\right)\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)$$
7	2 3 4 6	mp3an	$$⊢u=v\to \exists x\exists y\left(x=u\wedge y=v\right)$$
8	1 7	jaoi	$$⊢\left(\neg \forall xx=y\vee u=v\right)\to \exists x\exists y\left(x=u\wedge y=v\right)$$
9		hbnae	$$⊢\neg \forall xx=y\to \forall y\neg \forall xx=y$$
10	9	eximi	$$⊢\exists y\neg \forall xx=y\to \exists y\forall y\neg \forall xx=y$$
11		nfa1	$$⊢Ⅎy\forall y\neg \forall xx=y$$
12	11	19.9	$$⊢\exists y\forall y\neg \forall xx=y\leftrightarrow \forall y\neg \forall xx=y$$
13	10 12	sylib	$$⊢\exists y\neg \forall xx=y\to \forall y\neg \forall xx=y$$
14		sp	$$⊢\forall y\neg \forall xx=y\to \neg \forall xx=y$$
15	13 14	syl	$$⊢\exists y\neg \forall xx=y\to \neg \forall xx=y$$
16		excom	$$⊢\exists x\exists y\left(x=u\wedge y=v\right)\leftrightarrow \exists y\exists x\left(x=u\wedge y=v\right)$$
17		nfa1	$$⊢Ⅎx\forall xx=y$$
18	17	nfn	$$⊢Ⅎx\neg \forall xx=y$$
19	18	19.9	$$⊢\exists x\neg \forall xx=y\leftrightarrow \neg \forall xx=y$$
20		id	$$⊢u\ne v\to u\ne v$$
21		simpr	$$⊢\left(u\ne v\wedge \left(x=u\wedge y=v\right)\right)\to \left(x=u\wedge y=v\right)$$
22		simpl	$$⊢\left(x=u\wedge y=v\right)\to x=u$$
23	21 22	syl	$$⊢\left(u\ne v\wedge \left(x=u\wedge y=v\right)\right)\to x=u$$
24		pm13.181	$$⊢\left(x=u\wedge u\ne v\right)\to x\ne v$$
25	24	ancoms	$$⊢\left(u\ne v\wedge x=u\right)\to x\ne v$$
26	20 23 25	syl2an2r	$$⊢\left(u\ne v\wedge \left(x=u\wedge y=v\right)\right)\to x\ne v$$
27		simpr	$$⊢\left(x=u\wedge y=v\right)\to y=v$$
28	21 27	syl	$$⊢\left(u\ne v\wedge \left(x=u\wedge y=v\right)\right)\to y=v$$
29		neeq2	$$⊢y=v\to \left(x\ne y\leftrightarrow x\ne v\right)$$
30	29	biimparc	$$⊢\left(x\ne v\wedge y=v\right)\to x\ne y$$
31	26 28 30	syl2anc	$$⊢\left(u\ne v\wedge \left(x=u\wedge y=v\right)\right)\to x\ne y$$
32		df-ne	$$⊢x\ne y\leftrightarrow \neg x=y$$
33	32	bicomi	$$⊢\neg x=y\leftrightarrow x\ne y$$
34		sp	$$⊢\forall xx=y\to x=y$$
35	34	con3i	$$⊢\neg x=y\to \neg \forall xx=y$$
36	33 35	sylbir	$$⊢x\ne y\to \neg \forall xx=y$$
37	31 36	syl	$$⊢\left(u\ne v\wedge \left(x=u\wedge y=v\right)\right)\to \neg \forall xx=y$$
38	37	ex	$$⊢u\ne v\to \left(\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)$$
39	38	alrimiv	$$⊢u\ne v\to \forall x\left(\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)$$
40		exim	$$⊢\forall x\left(\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\to \left(\exists x\left(x=u\wedge y=v\right)\to \exists x\neg \forall xx=y\right)$$
41	39 40	syl	$$⊢u\ne v\to \left(\exists x\left(x=u\wedge y=v\right)\to \exists x\neg \forall xx=y\right)$$
42		imbi2	$$⊢\left(\exists x\neg \forall xx=y\leftrightarrow \neg \forall xx=y\right)\to \left(\left(\exists x\left(x=u\wedge y=v\right)\to \exists x\neg \forall xx=y\right)\leftrightarrow \left(\exists x\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\right)$$
43	42	biimpa	$$⊢\left(\left(\exists x\neg \forall xx=y\leftrightarrow \neg \forall xx=y\right)\wedge \left(\exists x\left(x=u\wedge y=v\right)\to \exists x\neg \forall xx=y\right)\right)\to \left(\exists x\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)$$
44	19 41 43	sylancr	$$⊢u\ne v\to \left(\exists x\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)$$
45	44	alrimiv	$$⊢u\ne v\to \forall y\left(\exists x\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)$$
46		exim	$$⊢\forall y\left(\exists x\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\to \left(\exists y\exists x\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)$$
47	45 46	syl	$$⊢u\ne v\to \left(\exists y\exists x\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)$$
48		imbi1	$$⊢\left(\exists x\exists y\left(x=u\wedge y=v\right)\leftrightarrow \exists y\exists x\left(x=u\wedge y=v\right)\right)\to \left(\left(\exists x\exists y\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)\leftrightarrow \left(\exists y\exists x\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)\right)$$
49	48	biimpar	$$⊢\left(\left(\exists x\exists y\left(x=u\wedge y=v\right)\leftrightarrow \exists y\exists x\left(x=u\wedge y=v\right)\right)\wedge \left(\exists y\exists x\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)\right)\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)$$
50	16 47 49	sylancr	$$⊢u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)$$
51		pm3.34	$$⊢\left(\left(\exists y\neg \forall xx=y\to \neg \forall xx=y\right)\wedge \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)\right)\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)$$
52	15 50 51	sylancr	$$⊢u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)$$
53		orc	$$⊢\neg \forall xx=y\to \left(\neg \forall xx=y\vee u=v\right)$$
54	53	imim2i	$$⊢\left(\exists x\exists y\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)$$
55	52 54	syl	$$⊢u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)$$
56	55	idiALT	$$⊢u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)$$
57		id	$$⊢u=v\to u=v$$
58		ax-1	$$⊢u=v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to u=v\right)$$
59	57 58	syl	$$⊢u=v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to u=v\right)$$
60		olc	$$⊢u=v\to \left(\neg \forall xx=y\vee u=v\right)$$
61	60	imim2i	$$⊢\left(\exists x\exists y\left(x=u\wedge y=v\right)\to u=v\right)\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)$$
62	59 61	syl	$$⊢u=v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)$$
63	62	idiALT	$$⊢u=v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)$$
64		exmidne	$$⊢\left(u=v\vee u\ne v\right)$$
65		jao	$$⊢\left(u=v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)\right)\to \left(\left(u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)\right)\to \left(\left(u=v\vee u\ne v\right)\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)\right)\right)$$
66	65	3imp21	$$⊢\left(\left(u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)\right)\wedge \left(u=v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)\right)\wedge \left(u=v\vee u\ne v\right)\right)\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)$$
67	56 63 64 66	mp3an	$$⊢\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)$$
68	8 67	impbii	$$⊢\left(\neg \forall xx=y\vee u=v\right)\leftrightarrow \exists x\exists y\left(x=u\wedge y=v\right)$$