Metamath Proof Explorer

Theorem axpownd

Description: A version of 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) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axpowndlem4 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) )
2 axpowndlem1 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
3 2 aecoms ⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
4 2 a1d ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) )
5 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
6 nfae ⊢ Ⅎ 𝑦 ∀ 𝑦 𝑦 = 𝑧
7 5 6 nfan ⊢ Ⅎ 𝑦 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 )
8 el ⊢ ∃ 𝑤 𝑥 ∈ 𝑤
9 nfcvf2 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 )
10 nfcvd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑤 )
11 9 10 nfeld ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 ∈ 𝑤 )
12 elequ2 ⊢ ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) )
13 12 a1i ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) ) )
14 5 11 13 cbvexd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑤 𝑥 ∈ 𝑤 ↔ ∃ 𝑦 𝑥 ∈ 𝑦 ) )
15 8 14 mpbii ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑦 𝑥 ∈ 𝑦 )
16 15 19.8ad ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∃ 𝑦 𝑥 ∈ 𝑦 )
17 df-ex ⊢ ( ∃ 𝑥 ∃ 𝑦 𝑥 ∈ 𝑦 ↔ ¬ ∀ 𝑥 ¬ ∃ 𝑦 𝑥 ∈ 𝑦 )
18 16 17 sylib ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ¬ ∀ 𝑥 ¬ ∃ 𝑦 𝑥 ∈ 𝑦 )
19 18 adantr ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ¬ ∀ 𝑥 ¬ ∃ 𝑦 𝑥 ∈ 𝑦 )
20 biidd ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ 𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑦 ) )
21 20 dral1 ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑦 ¬ 𝑥 ∈ 𝑦 ↔ ∀ 𝑧 ¬ 𝑥 ∈ 𝑦 ) )
22 alnex ⊢ ( ∀ 𝑦 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑦 𝑥 ∈ 𝑦 )
23 alnex ⊢ ( ∀ 𝑧 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑧 𝑥 ∈ 𝑦 )
24 21 22 23 3bitr3g ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ ∃ 𝑦 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑧 𝑥 ∈ 𝑦 ) )
25 nd2 ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ¬ ∀ 𝑦 𝑥 ∈ 𝑧 )
26 mtt ⊢ ( ¬ ∀ 𝑦 𝑥 ∈ 𝑧 → ( ¬ ∃ 𝑧 𝑥 ∈ 𝑦 ↔ ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) )
27 25 26 syl ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ ∃ 𝑧 𝑥 ∈ 𝑦 ↔ ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) )
28 24 27 bitrd ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ ∃ 𝑦 𝑥 ∈ 𝑦 ↔ ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) )
29 28 dral2 ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 ¬ ∃ 𝑦 𝑥 ∈ 𝑦 ↔ ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) )
30 29 adantl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∀ 𝑥 ¬ ∃ 𝑦 𝑥 ∈ 𝑦 ↔ ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) )
31 19 30 mtbid ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ¬ ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) )
32 31 pm2.21d ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
33 7 32 alrimi ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
34 33 19.8ad ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
35 34 a1d ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
36 35 ex ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) )
37 4 36 pm2.61i ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
38 1 3 37 pm2.61ii ⊢ ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )