Metamath Proof Explorer

Theorem axpowg3

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

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

Proof

Step Hyp Ref Expression
1 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑤
2 nfv ⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑤
3 nfnae ⊢ Ⅎ 𝑤 ¬ ∀ 𝑥 𝑥 = 𝑤
4 nfcvf ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → Ⅎ 𝑥 𝑤 )
5 nfcvd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → Ⅎ 𝑥 𝑧 )
6 4 5 nfeld ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → Ⅎ 𝑥 𝑤 ∈ 𝑧 )
7 nfcvd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → Ⅎ 𝑥 𝑣 )
8 4 7 nfeld ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → Ⅎ 𝑥 𝑤 ∈ 𝑣 )
9 6 8 nfimd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → Ⅎ 𝑥 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) )
10 3 9 nfald ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → Ⅎ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) )
11 nfvd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → Ⅎ 𝑥 𝑧 ∈ 𝑦 )
12 10 11 nfimd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → Ⅎ 𝑥 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 ) )
13 2 12 nfald ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → Ⅎ 𝑥 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 ) )
14 1 13 nfexd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → Ⅎ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 ) )
15 nfvd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → Ⅎ 𝑣 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
16 dveeq2 ⊢ ( ¬ ∀ 𝑤 𝑤 = 𝑥 → ( 𝑣 = 𝑥 → ∀ 𝑤 𝑣 = 𝑥 ) )
17 16 naecoms ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → ( 𝑣 = 𝑥 → ∀ 𝑤 𝑣 = 𝑥 ) )
18 nfv ⊢ Ⅎ 𝑦 𝑣 = 𝑥
19 18 nfal ⊢ Ⅎ 𝑦 ∀ 𝑤 𝑣 = 𝑥
20 ax9v2 ⊢ ( 𝑥 = 𝑣 → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣 ) )
21 20 equcoms ⊢ ( 𝑣 = 𝑥 → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣 ) )
22 21 imim2d ⊢ ( 𝑣 = 𝑥 → ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) ) )
23 22 al2imi ⊢ ( ∀ 𝑤 𝑣 = 𝑥 → ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) ) )
24 23 imim1d ⊢ ( ∀ 𝑤 𝑣 = 𝑥 → ( ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 ) → ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
25 24 alimdv ⊢ ( ∀ 𝑤 𝑣 = 𝑥 → ( ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 ) → ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
26 19 25 eximd ⊢ ( ∀ 𝑤 𝑣 = 𝑥 → ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
27 17 26 syl6 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → ( 𝑣 = 𝑥 → ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) ) )
28 nfae ⊢ Ⅎ 𝑦 ∀ 𝑥 𝑥 = 𝑤
29 axc11r ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → ∀ 𝑥 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ) )
30 ax8 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝑧 → 𝑤 ∈ 𝑧 ) )
31 ax8 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥 ) )
32 31 equcoms ⊢ ( 𝑥 = 𝑤 → ( 𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥 ) )
33 30 32 imim12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) ) )
34 33 al2imi ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ∀ 𝑥 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) ) )
35 29 34 syld ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) ) )
36 35 imim1d ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) → ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
37 36 alimdv ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ∀ 𝑧 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) → ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
38 28 37 eximd ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
39 axpowg ⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 )
40 39 ax-gen ⊢ ∀ 𝑣 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 )
41 axprlem1 ⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦 )
42 elirrv ⊢ ¬ 𝑥 ∈ 𝑥
43 mtt ⊢ ( ¬ 𝑥 ∈ 𝑥 → ( ¬ 𝑥 ∈ 𝑧 ↔ ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) ) )
44 42 43 ax-mp ⊢ ( ¬ 𝑥 ∈ 𝑧 ↔ ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) )
45 44 biimpri ⊢ ( ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → ¬ 𝑥 ∈ 𝑧 )
46 45 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 )
47 46 imim1i ⊢ ( ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
48 47 alimi ⊢ ( ∀ 𝑧 ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦 ) → ∀ 𝑧 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
49 41 48 eximii ⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )
50 49 ax-gen ⊢ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )
51 14 15 27 38 40 50 dvelimalcasei ⊢ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )
52 51 spi ⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )