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 
|- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )

Proof

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