ax12v2-o

Description: Rederivation of ax-c15 from ax12v (without using ax-c15 or the full ax-12 ). Thus, the hypothesis ( ax12v ) provides an alternate axiom that can be used in place of ax-c15 . See also axc15 . (Contributed by NM, 2-Feb-2007) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	ax12v2-o.1	⊢ ( 𝑥 = 𝑧 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
	Assertion	ax12v2-o	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax12v2-o.1	⊢ ( 𝑥 = 𝑧 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
2		ax6ev	⊢ ∃ 𝑧 𝑧 = 𝑦
3		equequ2	⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑥 = 𝑦 ) )
4	3	adantl	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦 ) → ( 𝑥 = 𝑧 ↔ 𝑥 = 𝑦 ) )
5		dveeq2-o	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) )
6	5	imp	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦 ) → ∀ 𝑥 𝑧 = 𝑦 )
7		nfa1-o	⊢ Ⅎ 𝑥 ∀ 𝑥 𝑧 = 𝑦
8	3	imbi1d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 = 𝑧 → 𝜑 ) ↔ ( 𝑥 = 𝑦 → 𝜑 ) ) )
9	8	sps-o	⊢ ( ∀ 𝑥 𝑧 = 𝑦 → ( ( 𝑥 = 𝑧 → 𝜑 ) ↔ ( 𝑥 = 𝑦 → 𝜑 ) ) )
10	7 9	albid	⊢ ( ∀ 𝑥 𝑧 = 𝑦 → ( ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
11	6 10	syl	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦 ) → ( ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
12	11	imbi2d	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦 ) → ( ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ↔ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
13	4 12	imbi12d	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦 ) → ( ( 𝑥 = 𝑧 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) ↔ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) )
14	1 13	mpbii	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦 ) → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
15	14	ex	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) )
16	15	exlimdv	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑧 𝑧 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) )
17	2 16	mpi	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )

Metamath Proof Explorer

Theorem ax12v2-o

Proof