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

Metamath Proof Explorer

Theorem ax12inda

Description: Induction step for constructing a substitution instance of ax-c15 without using ax-c15 . Quantification case. (When z and y are distinct, ax12inda2 may be used instead to avoid the dummy variable w in the proof.) (Contributed by NM, 24-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ax12inda.1 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → ( 𝑥 = 𝑤 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) ) ) )
2 ax6ev ⊢ ∃ 𝑤 𝑤 = 𝑦
3 1 ax12inda2 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → ( 𝑥 = 𝑤 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑤 → ∀ 𝑧 𝜑 ) ) ) )
4 dveeq2-o ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑤 = 𝑦 → ∀ 𝑥 𝑤 = 𝑦 ) )
5 4 imp ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ∀ 𝑥 𝑤 = 𝑦 )
6 hba1-o ⊢ ( ∀ 𝑥 𝑤 = 𝑦 → ∀ 𝑥 ∀ 𝑥 𝑤 = 𝑦 )
7 equequ2 ⊢ ( 𝑤 = 𝑦 → ( 𝑥 = 𝑤 ↔ 𝑥 = 𝑦 ) )
8 7 sps-o ⊢ ( ∀ 𝑥 𝑤 = 𝑦 → ( 𝑥 = 𝑤 ↔ 𝑥 = 𝑦 ) )
9 6 8 albidh ⊢ ( ∀ 𝑥 𝑤 = 𝑦 → ( ∀ 𝑥 𝑥 = 𝑤 ↔ ∀ 𝑥 𝑥 = 𝑦 ) )
10 9 notbid ⊢ ( ∀ 𝑥 𝑤 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑤 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
11 5 10 syl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑤 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
12 7 adantl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( 𝑥 = 𝑤 ↔ 𝑥 = 𝑦 ) )
13 8 imbi1d ⊢ ( ∀ 𝑥 𝑤 = 𝑦 → ( ( 𝑥 = 𝑤 → ∀ 𝑧 𝜑 ) ↔ ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
14 6 13 albidh ⊢ ( ∀ 𝑥 𝑤 = 𝑦 → ( ∀ 𝑥 ( 𝑥 = 𝑤 → ∀ 𝑧 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
15 5 14 syl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( ∀ 𝑥 ( 𝑥 = 𝑤 → ∀ 𝑧 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
16 15 imbi2d ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑤 → ∀ 𝑧 𝜑 ) ) ↔ ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) )
17 12 16 imbi12d ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( ( 𝑥 = 𝑤 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑤 → ∀ 𝑧 𝜑 ) ) ) ↔ ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) ) )
18 11 17 imbi12d ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( ( ¬ ∀ 𝑥 𝑥 = 𝑤 → ( 𝑥 = 𝑤 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑤 → ∀ 𝑧 𝜑 ) ) ) ) ↔ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) ) ) )
19 3 18 mpbii ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) ) )
20 19 ex ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑤 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) ) ) )
21 20 exlimdv ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑤 𝑤 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) ) ) )
22 2 21 mpi ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) ) )
23 22 pm2.43i ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) )