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

Metamath Proof Explorer

Theorem ax12inda2ALT

Description: Alternate proof of ax12inda2 , slightly more direct and not requiring ax-c16 . (Contributed by NM, 4-May-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ax12inda2.1 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
Assertion ax12inda2ALT ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) )

Proof

Step Hyp Ref Expression
1 ax12inda2.1 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
2 ax-1 ⊢ ( ∀ 𝑥 𝜑 → ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) )
3 2 axc4i-o ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) )
4 3 a1i ⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) ) )
5 biidd ⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( 𝜑 ↔ 𝜑 ) )
6 5 dral1-o ⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑧 𝜑 ↔ ∀ 𝑥 𝜑 ) )
7 6 imbi2d ⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ↔ ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) ) )
8 7 dral2-o ⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) ) )
9 4 6 8 3imtr4d ⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
10 9 aecoms-o ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
11 10 a1d ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) )
12 11 a1d ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) ) )
13 simplr ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) ∧ 𝑥 = 𝑦 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 )
14 dveeq1-o ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) )
15 14 naecoms-o ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) )
16 15 imp ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ 𝑥 = 𝑦 ) → ∀ 𝑧 𝑥 = 𝑦 )
17 16 adantlr ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) ∧ 𝑥 = 𝑦 ) → ∀ 𝑧 𝑥 = 𝑦 )
18 hbnae-o ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦 )
19 hba1-o ⊢ ( ∀ 𝑧 𝑥 = 𝑦 → ∀ 𝑧 ∀ 𝑧 𝑥 = 𝑦 )
20 18 19 hban ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑧 𝑥 = 𝑦 ) → ∀ 𝑧 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑧 𝑥 = 𝑦 ) )
21 ax-c5 ⊢ ( ∀ 𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦 )
22 1 imp ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
23 21 22 sylan2 ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑧 𝑥 = 𝑦 ) → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
24 20 23 alimdh ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑧 𝑥 = 𝑦 ) → ( ∀ 𝑧 𝜑 → ∀ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
25 13 17 24 syl2anc ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) ∧ 𝑥 = 𝑦 ) → ( ∀ 𝑧 𝜑 → ∀ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
26 ax-11 ⊢ ( ∀ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑥 = 𝑦 → 𝜑 ) )
27 hbnae-o ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑧 )
28 hbnae-o ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑧 )
29 28 15 nf5dh ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑧 𝑥 = 𝑦 )
30 19.21t ⊢ ( Ⅎ 𝑧 𝑥 = 𝑦 → ( ∀ 𝑧 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
31 29 30 syl ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑧 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
32 27 31 albidh ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑥 ∀ 𝑧 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
33 26 32 imbitrid ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
34 33 ad2antrr ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) ∧ 𝑥 = 𝑦 ) → ( ∀ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
35 25 34 syld ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) ∧ 𝑥 = 𝑦 ) → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
36 35 exp31 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) ) )
37 12 36 pm2.61i ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) )