Metamath Proof Explorer

Theorem axpowg2

Description: A generalization of ax-pow in which x and w need not be distinct. This theorem scheme bundles ax-pow with the degenerate instance E. y A. z ( A. x ( x e. z -> x e. x ) -> z e. y ) which is satisfied by the existence of a set that contains all empty sets (see axprlem1 ). 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 axpowg2 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑤
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 ax9v2 ⊢ ( 𝑥 = 𝑣 → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣 ) )
19 18 equcoms ⊢ ( 𝑣 = 𝑥 → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣 ) )
20 19 imim2d ⊢ ( 𝑣 = 𝑥 → ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) ) )
21 20 al2imi ⊢ ( ∀ 𝑤 𝑣 = 𝑥 → ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) ) )
22 21 imim1d ⊢ ( ∀ 𝑤 𝑣 = 𝑥 → ( ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 ) → ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
23 22 alimdv ⊢ ( ∀ 𝑤 𝑣 = 𝑥 → ( ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 ) → ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
24 23 eximdv ⊢ ( ∀ 𝑤 𝑣 = 𝑥 → ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
25 17 24 syl6 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → ( 𝑣 = 𝑥 → ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) ) )
26 axc11r ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → ∀ 𝑥 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ) )
27 ax8 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝑧 → 𝑤 ∈ 𝑧 ) )
28 ax8 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥 ) )
29 28 equcoms ⊢ ( 𝑥 = 𝑤 → ( 𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥 ) )
30 27 29 imim12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) ) )
31 30 al2imi ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ∀ 𝑥 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) ) )
32 26 31 syld ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) ) )
33 32 imim1d ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) → ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
34 33 alimdv ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ∀ 𝑧 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) → ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
35 34 eximdv ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
36 ax-pow ⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 )
37 36 ax-gen ⊢ ∀ 𝑣 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣 ) → 𝑧 ∈ 𝑦 )
38 axprlem1 ⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦 )
39 elirrv ⊢ ¬ 𝑥 ∈ 𝑥
40 mtt ⊢ ( ¬ 𝑥 ∈ 𝑥 → ( ¬ 𝑥 ∈ 𝑧 ↔ ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) ) )
41 39 40 ax-mp ⊢ ( ¬ 𝑥 ∈ 𝑧 ↔ ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) )
42 41 biimpri ⊢ ( ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → ¬ 𝑥 ∈ 𝑧 )
43 42 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 )
44 43 imim1i ⊢ ( ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
45 44 alimi ⊢ ( ∀ 𝑧 ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦 ) → ∀ 𝑧 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
46 38 45 eximii ⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )
47 46 ax-gen ⊢ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )
48 14 15 25 35 37 47 dvelimalcasei ⊢ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )
49 48 spi ⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )