Theorem axpowg3 35789

Description: A generalization of ax-pow 5327 that combines axpowg 35787 and axpowg2 35788 into a single theorem scheme. Unlike ax-pow 5327, this scheme lacks a distinct variable condition for 𝑦 and 𝑤 as well as for 𝑥 and 𝑤. Usage of this theorem is discouraged because it depends on ax-13 2402. (Contributed by BTernaryTau, 26-May-2026.) (New usage is discouraged.)

Assertion

Ref	Expression
axpowg3	⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

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

Proof of Theorem axpowg3

Dummy variable 𝑣 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfnae 2464	. . . 4 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑤
2		nfv 1947	. . . . 5 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑤
3		nfnae 2464	. . . . . . 7 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑤
4		nfcvf 2949	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑤)
5		nfcvd 2924	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑧)
6	4, 5	nfeld 2934	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥 𝑤 ∈ 𝑧)
7		nfcvd 2924	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑣)
8	4, 7	nfeld 2934	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥 𝑤 ∈ 𝑣)
9	6, 8	nfimd 1927	. . . . . . 7 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣))
10	3, 9	nfald 2359	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣))
11		nfvd 1948	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥 𝑧 ∈ 𝑦)
12	10, 11	nfimd 1927	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦))
13	2, 12	nfald 2359	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦))
14	1, 13	nfexd 2360	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦))
15		nfvd 1948	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑣∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
16		dveeq2 2408	. . . . 5 ⊢ (¬ ∀𝑤 𝑤 = 𝑥 → (𝑣 = 𝑥 → ∀𝑤 𝑣 = 𝑥))
17	16	naecoms 2459	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑣 = 𝑥 → ∀𝑤 𝑣 = 𝑥))
18		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑦 𝑣 = 𝑥
19	18	nfal 2354	. . . . 5 ⊢ Ⅎ𝑦∀𝑤 𝑣 = 𝑥
20		ax9v2 2158	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣))
21	20	equcoms 2053	. . . . . . . . 9 ⊢ (𝑣 = 𝑥 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣))
22	21	imim2d 58	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣)))
23	22	al2imi 1848	. . . . . . 7 ⊢ (∀𝑤 𝑣 = 𝑥 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣)))
24	23	imim1d 83	. . . . . 6 ⊢ (∀𝑤 𝑣 = 𝑥 → ((∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
25	24	alimdv 1949	. . . . 5 ⊢ (∀𝑤 𝑣 = 𝑥 → (∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
26	19, 25	eximd 2253	. . . 4 ⊢ (∀𝑤 𝑣 = 𝑥 → (∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
27	17, 26	syl6 36	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑣 = 𝑥 → (∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))))
28		nfae 2463	. . . 4 ⊢ Ⅎ𝑦∀𝑥 𝑥 = 𝑤
29		axc11r 2398	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)))
30		ax8 2151	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝑧 → 𝑤 ∈ 𝑧))
31		ax8 2151	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥))
32	31	equcoms 2053	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥))
33	30, 32	imim12d 82	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
34	33	al2imi 1848	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
35	29, 34	syld 48	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
36	35	imim1d 83	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑤 → ((∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
37	36	alimdv 1949	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
38	28, 37	eximd 2253	. . 3 ⊢ (∀𝑥 𝑥 = 𝑤 → (∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
39		axpowg 35787	. . . 4 ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦)
40	39	ax-gen 1828	. . 3 ⊢ ∀𝑣∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦)
41		axprlem1 5385	. . . . 5 ⊢ ∃𝑦∀𝑧(∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦)
42		elirrv 9575	. . . . . . . . . 10 ⊢ ¬ 𝑥 ∈ 𝑥
43		mtt 367	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝑥 → (¬ 𝑥 ∈ 𝑧 ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
44	42, 43	ax-mp 5	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝑧 ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥))
45	44	biimpri 231	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → ¬ 𝑥 ∈ 𝑧)
46	45	alimi 1844	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → ∀𝑥 ¬ 𝑥 ∈ 𝑧)
47	46	imim1i 64	. . . . . 6 ⊢ ((∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦) → (∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦))
48	47	alimi 1844	. . . . 5 ⊢ (∀𝑧(∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦))
49	41, 48	eximii 1870	. . . 4 ⊢ ∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦)
50	49	ax-gen 1828	. . 3 ⊢ ∀𝑥∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦)
51	14, 15, 27, 38, 40, 50	dvelimalcasei 35689	. 2 ⊢ ∀𝑥∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
52	51	spi 2221	1 ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-13 2402  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-reg 9570

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-cleq 2753  df-clel 2836  df-nfc 2910

This theorem is used by: (None)