Metamath Proof Explorer

Theorem axpowndlem2

Description: Lemma for the Axiom of Power Sets with no distinct variable conditions. Revised to remove a redundant antecedent from the consequence. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 4-Jan-2002) (Proof shortened by Mario Carneiro, 6-Dec-2016) (Revised and shortened by Wolf Lammen, 9-Jun-2019.) (New usage is discouraged.)

Ref Expression
Assertion axpowndlem2 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 zfpow ⊢ ∃ 𝑤 ∀ 𝑦 ( ∀ 𝑤 ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 )
2 19.8a ⊢ ( 𝑤 ∈ 𝑦 → ∃ 𝑧 𝑤 ∈ 𝑦 )
3 sp ⊢ ( ∀ 𝑦 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑧 )
4 2 3 imim12i ⊢ ( ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑧 ) )
5 4 alimi ⊢ ( ∀ 𝑤 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑧 ) )
6 5 imim1i ⊢ ( ( ∀ 𝑤 ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) → ( ∀ 𝑤 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) )
7 6 alimi ⊢ ( ∀ 𝑦 ( ∀ 𝑤 ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) → ∀ 𝑦 ( ∀ 𝑤 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) )
8 1 7 eximii ⊢ ∃ 𝑤 ∀ 𝑦 ( ∀ 𝑤 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 )
9 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
10 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑧
11 9 10 nfan ⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
12 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
13 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑧
14 12 13 nfan ⊢ Ⅎ 𝑦 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
15 nfv ⊢ Ⅎ 𝑤 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
16 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦
17 nfcvd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑤 )
18 nfcvf ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 )
19 17 18 nfeld ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑤 ∈ 𝑦 )
20 16 19 nfexd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ∃ 𝑧 𝑤 ∈ 𝑦 )
21 20 adantr ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ∃ 𝑧 𝑤 ∈ 𝑦 )
22 nfcvd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑥 𝑤 )
23 nfcvf ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑥 𝑧 )
24 22 23 nfeld ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑥 𝑤 ∈ 𝑧 )
25 13 24 nfald ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑥 ∀ 𝑦 𝑤 ∈ 𝑧 )
26 25 adantl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ∀ 𝑦 𝑤 ∈ 𝑧 )
27 21 26 nfimd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) )
28 15 27 nfald ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ∀ 𝑤 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) )
29 18 17 nfeld ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 ∈ 𝑤 )
30 29 adantr ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑦 ∈ 𝑤 )
31 28 30 nfimd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( ∀ 𝑤 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) )
32 14 31 nfald ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ∀ 𝑦 ( ∀ 𝑤 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) )
33 nfeqf2 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 𝑤 = 𝑥 )
34 33 naecoms ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑤 = 𝑥 )
35 34 adantr ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑦 𝑤 = 𝑥 )
36 14 35 nfan1 ⊢ Ⅎ 𝑦 ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 )
37 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑧
38 nfeqf2 ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 𝑤 = 𝑥 )
39 38 naecoms ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑧 𝑤 = 𝑥 )
40 37 39 nfan1 ⊢ Ⅎ 𝑧 ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ 𝑤 = 𝑥 )
41 elequ1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
42 41 adantl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ 𝑤 = 𝑥 ) → ( 𝑤 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
43 40 42 exbid ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ 𝑤 = 𝑥 ) → ( ∃ 𝑧 𝑤 ∈ 𝑦 ↔ ∃ 𝑧 𝑥 ∈ 𝑦 ) )
44 43 adantll ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ∃ 𝑧 𝑤 ∈ 𝑦 ↔ ∃ 𝑧 𝑥 ∈ 𝑦 ) )
45 12 34 nfan1 ⊢ Ⅎ 𝑦 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑥 )
46 elequ1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧 ) )
47 46 adantl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( 𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧 ) )
48 45 47 albid ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( ∀ 𝑦 𝑤 ∈ 𝑧 ↔ ∀ 𝑦 𝑥 ∈ 𝑧 ) )
49 48 adantlr ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ∀ 𝑦 𝑤 ∈ 𝑧 ↔ ∀ 𝑦 𝑥 ∈ 𝑧 ) )
50 44 49 imbi12d ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) ↔ ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) )
51 50 ex ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( 𝑤 = 𝑥 → ( ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) ↔ ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) ) )
52 11 27 51 cbvald ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∀ 𝑤 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) )
53 52 adantr ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ∀ 𝑤 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) )
54 elequ2 ⊢ ( 𝑤 = 𝑥 → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥 ) )
55 54 adantl ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥 ) )
56 53 55 imbi12d ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ( ∀ 𝑤 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) ↔ ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
57 36 56 albid ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ∀ 𝑦 ( ∀ 𝑤 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) ↔ ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
58 57 ex ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( 𝑤 = 𝑥 → ( ∀ 𝑦 ( ∀ 𝑤 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) ↔ ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) )
59 11 32 58 cbvexd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∃ 𝑤 ∀ 𝑦 ( ∀ 𝑤 ( ∃ 𝑧 𝑤 ∈ 𝑦 → ∀ 𝑦 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) ↔ ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
60 8 59 mpbii ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
61 60 ex ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )