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 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥𝑦 → ∀ 𝑦 𝑥𝑧 ) → 𝑦𝑥 ) ) )