Theorem example-E7.1b 1075

Description: '𝑥' is effectively free in the statement '(𝑥 ⋅ 𝑦 = 0)'. †

Note that if we could show '⊢ Ⅎ𝑥(𝑥 ⋅ 𝑦) = 0', then we would also be able to show that '⊢ ∀𝑦Ⅎ𝑥(𝑥 ⋅ 𝑦) = 0', which would contradict the conclusion of this example. This means that, without any extra hypotheses, '𝑥' is effectively free (and thus also grammatically free, obviously) in the WFF '(𝑥 ⋅ 𝑦) = 0'. However, adding the open hypothesis '𝑦 = 0', either as a theorem hypothesis or as an antecedent, causes '𝑥' to become effectively not free in '(𝑥 ⋅ 𝑦) = 0'. This is why we say that '𝑥' is *conditionally* not free in '𝜑' when we can deduce 'Ⅎ𝑥𝜑' with the addition of one or more hypotheses, but cannot do so working strictly from axioms.

Since no arithmetic axioms have been introduced, we state '(0 ⋅ 𝑦) = 0' as a hypothesis. We also state '¬ ∀𝑥∀𝑦(𝑥 ⋅ 𝑦) = 0' as a hypothesis. With the Peano Axioms, we will define '1'. The second hypothesis then follows from the case '¬ (1⋅1) = 0'.

Hypotheses

Ref	Expression
example-E7.1b.1	⊢ (0 ⋅ 𝑦) = 0
example-E7.1b.2	⊢ ¬ ∀𝑥∀𝑦 (𝑥 ⋅ 𝑦) = 0

Assertion

Ref	Expression
example-E7.1b	⊢ ¬ ∀𝑦Ⅎ𝑥 (𝑥 ⋅ 𝑦) = 0

Distinct variable group:   𝑥,𝑦

Proof of Theorem example-E7.1b

Step	Hyp	Ref	Expression
1		dfnfreealtonlyif-P7 966	. . . . 5 ⊢ (Ⅎ𝑥 (𝑥 ⋅ 𝑦) = 0 → (∃𝑥 (𝑥 ⋅ 𝑦) = 0 → ∀𝑥 (𝑥 ⋅ 𝑦) = 0))
2	1	dalloverim-P7.GENF.RC 1027	. . . 4 ⊢ (∀𝑦Ⅎ𝑥 (𝑥 ⋅ 𝑦) = 0 → (∀𝑦∃𝑥 (𝑥 ⋅ 𝑦) = 0 → ∀𝑦∀𝑥 (𝑥 ⋅ 𝑦) = 0))
3		axL6ex-P7 925	. . . . . 6 ⊢ ∃𝑥 𝑥 = 0
4		ndsubmultl-P7.24d.CL 921	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑥 ⋅ 𝑦) = (0 ⋅ 𝑦))
5		example-E7.1b.1	. . . . . . . . 9 ⊢ (0 ⋅ 𝑦) = 0
6	5	rcp-NDIMP0addall 207	. . . . . . . 8 ⊢ (𝑥 = 0 → (0 ⋅ 𝑦) = 0)
7	4, 6	eqtrns-P7 987	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ⋅ 𝑦) = 0)
8	7	alloverimex-P7.GENF.RC 950	. . . . . 6 ⊢ (∃𝑥 𝑥 = 0 → ∃𝑥 (𝑥 ⋅ 𝑦) = 0)
9	3, 8	rcp-NDIME0 228	. . . . 5 ⊢ ∃𝑥 (𝑥 ⋅ 𝑦) = 0
10	9	axGEN-P7 933	. . . 4 ⊢ ∀𝑦∃𝑥 (𝑥 ⋅ 𝑦) = 0
11	2, 10	mae-P3.23.RC 258	. . 3 ⊢ (∀𝑦Ⅎ𝑥 (𝑥 ⋅ 𝑦) = 0 → ∀𝑦∀𝑥 (𝑥 ⋅ 𝑦) = 0)
12		allcomm-P7 1058	. . 3 ⊢ (∀𝑦∀𝑥 (𝑥 ⋅ 𝑦) = 0 ↔ ∀𝑥∀𝑦 (𝑥 ⋅ 𝑦) = 0)
13	11, 12	subimr2-P4.RC 543	. 2 ⊢ (∀𝑦Ⅎ𝑥 (𝑥 ⋅ 𝑦) = 0 → ∀𝑥∀𝑦 (𝑥 ⋅ 𝑦) = 0)
14		example-E7.1b.2	. . 3 ⊢ ¬ ∀𝑥∀𝑦 (𝑥 ⋅ 𝑦) = 0
15	14	rcp-NDIMP0addall 207	. 2 ⊢ (∀𝑦Ⅎ𝑥 (𝑥 ⋅ 𝑦) = 0 → ¬ ∀𝑥∀𝑦 (𝑥 ⋅ 𝑦) = 0)
16	13, 15	rcp-NDNEGI1 218	1 ⊢ ¬ ∀𝑦Ⅎ𝑥 (𝑥 ⋅ 𝑦) = 0

Syntax hints:  term-obj 1  0term_zero 2   ⋅ term-mult 5   = wff-equals 6  ∀wff-forall 8  ¬ wff-neg 9  ∃wff-exists 595  Ⅎwff-nfree 681

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19  ax-L9-multl 25  ax-L10 27  ax-L11 28  ax-L12 29

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596  df-nfree-D6.1 682  df-psub-D6.2 716

This theorem is referenced by: (None)