Theorem ax4 976

Description: Theorem showing that ax-4 977 can be derived from ax-5 964, ax-gen 967, ax-8 968, ax-9 969, ax-11 971, and ax-17 975 and is therefore redundant. Lemma 21 of [Monk2] p. 114.

This theorem should not be referenced in any proof. Instead, we will use ax-4 977 below so that uses of ax-4 977 can be more easily identified. In particular, this will more cleanly separate out the theorems of "pure" predicate calculus that don't involve equality or distinct variables. A beginner can accept ax-4 977 a priori, so that the proof of this theorem (ax4 976), which involves equality as well as the distinct the distinct variable requirements of ax-17 975, can be put off until later.

Note: All predicate calculus axioms introduced from this point forward are redundant. Immediately before their introduction, we prove them from earlier axioms to demonstrate their redundancy. Specifically, redundant axioms ax-4 977, ax-5o 979, ax-6o 982, ax-9o 1127, ax-10o 1144, ax-11o 1222, ax-15 1364, and ax-16 1214 are proved by theorems ax4 976, ax5o 978, ax6o 981, ax9o 1126, ax10o 1143, ax11o 1221, ax15 1363, and ax16 1213.

Assertion

Ref	Expression
ax4	⊢ (∀xφ → φ)

Proof of Theorem ax4

Step	Hyp	Ref	Expression
1		ax-9 969	. 2 ⊢ ¬ ∀y ¬ y = x
2		ax-17 975	. . 3 ⊢ (¬ (∀xφ → φ) → ∀y ¬ (∀xφ → φ))
3		ax-9 969	. . . . . . . . . . . . . 14 ⊢ ¬ ∀x ¬ x = y
4		ax-17 975	. . . . . . . . . . . . . . 15 ⊢ (¬ y = y → ∀x ¬ y = y)
5		ax-8 968	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = y → (x = y → y = y))
6	5	pm2.43i 64	. . . . . . . . . . . . . . . . . 18 ⊢ (x = y → y = y)
7	6	con3i 98	. . . . . . . . . . . . . . . . 17 ⊢ (¬ y = y → ¬ x = y)
8	7	ax-gen 967	. . . . . . . . . . . . . . . 16 ⊢ ∀x(¬ y = y → ¬ x = y)
9		ax-5 964	. . . . . . . . . . . . . . . 16 ⊢ (∀x(¬ y = y → ¬ x = y) → (∀x ¬ y = y → ∀x ¬ x = y))
10	8, 9	ax-mp 7	. . . . . . . . . . . . . . 15 ⊢ (∀x ¬ y = y → ∀x ¬ x = y)
11	4, 10	syl 10	. . . . . . . . . . . . . 14 ⊢ (¬ y = y → ∀x ¬ x = y)
12	3, 11	mt3 112	. . . . . . . . . . . . 13 ⊢ y = y
13		ax-8 968	. . . . . . . . . . . . 13 ⊢ (y = x → (y = y → x = y))
14	12, 13	mpi 44	. . . . . . . . . . . 12 ⊢ (y = x → x = y)
15		ax-11 971	. . . . . . . . . . . 12 ⊢ (x = y → (∀y ¬ φ → ∀x(x = y → ¬ φ)))
16	14, 15	syl 10	. . . . . . . . . . 11 ⊢ (y = x → (∀y ¬ φ → ∀x(x = y → ¬ φ)))
17		ax-17 975	. . . . . . . . . . 11 ⊢ (¬ φ → ∀y ¬ φ)
18	16, 17	syl5 21	. . . . . . . . . 10 ⊢ (y = x → (¬ φ → ∀x(x = y → ¬ φ)))
19		con2 90	. . . . . . . . . . . 12 ⊢ ((x = y → ¬ φ) → (φ → ¬ x = y))
20	19	ax-gen 967	. . . . . . . . . . 11 ⊢ ∀x((x = y → ¬ φ) → (φ → ¬ x = y))
21		ax-5 964	. . . . . . . . . . 11 ⊢ (∀x((x = y → ¬ φ) → (φ → ¬ x = y)) → (∀x(x = y → ¬ φ) → ∀x(φ → ¬ x = y)))
22	20, 21	ax-mp 7	. . . . . . . . . 10 ⊢ (∀x(x = y → ¬ φ) → ∀x(φ → ¬ x = y))
23	18, 22	syl6 22	. . . . . . . . 9 ⊢ (y = x → (¬ φ → ∀x(φ → ¬ x = y)))
24		ax-5 964	. . . . . . . . 9 ⊢ (∀x(φ → ¬ x = y) → (∀xφ → ∀x ¬ x = y))
25	23, 24	syl6 22	. . . . . . . 8 ⊢ (y = x → (¬ φ → (∀xφ → ∀x ¬ x = y)))
26		con3 94	. . . . . . . . 9 ⊢ ((∀xφ → ∀x ¬ x = y) → (¬ ∀x ¬ x = y → ¬ ∀xφ))
27	3, 26	mpi 44	. . . . . . . 8 ⊢ ((∀xφ → ∀x ¬ x = y) → ¬ ∀xφ)
28	25, 27	syl6 22	. . . . . . 7 ⊢ (y = x → (¬ φ → ¬ ∀xφ))
29	28	a3d 75	. . . . . 6 ⊢ (y = x → (∀xφ → φ))
30	29	con3i 98	. . . . 5 ⊢ (¬ (∀xφ → φ) → ¬ y = x)
31	30	ax-gen 967	. . . 4 ⊢ ∀y(¬ (∀xφ → φ) → ¬ y = x)
32		ax-5 964	. . . 4 ⊢ (∀y(¬ (∀xφ → φ) → ¬ y = x) → (∀y ¬ (∀xφ → φ) → ∀y ¬ y = x))
33	31, 32	ax-mp 7	. . 3 ⊢ (∀y ¬ (∀xφ → φ) → ∀y ¬ y = x)
34	2, 33	syl 10	. 2 ⊢ (¬ (∀xφ → φ) → ∀y ¬ y = x)
35	1, 34	mt3 112	1 ⊢ (∀xφ → φ)

Syntax hints:  ¬ wn 2   → wi 3  ∀wal 958

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 964  ax-gen 967  ax-8 968  ax-9 969  ax-11 971  ax-17 975

Copyright terms: Public domain