Theorem ax12indalem 36096

Description: Lemma for ax12inda2 36098 and ax12inda 36099. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
ax12indalem.1	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))

Assertion

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

Proof of Theorem ax12indalem

Step	Hyp	Ref	Expression
1		ax-1 6	. . . . . . . . 9 ⊢ (∀𝑥𝜑 → (𝑥 = 𝑦 → ∀𝑥𝜑))
2	1	axc4i-o 36049	. . . . . . . 8 ⊢ (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑))
3	2	a1i 11	. . . . . . 7 ⊢ (∀𝑧 𝑧 = 𝑥 → (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)))
4		biidd 264	. . . . . . . 8 ⊢ (∀𝑧 𝑧 = 𝑥 → (𝜑 ↔ 𝜑))
5	4	dral1-o 36055	. . . . . . 7 ⊢ (∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 ↔ ∀𝑥𝜑))
6	5	imbi2d 343	. . . . . . . 8 ⊢ (∀𝑧 𝑧 = 𝑥 → ((𝑥 = 𝑦 → ∀𝑧𝜑) ↔ (𝑥 = 𝑦 → ∀𝑥𝜑)))
7	6	dral2-o 36081	. . . . . . 7 ⊢ (∀𝑧 𝑧 = 𝑥 → (∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)))
8	3, 5, 7	3imtr4d 296	. . . . . 6 ⊢ (∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
9	8	aecoms-o 36053	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
10	9	a1d 25	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
11	10	a1d 25	. . 3 ⊢ (∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
12	11	adantr 483	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
13		simplr 767	. . . . 5 ⊢ ((((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ¬ ∀𝑥 𝑥 = 𝑦)
14		aecom-o 36052	. . . . . . . . 9 ⊢ (∀𝑧 𝑧 = 𝑥 → ∀𝑥 𝑥 = 𝑧)
15	14	con3i 157	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ¬ ∀𝑧 𝑧 = 𝑥)
16		aecom-o 36052	. . . . . . . . 9 ⊢ (∀𝑧 𝑧 = 𝑦 → ∀𝑦 𝑦 = 𝑧)
17	16	con3i 157	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ¬ ∀𝑧 𝑧 = 𝑦)
18		axc9 2400	. . . . . . . . 9 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
19	18	imp 409	. . . . . . . 8 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
20	15, 17, 19	syl2an 597	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
21	20	imp 409	. . . . . 6 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦)
22	21	adantlr 713	. . . . 5 ⊢ ((((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦)
23		hbnae-o 36079	. . . . . . 7 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
24		hba1-o 36048	. . . . . . 7 ⊢ (∀𝑧 𝑥 = 𝑦 → ∀𝑧∀𝑧 𝑥 = 𝑦)
25	23, 24	hban 2308	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → ∀𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦))
26		ax-c5 36034	. . . . . . 7 ⊢ (∀𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦)
27		ax12indalem.1	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
28	27	imp 409	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
29	26, 28	sylan2 594	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
30	25, 29	alimdh 1818	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑)))
31	13, 22, 30	syl2anc 586	. . . 4 ⊢ ((((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑)))
32		ax-11 2161	. . . . . 6 ⊢ (∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥∀𝑧(𝑥 = 𝑦 → 𝜑))
33		hbnae-o 36079	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑧)
34		hbnae-o 36079	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ∀𝑥 ¬ ∀𝑦 𝑦 = 𝑧)
35	33, 34	hban 2308	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∀𝑥(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧))
36		hbnae-o 36079	. . . . . . . . . 10 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑧)
37		hbnae-o 36079	. . . . . . . . . 10 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧)
38	36, 37	hban 2308	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∀𝑧(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧))
39	38, 20	nf5dh 2151	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑧 𝑥 = 𝑦)
40		19.21t 2206	. . . . . . . 8 ⊢ (Ⅎ𝑧 𝑥 = 𝑦 → (∀𝑧(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
41	39, 40	syl 17	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑧(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
42	35, 41	albidh 1867	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑥∀𝑧(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
43	32, 42	syl5ib 246	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
44	43	ad2antrr 724	. . . 4 ⊢ ((((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
45	31, 44	syld 47	. . 3 ⊢ ((((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
46	45	exp31 422	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
47	12, 46	pm2.61ian 810	1 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2145  ax-11 2161  ax-12 2177  ax-13 2390  ax-c5 36034  ax-c4 36035  ax-c7 36036  ax-c10 36037  ax-c11 36038  ax-c9 36041

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785

This theorem is referenced by:  ax12inda2  36098