Theorem ax6e2ndeqALT 41637

Description: "At least two sets exist" expressed in the form of dtru 5236 is logically equivalent to the same expressed in a form similar to ax6e 2390 if dtru 5236 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 41615. (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 41264	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
2		ax6e2eq 41263	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
3	1	a1d 25	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
4		exmid 892	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦)
5		jao 958	. . . . 5 ⊢ ((∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → ((¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → ((∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))))
6	5	3imp 1108	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) ∧ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) ∧ (∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦)) → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
7	2, 3, 4, 6	mp3an 1458	. . 3 ⊢ (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
8	1, 7	jaoi 854	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
9		hbnae 2443	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
10	9	eximi 1836	. . . . . . . 8 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
11		nfa1 2152	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦
12	11	19.9 2203	. . . . . . . 8 ⊢ (∃𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
13	10, 12	sylib 221	. . . . . . 7 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
14		sp 2180	. . . . . . 7 ⊢ (∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
15	13, 14	syl 17	. . . . . 6 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
16		excom 2166	. . . . . . 7 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
17		nfa1 2152	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑥 𝑥 = 𝑦
18	17	nfn 1858	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦
19	18	19.9 2203	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
20		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ≠ 𝑣 → 𝑢 ≠ 𝑣)
21		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ≠ 𝑣 ∧ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
22		simpl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
23	21, 22	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ≠ 𝑣 ∧ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → 𝑥 = 𝑢)
24		pm13.181 3069	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑢 ≠ 𝑣) → 𝑥 ≠ 𝑣)
25	24	ancoms 462	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ≠ 𝑣 ∧ 𝑥 = 𝑢) → 𝑥 ≠ 𝑣)
26	20, 23, 25	syl2an2r 684	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ≠ 𝑣 ∧ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → 𝑥 ≠ 𝑣)
27		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
28	21, 27	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ≠ 𝑣 ∧ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → 𝑦 = 𝑣)
29		neeq2 3050	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑣 → (𝑥 ≠ 𝑦 ↔ 𝑥 ≠ 𝑣))
30	29	biimparc 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ≠ 𝑣 ∧ 𝑦 = 𝑣) → 𝑥 ≠ 𝑦)
31	26, 28, 30	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ≠ 𝑣 ∧ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → 𝑥 ≠ 𝑦)
32		df-ne 2988	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦)
33	32	bicomi 227	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦)
34		sp 2180	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
35	34	con3i 157	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
36	33, 35	sylbir 238	. . . . . . . . . . . . . 14 ⊢ (𝑥 ≠ 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
37	31, 36	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑢 ≠ 𝑣 ∧ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → ¬ ∀𝑥 𝑥 = 𝑦)
38	37	ex 416	. . . . . . . . . . . 12 ⊢ (𝑢 ≠ 𝑣 → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
39	38	alrimiv 1928	. . . . . . . . . . 11 ⊢ (𝑢 ≠ 𝑣 → ∀𝑥((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
40		exim 1835	. . . . . . . . . . 11 ⊢ (∀𝑥((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦))
41	39, 40	syl 17	. . . . . . . . . 10 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦))
42		imbi2 352	. . . . . . . . . . 11 ⊢ ((∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦) ↔ (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
43	42	biimpa 480	. . . . . . . . . 10 ⊢ (((∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) ∧ (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦)) → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
44	19, 41, 43	sylancr 590	. . . . . . . . 9 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
45	44	alrimiv 1928	. . . . . . . 8 ⊢ (𝑢 ≠ 𝑣 → ∀𝑦(∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
46		exim 1835	. . . . . . . 8 ⊢ (∀𝑦(∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦))
47	45, 46	syl 17	. . . . . . 7 ⊢ (𝑢 ≠ 𝑣 → (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦))
48		imbi1 351	. . . . . . . 8 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) ↔ (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)))
49	48	biimpar 481	. . . . . . 7 ⊢ (((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) ∧ (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦))
50	16, 47, 49	sylancr 590	. . . . . 6 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦))
51		pm3.34 765	. . . . . 6 ⊢ (((∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦) ∧ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
52	15, 50, 51	sylancr 590	. . . . 5 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦))
53		orc 864	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
54	53	imim2i 16	. . . . 5 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
55	52, 54	syl 17	. . . 4 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
56	55	idiALT 41183	. . 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 41183	. . 3 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
64		exmidne 2997	. . 3 ⊢ (𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣)
65		jao 958	. . . 4 ⊢ ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))))
66	65	3imp21 1111	. . 3 ⊢ (((𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) ∧ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) ∧ (𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣)) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
67	56, 63, 64, 66	mp3an 1458	. 2 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
68	8, 67	impbii 212	1 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844  ∀wal 1536   = wceq 1538  ∃wex 1781   ≠ wne 2987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-13 2379  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-v 3443

This theorem is referenced by: (None)