This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axpowndlem4

Description: Lemma for the Axiom of Power Sets with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 4-Jan-2002) (Proof shortened by Mario Carneiro, 10-Dec-2016) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axpowndlem3 ⊢ ( ¬ 𝑥 = 𝑤 → ∃ 𝑥 ∀ 𝑤 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) )
2 1 ax-gen ⊢ ∀ 𝑤 ( ¬ 𝑥 = 𝑤 → ∃ 𝑥 ∀ 𝑤 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) )
3 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑦 𝑦 = 𝑥
4 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑦 𝑦 = 𝑧
5 3 4 nfan ⊢ Ⅎ 𝑦 ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 )
6 nfcvf ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 𝑥 )
7 6 adantr ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 𝑥 )
8 nfcvd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 𝑤 )
9 7 8 nfeqd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 𝑥 = 𝑤 )
10 9 nfnd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 ¬ 𝑥 = 𝑤 )
11 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑥
12 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑧
13 11 12 nfan ⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 )
14 nfv ⊢ Ⅎ 𝑤 ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 )
15 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑦 𝑦 = 𝑥
16 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑦 𝑦 = 𝑧
17 15 16 nfan ⊢ Ⅎ 𝑧 ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 )
18 7 8 nfeld ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 𝑥 ∈ 𝑤 )
19 17 18 nfexd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 ∃ 𝑧 𝑥 ∈ 𝑤 )
20 nfcvf ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 𝑧 )
21 20 adantl ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 𝑧 )
22 7 21 nfeld ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 𝑥 ∈ 𝑧 )
23 14 22 nfald ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 ∀ 𝑤 𝑥 ∈ 𝑧 )
24 19 23 nfimd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) )
25 13 24 nfald ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) )
26 8 7 nfeld ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 𝑤 ∈ 𝑥 )
27 25 26 nfimd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) )
28 14 27 nfald ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 ∀ 𝑤 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) )
29 13 28 nfexd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 ∃ 𝑥 ∀ 𝑤 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) )
30 10 29 nfimd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 ( ¬ 𝑥 = 𝑤 → ∃ 𝑥 ∀ 𝑤 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) ) )
31 equequ2 ⊢ ( 𝑤 = 𝑦 → ( 𝑥 = 𝑤 ↔ 𝑥 = 𝑦 ) )
32 31 notbid ⊢ ( 𝑤 = 𝑦 → ( ¬ 𝑥 = 𝑤 ↔ ¬ 𝑥 = 𝑦 ) )
33 32 adantl ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ( ¬ 𝑥 = 𝑤 ↔ ¬ 𝑥 = 𝑦 ) )
34 nfcvd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑥 𝑤 )
35 nfcvf2 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑥 𝑦 )
36 35 adantr ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑥 𝑦 )
37 34 36 nfeqd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑥 𝑤 = 𝑦 )
38 13 37 nfan1 ⊢ Ⅎ 𝑥 ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 )
39 nfcvd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑧 𝑤 )
40 nfcvf2 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 𝑦 )
41 40 adantl ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑧 𝑦 )
42 39 41 nfeqd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑧 𝑤 = 𝑦 )
43 17 42 nfan1 ⊢ Ⅎ 𝑧 ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 )
44 elequ2 ⊢ ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) )
45 44 adantl ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) )
46 43 45 exbid ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ( ∃ 𝑧 𝑥 ∈ 𝑤 ↔ ∃ 𝑧 𝑥 ∈ 𝑦 ) )
47 biidd ⊢ ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧 ) )
48 47 a1i ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧 ) ) )
49 5 22 48 cbvald ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∀ 𝑤 𝑥 ∈ 𝑧 ↔ ∀ 𝑦 𝑥 ∈ 𝑧 ) )
50 49 adantr ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ( ∀ 𝑤 𝑥 ∈ 𝑧 ↔ ∀ 𝑦 𝑥 ∈ 𝑧 ) )
51 46 50 imbi12d ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ( ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) ↔ ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) )
52 38 51 albid ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) ↔ ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) )
53 elequ1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
54 53 adantl ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ( 𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
55 52 54 imbi12d ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ( ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) ↔ ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
56 55 ex ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( 𝑤 = 𝑦 → ( ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) ↔ ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) )
57 5 27 56 cbvald ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∀ 𝑤 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
58 13 57 exbid ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∃ 𝑥 ∀ 𝑤 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) ↔ ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
59 58 adantr ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ( ∃ 𝑥 ∀ 𝑤 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) ↔ ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
60 33 59 imbi12d ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ∧ 𝑤 = 𝑦 ) → ( ( ¬ 𝑥 = 𝑤 → ∃ 𝑥 ∀ 𝑤 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) ) ↔ ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) )
61 60 ex ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( 𝑤 = 𝑦 → ( ( ¬ 𝑥 = 𝑤 → ∃ 𝑥 ∀ 𝑤 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) ) ↔ ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) ) )
62 5 30 61 cbvald ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∀ 𝑤 ( ¬ 𝑥 = 𝑤 → ∃ 𝑥 ∀ 𝑤 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑤 → ∀ 𝑤 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) ) ↔ ∀ 𝑦 ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) )
63 2 62 mpbii ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ∀ 𝑦 ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
64 63 19.21bi ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
65 64 ex ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) )