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