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

Metamath Proof Explorer

Theorem dvelimf-o

Description: Proof of dvelimh that uses ax-c11 but not ax-c15 , ax-c11n , or ax-12 . Version of dvelimh using ax-c11 instead of axc11 . (Contributed by NM, 12-Nov-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses dvelimf-o.1 ⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
dvelimf-o.2 ⊢ ( 𝜓 → ∀ 𝑧 𝜓 )
dvelimf-o.3 ⊢ ( 𝑧 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion dvelimf-o ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → ∀ 𝑥 𝜓 ) )

Proof

Step Hyp Ref Expression
1 dvelimf-o.1 ⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2 dvelimf-o.2 ⊢ ( 𝜓 → ∀ 𝑧 𝜓 )
3 dvelimf-o.3 ⊢ ( 𝑧 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
4 hba1-o ⊢ ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑧 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) )
5 ax-c11 ⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑧 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) )
6 5 aecoms-o ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑧 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) )
7 4 6 syl5 ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) )
8 7 a1d ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) ) )
9 hbnae-o ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑧 )
10 hbnae-o ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦 )
11 9 10 hban ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ∀ 𝑧 ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
12 hbnae-o ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑧 )
13 hbnae-o ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 )
14 12 13 hban ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ∀ 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
15 ax-c9 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) ) )
16 15 imp ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) )
17 1 a1i ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝜑 → ∀ 𝑥 𝜑 ) )
18 14 16 17 hbimd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑧 = 𝑦 → 𝜑 ) ) )
19 11 18 hbald ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) )
20 19 ex ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) ) )
21 8 20 pm2.61i ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) )
22 2 3 equsalh ⊢ ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ↔ 𝜓 )
23 22 albii ⊢ ( ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ↔ ∀ 𝑥 𝜓 )
24 21 22 23 3imtr3g ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → ∀ 𝑥 𝜓 ) )