Theorem dvelimALT 2029

Description: Version of dvelim 2036 that doesn't use ax-10 1519. Because it has different distinct variable constraints than dvelim 2036 and is used in important proofs, it would be better if it had a name which does not end in ALT (ideally more close to set.mm naming). (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
dvelimALT.1	⊢ (𝜑 → ∀𝑥𝜑)
dvelimALT.2	⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
dvelimALT	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))

Distinct variable groups:   𝜓,𝑧   𝑥,𝑧   𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝜓(𝑥,𝑦)

Proof of Theorem dvelimALT

Step	Hyp	Ref	Expression
1		nfv 1542	. . . 4 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
2		ax12or 1522	. . . . . . . . 9 ⊢ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)))
3		orcom 729	. . . . . . . . . 10 ⊢ ((∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ↔ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦))
4	3	orbi2i 763	. . . . . . . . 9 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))) ↔ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦)))
5	2, 4	mpbi 145	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦))
6		orass 768	. . . . . . . 8 ⊢ (((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦) ↔ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦)))
7	5, 6	mpbir 146	. . . . . . 7 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦)
8		nfa1 1555	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 𝑥 = 𝑧
9		ax16ALT 1873	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑧 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
10	8, 9	nfd 1537	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑧 = 𝑦)
11		dvelimALT.1	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥𝜑)
12	11	nfi 1476	. . . . . . . . . . 11 ⊢ Ⅎ𝑥𝜑
13	12	a1i 9	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝜑)
14	10, 13	nfimd 1599	. . . . . . . . 9 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
15		df-nf 1475	. . . . . . . . . 10 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 ↔ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
16		id 19	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
17	12	a1i 9	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥𝜑)
18	16, 17	nfimd 1599	. . . . . . . . . 10 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
19	15, 18	sylbir 135	. . . . . . . . 9 ⊢ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
20	14, 19	jaoi 717	. . . . . . . 8 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
21	20	orim1i 761	. . . . . . 7 ⊢ (((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦) → (Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦))
22	7, 21	ax-mp 5	. . . . . 6 ⊢ (Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦)
23		orcom 729	. . . . . 6 ⊢ ((Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦) ↔ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥(𝑧 = 𝑦 → 𝜑)))
24	22, 23	mpbi 145	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
25	24	ori 724	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
26	1, 25	nfald 1774	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜑))
27		ax-17 1540	. . . . 5 ⊢ (𝜓 → ∀𝑧𝜓)
28		dvelimALT.2	. . . . 5 ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))
29	27, 28	equsalh 1740	. . . 4 ⊢ (∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ 𝜓)
30	29	nfbii 1487	. . 3 ⊢ (Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ Ⅎ𝑥𝜓)
31	26, 30	sylib 122	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)
32	31	nfrd 1534	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105   ∨ wo 709  ∀wal 1362  Ⅎwnf 1474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-i12 1521  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777

This theorem is referenced by:  hbsb4  2031