Theorem ax6e2ndeqALT 42551

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

Assertion

Ref	Expression
ax6e2ndeqALT	⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Distinct variable groups:   𝑥,𝑢   𝑦,𝑢   𝑥,𝑣   𝑦,𝑣

Proof of Theorem ax6e2ndeqALT

Step	Hyp	Ref	Expression
1		ax6e2nd 42178	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
2		ax6e2eq 42177	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
3	1	a1d 25	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
4		exmid 892	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦)
5		jao 958	. . . . 5 ⊢ ((∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → ((¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → ((∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))))
6	5	3imp 1110	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) ∧ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) ∧ (∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦)) → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
7	2, 3, 4, 6	mp3an 1460	. . 3 ⊢ (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
8	1, 7	jaoi 854	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
9		hbnae 2432	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
10	9	eximi 1837	. . . . . . . 8 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
11		nfa1 2148	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦
12	11	19.9 2198	. . . . . . . 8 ⊢ (∃𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
13	10, 12	sylib 217	. . . . . . 7 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
14		sp 2176	. . . . . . 7 ⊢ (∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
15	13, 14	syl 17	. . . . . 6 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
16		excom 2162	. . . . . . 7 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
17		nfa1 2148	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑥 𝑥 = 𝑦
18	17	nfn 1860	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦
19	18	19.9 2198	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
20		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ≠ 𝑣 → 𝑢 ≠ 𝑣)
21		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ≠ 𝑣 ∧ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
22		simpl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
23	21, 22	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ≠ 𝑣 ∧ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → 𝑥 = 𝑢)
24		pm13.181 3026	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑢 ≠ 𝑣) → 𝑥 ≠ 𝑣)
25	24	ancoms 459	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ≠ 𝑣 ∧ 𝑥 = 𝑢) → 𝑥 ≠ 𝑣)
26	20, 23, 25	syl2an2r 682	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ≠ 𝑣 ∧ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → 𝑥 ≠ 𝑣)
27		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
28	21, 27	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ≠ 𝑣 ∧ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → 𝑦 = 𝑣)
29		neeq2 3007	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑣 → (𝑥 ≠ 𝑦 ↔ 𝑥 ≠ 𝑣))
30	29	biimparc 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ≠ 𝑣 ∧ 𝑦 = 𝑣) → 𝑥 ≠ 𝑦)
31	26, 28, 30	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ≠ 𝑣 ∧ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → 𝑥 ≠ 𝑦)
32		df-ne 2944	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦)
33	32	bicomi 223	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦)
34		sp 2176	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
35	34	con3i 154	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
36	33, 35	sylbir 234	. . . . . . . . . . . . . 14 ⊢ (𝑥 ≠ 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
37	31, 36	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑢 ≠ 𝑣 ∧ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → ¬ ∀𝑥 𝑥 = 𝑦)
38	37	ex 413	. . . . . . . . . . . 12 ⊢ (𝑢 ≠ 𝑣 → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
39	38	alrimiv 1930	. . . . . . . . . . 11 ⊢ (𝑢 ≠ 𝑣 → ∀𝑥((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
40		exim 1836	. . . . . . . . . . 11 ⊢ (∀𝑥((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦))
41	39, 40	syl 17	. . . . . . . . . 10 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦))
42		imbi2 349	. . . . . . . . . . 11 ⊢ ((∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦) ↔ (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
43	42	biimpa 477	. . . . . . . . . 10 ⊢ (((∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) ∧ (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦)) → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
44	19, 41, 43	sylancr 587	. . . . . . . . 9 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
45	44	alrimiv 1930	. . . . . . . 8 ⊢ (𝑢 ≠ 𝑣 → ∀𝑦(∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
46		exim 1836	. . . . . . . 8 ⊢ (∀𝑦(∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦))
47	45, 46	syl 17	. . . . . . 7 ⊢ (𝑢 ≠ 𝑣 → (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦))
48		imbi1 348	. . . . . . . 8 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) ↔ (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)))
49	48	biimpar 478	. . . . . . 7 ⊢ (((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) ∧ (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦))
50	16, 47, 49	sylancr 587	. . . . . 6 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦))
51		pm3.34 763	. . . . . 6 ⊢ (((∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦) ∧ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
52	15, 50, 51	sylancr 587	. . . . 5 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
53		orc 864	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
54	53	imim2i 16	. . . . 5 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
55	52, 54	syl 17	. . . 4 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
56	55	idiALT 42097	. . 3 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
57		id 22	. . . . . 6 ⊢ (𝑢 = 𝑣 → 𝑢 = 𝑣)
58		ax-1 6	. . . . . 6 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣))
59	57, 58	syl 17	. . . . 5 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣))
60		olc 865	. . . . . 6 ⊢ (𝑢 = 𝑣 → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
61	60	imim2i 16	. . . . 5 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
62	59, 61	syl 17	. . . 4 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
63	62	idiALT 42097	. . 3 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
64		exmidne 2953	. . 3 ⊢ (𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣)
65		jao 958	. . . 4 ⊢ ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))))
66	65	3imp21 1113	. . 3 ⊢ (((𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) ∧ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) ∧ (𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣)) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
67	56, 63, 64, 66	mp3an 1460	. 2 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
68	8, 67	impbii 208	1 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844  ∀wal 1537   = wceq 1539  ∃wex 1782   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2372  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-v 3434

This theorem is referenced by: (None)