Metamath Proof Explorer


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 ¬xx=yu=vxyx=uy=v

Proof

Step Hyp Ref Expression
1 ax6e2nd ¬xx=yxyx=uy=v
2 ax6e2eq xx=yu=vxyx=uy=v
3 1 a1d ¬xx=yu=vxyx=uy=v
4 exmid xx=y¬xx=y
5 jao xx=yu=vxyx=uy=v¬xx=yu=vxyx=uy=vxx=y¬xx=yu=vxyx=uy=v
6 5 3imp xx=yu=vxyx=uy=v¬xx=yu=vxyx=uy=vxx=y¬xx=yu=vxyx=uy=v
7 2 3 4 6 mp3an u=vxyx=uy=v
8 1 7 jaoi ¬xx=yu=vxyx=uy=v
9 hbnae ¬xx=yy¬xx=y
10 9 eximi y¬xx=yyy¬xx=y
11 nfa1 yy¬xx=y
12 11 19.9 yy¬xx=yy¬xx=y
13 10 12 sylib y¬xx=yy¬xx=y
14 sp y¬xx=y¬xx=y
15 13 14 syl y¬xx=y¬xx=y
16 excom xyx=uy=vyxx=uy=v
17 nfa1 xxx=y
18 17 nfn x¬xx=y
19 18 19.9 x¬xx=y¬xx=y
20 id uvuv
21 simpr uvx=uy=vx=uy=v
22 simpl x=uy=vx=u
23 21 22 syl uvx=uy=vx=u
24 pm13.181 x=uuvxv
25 24 ancoms uvx=uxv
26 20 23 25 syl2an2r uvx=uy=vxv
27 simpr x=uy=vy=v
28 21 27 syl uvx=uy=vy=v
29 neeq2 y=vxyxv
30 29 biimparc xvy=vxy
31 26 28 30 syl2anc uvx=uy=vxy
32 df-ne xy¬x=y
33 32 bicomi ¬x=yxy
34 sp xx=yx=y
35 34 con3i ¬x=y¬xx=y
36 33 35 sylbir xy¬xx=y
37 31 36 syl uvx=uy=v¬xx=y
38 37 ex uvx=uy=v¬xx=y
39 38 alrimiv uvxx=uy=v¬xx=y
40 exim xx=uy=v¬xx=yxx=uy=vx¬xx=y
41 39 40 syl uvxx=uy=vx¬xx=y
42 imbi2 x¬xx=y¬xx=yxx=uy=vx¬xx=yxx=uy=v¬xx=y
43 42 biimpa x¬xx=y¬xx=yxx=uy=vx¬xx=yxx=uy=v¬xx=y
44 19 41 43 sylancr uvxx=uy=v¬xx=y
45 44 alrimiv uvyxx=uy=v¬xx=y
46 exim yxx=uy=v¬xx=yyxx=uy=vy¬xx=y
47 45 46 syl uvyxx=uy=vy¬xx=y
48 imbi1 xyx=uy=vyxx=uy=vxyx=uy=vy¬xx=yyxx=uy=vy¬xx=y
49 48 biimpar xyx=uy=vyxx=uy=vyxx=uy=vy¬xx=yxyx=uy=vy¬xx=y
50 16 47 49 sylancr uvxyx=uy=vy¬xx=y
51 pm3.34 y¬xx=y¬xx=yxyx=uy=vy¬xx=yxyx=uy=v¬xx=y
52 15 50 51 sylancr uvxyx=uy=v¬xx=y
53 orc ¬xx=y¬xx=yu=v
54 53 imim2i xyx=uy=v¬xx=yxyx=uy=v¬xx=yu=v
55 52 54 syl uvxyx=uy=v¬xx=yu=v
56 55 idiALT uvxyx=uy=v¬xx=yu=v
57 id u=vu=v
58 ax-1 u=vxyx=uy=vu=v
59 57 58 syl u=vxyx=uy=vu=v
60 olc u=v¬xx=yu=v
61 60 imim2i xyx=uy=vu=vxyx=uy=v¬xx=yu=v
62 59 61 syl u=vxyx=uy=v¬xx=yu=v
63 62 idiALT u=vxyx=uy=v¬xx=yu=v
64 exmidne u=vuv
65 jao u=vxyx=uy=v¬xx=yu=vuvxyx=uy=v¬xx=yu=vu=vuvxyx=uy=v¬xx=yu=v
66 65 3imp21 uvxyx=uy=v¬xx=yu=vu=vxyx=uy=v¬xx=yu=vu=vuvxyx=uy=v¬xx=yu=v
67 56 63 64 66 mp3an xyx=uy=v¬xx=yu=v
68 8 67 impbii ¬xx=yu=vxyx=uy=v