Theorem ax12inda 39532

Description: Induction step for constructing a substitution instance of ax-c15 39473 without using ax-c15 39473. Quantification case. (When 𝑧 and 𝑦 are distinct, ax12inda2 39531 may be used instead to avoid the dummy variable 𝑤 in the proof.) (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
ax12inda.1	⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑥 = 𝑤 → (𝜑 → ∀𝑥(𝑥 = 𝑤 → 𝜑))))

Assertion

Ref	Expression
ax12inda	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))

Distinct variable groups:   𝜑,𝑤   𝑥,𝑤   𝑦,𝑤   𝑧,𝑤

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

Proof of Theorem ax12inda

Step	Hyp	Ref	Expression
1		ax6ev 1988	. . 3 ⊢ ∃𝑤 𝑤 = 𝑦
2		ax12inda.1	. . . . . . 7 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑥 = 𝑤 → (𝜑 → ∀𝑥(𝑥 = 𝑤 → 𝜑))))
3	2	ax12inda2 39531	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑥 = 𝑤 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑤 → ∀𝑧𝜑))))
4		dveeq2-o 39517	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
5	4	imp 410	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → ∀𝑥 𝑤 = 𝑦)
6		hba1-o 39481	. . . . . . . . . 10 ⊢ (∀𝑥 𝑤 = 𝑦 → ∀𝑥∀𝑥 𝑤 = 𝑦)
7		equequ2 2045	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑦 → (𝑥 = 𝑤 ↔ 𝑥 = 𝑦))
8	7	sps-o 39492	. . . . . . . . . 10 ⊢ (∀𝑥 𝑤 = 𝑦 → (𝑥 = 𝑤 ↔ 𝑥 = 𝑦))
9	6, 8	albidh 1885	. . . . . . . . 9 ⊢ (∀𝑥 𝑤 = 𝑦 → (∀𝑥 𝑥 = 𝑤 ↔ ∀𝑥 𝑥 = 𝑦))
10	9	notbid 320	. . . . . . . 8 ⊢ (∀𝑥 𝑤 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 ↔ ¬ ∀𝑥 𝑥 = 𝑦))
11	5, 10	syl 17	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (¬ ∀𝑥 𝑥 = 𝑤 ↔ ¬ ∀𝑥 𝑥 = 𝑦))
12	7	adantl 485	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (𝑥 = 𝑤 ↔ 𝑥 = 𝑦))
13	8	imbi1d 343	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑤 = 𝑦 → ((𝑥 = 𝑤 → ∀𝑧𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
14	6, 13	albidh 1885	. . . . . . . . . 10 ⊢ (∀𝑥 𝑤 = 𝑦 → (∀𝑥(𝑥 = 𝑤 → ∀𝑧𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
15	5, 14	syl 17	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (∀𝑥(𝑥 = 𝑤 → ∀𝑧𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
16	15	imbi2d 342	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → ((∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑤 → ∀𝑧𝜑)) ↔ (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
17	12, 16	imbi12d 346	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → ((𝑥 = 𝑤 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑤 → ∀𝑧𝜑))) ↔ (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
18	11, 17	imbi12d 346	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → ((¬ ∀𝑥 𝑥 = 𝑤 → (𝑥 = 𝑤 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑤 → ∀𝑧𝜑)))) ↔ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))))
19	3, 18	mpbii 235	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
20	19	ex 416	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑤 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))))
21	20	exlimdv 1952	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑤 𝑤 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))))
22	1, 21	mpi 20	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
23	22	pm2.43i 52	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1557  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-10 2174  ax-11 2190  ax-12 2211  ax-13 2402  ax-c5 39467  ax-c4 39468  ax-c7 39469  ax-c10 39470  ax-c11 39471  ax-c9 39474  ax-c16 39476

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-nf 1803

This theorem is referenced by: (None)