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 ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )

Proof

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