Theorem ax12inda 36699

Description: Induction step for constructing a substitution instance of ax-c15 36640 without using ax-c15 36640. Quantification case. (When 𝑧 and 𝑦 are distinct, ax12inda2 36698 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 1978	. . 3 ⊢ ∃𝑤 𝑤 = 𝑦
2		ax12inda.1	. . . . . . 7 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑥 = 𝑤 → (𝜑 → ∀𝑥(𝑥 = 𝑤 → 𝜑))))
3	2	ax12inda2 36698	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑥 = 𝑤 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑤 → ∀𝑧𝜑))))
4		dveeq2-o 36684	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
5	4	imp 410	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → ∀𝑥 𝑤 = 𝑦)
6		hba1-o 36648	. . . . . . . . . 10 ⊢ (∀𝑥 𝑤 = 𝑦 → ∀𝑥∀𝑥 𝑤 = 𝑦)
7		equequ2 2034	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑦 → (𝑥 = 𝑤 ↔ 𝑥 = 𝑦))
8	7	sps-o 36659	. . . . . . . . . 10 ⊢ (∀𝑥 𝑤 = 𝑦 → (𝑥 = 𝑤 ↔ 𝑥 = 𝑦))
9	6, 8	albidh 1874	. . . . . . . . 9 ⊢ (∀𝑥 𝑤 = 𝑦 → (∀𝑥 𝑥 = 𝑤 ↔ ∀𝑥 𝑥 = 𝑦))
10	9	notbid 321	. . . . . . . 8 ⊢ (∀𝑥 𝑤 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 ↔ ¬ ∀𝑥 𝑥 = 𝑦))
11	5, 10	syl 17	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (¬ ∀𝑥 𝑥 = 𝑤 ↔ ¬ ∀𝑥 𝑥 = 𝑦))
12	7	adantl 485	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (𝑥 = 𝑤 ↔ 𝑥 = 𝑦))
13	8	imbi1d 345	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑤 = 𝑦 → ((𝑥 = 𝑤 → ∀𝑧𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
14	6, 13	albidh 1874	. . . . . . . . . 10 ⊢ (∀𝑥 𝑤 = 𝑦 → (∀𝑥(𝑥 = 𝑤 → ∀𝑧𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
15	5, 14	syl 17	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (∀𝑥(𝑥 = 𝑤 → ∀𝑧𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
16	15	imbi2d 344	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → ((∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑤 → ∀𝑧𝜑)) ↔ (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
17	12, 16	imbi12d 348	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → ((𝑥 = 𝑤 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑤 → ∀𝑧𝜑))) ↔ (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
18	11, 17	imbi12d 348	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → ((¬ ∀𝑥 𝑥 = 𝑤 → (𝑥 = 𝑤 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑤 → ∀𝑧𝜑)))) ↔ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))))
19	3, 18	mpbii 236	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
20	19	ex 416	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑤 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))))
21	20	exlimdv 1941	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑤 𝑤 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))))
22	1, 21	mpi 20	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
23	22	pm2.43i 52	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1541  ∃wex 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-10 2141  ax-11 2158  ax-12 2175  ax-13 2371  ax-c5 36634  ax-c4 36635  ax-c7 36636  ax-c10 36637  ax-c11 36638  ax-c9 36641  ax-c16 36643

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792

This theorem is referenced by: (None)