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

Metamath Proof Explorer

Theorem dtruALT2

Description: Alternate proof of dtru using ax-pow instead of ax-pr . See dtruALT for another proof using ax-pow instead of ax-pr . (Contributed by NM, 7-Nov-2006) Avoid ax-13 . (Revised by BJ, 31-May-2019) Avoid ax-12 . (Revised by Rohan Ridenour, 9-Oct-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dtruALT2 ¬ ∀ 𝑥 𝑥 = 𝑦

Proof

Step Hyp Ref Expression
1 elALT2 ⊢ ∃ 𝑤 𝑥 ∈ 𝑤
2 ax-nul ⊢ ∃ 𝑧 ∀ 𝑥 ¬ 𝑥 ∈ 𝑧
3 elequ1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝑧 ↔ 𝑤 ∈ 𝑧 ) )
4 3 notbid ⊢ ( 𝑥 = 𝑤 → ( ¬ 𝑥 ∈ 𝑧 ↔ ¬ 𝑤 ∈ 𝑧 ) )
5 4 spw ⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧 )
6 2 5 eximii ⊢ ∃ 𝑧 ¬ 𝑥 ∈ 𝑧
7 exdistrv ⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) ↔ ( ∃ 𝑤 𝑥 ∈ 𝑤 ∧ ∃ 𝑧 ¬ 𝑥 ∈ 𝑧 ) )
8 1 6 7 mpbir2an ⊢ ∃ 𝑤 ∃ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 )
9 ax9v2 ⊢ ( 𝑤 = 𝑧 → ( 𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧 ) )
10 9 com12 ⊢ ( 𝑥 ∈ 𝑤 → ( 𝑤 = 𝑧 → 𝑥 ∈ 𝑧 ) )
11 10 con3dimp ⊢ ( ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) → ¬ 𝑤 = 𝑧 )
12 11 2eximi ⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) → ∃ 𝑤 ∃ 𝑧 ¬ 𝑤 = 𝑧 )
13 equequ2 ⊢ ( 𝑧 = 𝑦 → ( 𝑤 = 𝑧 ↔ 𝑤 = 𝑦 ) )
14 13 notbid ⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦 ) )
15 ax7v1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 = 𝑦 → 𝑤 = 𝑦 ) )
16 15 con3d ⊢ ( 𝑥 = 𝑤 → ( ¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦 ) )
17 16 spimevw ⊢ ( ¬ 𝑤 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
18 14 17 biimtrdi ⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) )
19 ax7v1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑦 → 𝑧 = 𝑦 ) )
20 19 con3d ⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦 ) )
21 20 spimevw ⊢ ( ¬ 𝑧 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
22 21 a1d ⊢ ( ¬ 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) )
23 18 22 pm2.61i ⊢ ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
24 23 exlimivv ⊢ ( ∃ 𝑤 ∃ 𝑧 ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
25 8 12 24 mp2b ⊢ ∃ 𝑥 ¬ 𝑥 = 𝑦
26 exnal ⊢ ( ∃ 𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 )
27 25 26 mpbi ⊢ ¬ ∀ 𝑥 𝑥 = 𝑦