Metamath Proof Explorer


Theorem sn-dtru

Description: dtru without ax-8 or ax-12 . (Contributed by SN, 21-Sep-2023)

Ref Expression
Assertion sn-dtru ¬ ∀ 𝑥 𝑥 = 𝑦

Proof

Step Hyp Ref Expression
1 sn-el 𝑤𝑥 𝑥𝑤
2 ax-nul 𝑧𝑥 ¬ 𝑥𝑧
3 exdistrv ( ∃ 𝑤𝑧 ( ∃ 𝑥 𝑥𝑤 ∧ ∀ 𝑥 ¬ 𝑥𝑧 ) ↔ ( ∃ 𝑤𝑥 𝑥𝑤 ∧ ∃ 𝑧𝑥 ¬ 𝑥𝑧 ) )
4 1 2 3 mpbir2an 𝑤𝑧 ( ∃ 𝑥 𝑥𝑤 ∧ ∀ 𝑥 ¬ 𝑥𝑧 )
5 ax9v1 ( 𝑤 = 𝑧 → ( 𝑥𝑤𝑥𝑧 ) )
6 5 eximdv ( 𝑤 = 𝑧 → ( ∃ 𝑥 𝑥𝑤 → ∃ 𝑥 𝑥𝑧 ) )
7 df-ex ( ∃ 𝑥 𝑥𝑧 ↔ ¬ ∀ 𝑥 ¬ 𝑥𝑧 )
8 6 7 syl6ib ( 𝑤 = 𝑧 → ( ∃ 𝑥 𝑥𝑤 → ¬ ∀ 𝑥 ¬ 𝑥𝑧 ) )
9 imnan ( ( ∃ 𝑥 𝑥𝑤 → ¬ ∀ 𝑥 ¬ 𝑥𝑧 ) ↔ ¬ ( ∃ 𝑥 𝑥𝑤 ∧ ∀ 𝑥 ¬ 𝑥𝑧 ) )
10 8 9 sylib ( 𝑤 = 𝑧 → ¬ ( ∃ 𝑥 𝑥𝑤 ∧ ∀ 𝑥 ¬ 𝑥𝑧 ) )
11 10 con2i ( ( ∃ 𝑥 𝑥𝑤 ∧ ∀ 𝑥 ¬ 𝑥𝑧 ) → ¬ 𝑤 = 𝑧 )
12 11 2eximi ( ∃ 𝑤𝑧 ( ∃ 𝑥 𝑥𝑤 ∧ ∀ 𝑥 ¬ 𝑥𝑧 ) → ∃ 𝑤𝑧 ¬ 𝑤 = 𝑧 )
13 equeuclr ( 𝑧 = 𝑦 → ( 𝑤 = 𝑦𝑤 = 𝑧 ) )
14 13 con3d ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ¬ 𝑤 = 𝑦 ) )
15 ax7v1 ( 𝑥 = 𝑤 → ( 𝑥 = 𝑦𝑤 = 𝑦 ) )
16 15 con3d ( 𝑥 = 𝑤 → ( ¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦 ) )
17 16 spimevw ( ¬ 𝑤 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
18 14 17 syl6 ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) )
19 ax7v1 ( 𝑥 = 𝑧 → ( 𝑥 = 𝑦𝑧 = 𝑦 ) )
20 19 con3d ( 𝑥 = 𝑧 → ( ¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦 ) )
21 20 spimevw ( ¬ 𝑧 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
22 21 a1d ( ¬ 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) )
23 18 22 pm2.61i ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
24 23 exlimivv ( ∃ 𝑤𝑧 ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
25 4 12 24 mp2b 𝑥 ¬ 𝑥 = 𝑦
26 exnal ( ∃ 𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 )
27 25 26 mpbi ¬ ∀ 𝑥 𝑥 = 𝑦