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

Metamath Proof Explorer

Theorem axpowndlem3

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) (Revised by Mario Carneiro, 10-Dec-2016) (Proof shortened by Wolf Lammen, 10-Jun-2019) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 sp ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 )
2 p0ex ⊢ { ∅ } ∈ V
3 eleq2 ⊢ ( 𝑥 = { ∅ } → ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ { ∅ } ) )
4 3 imbi2d ⊢ ( 𝑥 = { ∅ } → ( ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 ) ↔ ( 𝑤 = ∅ → 𝑤 ∈ { ∅ } ) ) )
5 4 albidv ⊢ ( 𝑥 = { ∅ } → ( ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 ) ↔ ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ { ∅ } ) ) )
6 2 5 spcev ⊢ ( ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ { ∅ } ) → ∃ 𝑥 ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 ) )
7 0ex ⊢ ∅ ∈ V
8 7 snid ⊢ ∅ ∈ { ∅ }
9 eleq1 ⊢ ( 𝑤 = ∅ → ( 𝑤 ∈ { ∅ } ↔ ∅ ∈ { ∅ } ) )
10 8 9 mpbiri ⊢ ( 𝑤 = ∅ → 𝑤 ∈ { ∅ } )
11 6 10 mpg ⊢ ∃ 𝑥 ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 )
12 neq0 ⊢ ( ¬ 𝑤 = ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑤 )
13 12 con1bii ⊢ ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 ↔ 𝑤 = ∅ )
14 13 imbi1i ⊢ ( ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 ) )
15 14 albii ⊢ ( ∀ 𝑤 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 ) )
16 15 exbii ⊢ ( ∃ 𝑥 ∀ 𝑤 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ∃ 𝑥 ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 ) )
17 11 16 mpbir ⊢ ∃ 𝑥 ∀ 𝑤 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 )
18 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
19 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
20 nfcvf2 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 )
21 nfcvd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑤 )
22 20 21 nfeld ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 ∈ 𝑤 )
23 18 22 nfexd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ∃ 𝑥 𝑥 ∈ 𝑤 )
24 23 nfnd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ¬ ∃ 𝑥 𝑥 ∈ 𝑤 )
25 21 20 nfeld ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑤 ∈ 𝑥 )
26 24 25 nfimd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) )
27 nfeqf2 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑤 = 𝑦 )
28 18 27 nfan1 ⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 )
29 elequ2 ⊢ ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) )
30 29 adantl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) )
31 28 30 exbid ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( ∃ 𝑥 𝑥 ∈ 𝑤 ↔ ∃ 𝑥 𝑥 ∈ 𝑦 ) )
32 31 notbid ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 ↔ ¬ ∃ 𝑥 𝑥 ∈ 𝑦 ) )
33 elequ1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
34 33 adantl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( 𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
35 32 34 imbi12d ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) ) )
36 35 ex ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑤 = 𝑦 → ( ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) ) ) )
37 19 26 36 cbvald ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑤 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) ) )
38 18 37 exbid ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∀ 𝑤 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ∃ 𝑥 ∀ 𝑦 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) ) )
39 17 38 mpbii ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) )
40 nfae ⊢ Ⅎ 𝑥 ∀ 𝑥 𝑥 = 𝑧
41 nfae ⊢ Ⅎ 𝑦 ∀ 𝑥 𝑥 = 𝑧
42 axc11r ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑧 ¬ 𝑥 ∈ 𝑦 → ∀ 𝑥 ¬ 𝑥 ∈ 𝑦 ) )
43 alnex ⊢ ( ∀ 𝑧 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑧 𝑥 ∈ 𝑦 )
44 alnex ⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑥 𝑥 ∈ 𝑦 )
45 42 43 44 3imtr3g ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∃ 𝑧 𝑥 ∈ 𝑦 → ¬ ∃ 𝑥 𝑥 ∈ 𝑦 ) )
46 nd3 ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ¬ ∀ 𝑦 𝑥 ∈ 𝑧 )
47 46 pm2.21d ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑦 𝑥 ∈ 𝑧 → ¬ ∃ 𝑥 𝑥 ∈ 𝑦 ) )
48 45 47 jad ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → ¬ ∃ 𝑥 𝑥 ∈ 𝑦 ) )
49 48 spsd ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → ¬ ∃ 𝑥 𝑥 ∈ 𝑦 ) )
50 49 imim1d ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) → ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
51 41 50 alimd ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑦 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) → ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
52 40 51 eximd ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∃ 𝑥 ∀ 𝑦 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
53 39 52 syl5com ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
54 axpowndlem2 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
55 53 54 pm2.61d ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
56 1 55 nsyl5 ⊢ ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )