rexanuz2nf

Description: A simple counterexample related to theorem rexanuz2 , demonstrating the necessity of its disjoint variable constraints. Here, j appears free in ph , showing that without these constraints, rexanuz2 and similar theorems would not hold (see rexanre and rexanuz ). (Contributed by Glauco Siliprandi, 15-Feb-2025)

	Ref	Expression
Hypotheses	rexanuz2nf.1	$⊢ Z = ℕ_{0}$
	rexanuz2nf.2	$⊢ φ \leftrightarrow (j = 0 \land j \leq k)$
	rexanuz2nf.3	$⊢ ψ \leftrightarrow 0 < k$
Assertion	rexanuz2nf	$⊢ \neg (\exists j \in Z \forall k \in ℤ_{\geq j} (φ \land ψ) \leftrightarrow (\exists j \in Z \forall k \in ℤ_{\geq j} φ \land \exists j \in Z \forall k \in ℤ_{\geq j} ψ))$

Proof

Step	Hyp	Ref	Expression
1		rexanuz2nf.1	$⊢ Z = ℕ_{0}$
2		rexanuz2nf.2	$⊢ φ \leftrightarrow (j = 0 \land j \leq k)$
3		rexanuz2nf.3	$⊢ ψ \leftrightarrow 0 < k$
4		0nn0	$⊢ 0 \in ℕ_{0}$
5		nn0ge0	$⊢ k \in ℕ_{0} \to 0 \leq k$
6	5	rgen	$⊢ \forall k \in ℕ_{0} 0 \leq k$
7		fveq2	$⊢ j = 0 \to ℤ_{\geq j} = ℤ_{\geq 0}$
8		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
9	7 8	eqtr4di	$⊢ j = 0 \to ℤ_{\geq j} = ℕ_{0}$
10	9	raleqdv	$⊢ j = 0 \to (\forall k \in ℤ_{\geq j} (j = 0 \land j \leq k) \leftrightarrow \forall k \in ℕ_{0} (j = 0 \land j \leq k))$
11	5	ad2antlr	$⊢ ((j = 0 \land k \in ℕ_{0}) \land (j = 0 \land j \leq k)) \to 0 \leq k$
12		simpll	$⊢ ((j = 0 \land k \in ℕ_{0}) \land 0 \leq k) \to j = 0$
13		simpr	$⊢ ((j = 0 \land k \in ℕ_{0}) \land 0 \leq k) \to 0 \leq k$
14	12 13	eqbrtrd	$⊢ ((j = 0 \land k \in ℕ_{0}) \land 0 \leq k) \to j \leq k$
15	12 14	jca	$⊢ ((j = 0 \land k \in ℕ_{0}) \land 0 \leq k) \to (j = 0 \land j \leq k)$
16	11 15	impbida	$⊢ (j = 0 \land k \in ℕ_{0}) \to ((j = 0 \land j \leq k) \leftrightarrow 0 \leq k)$
17	16	ralbidva	$⊢ j = 0 \to (\forall k \in ℕ_{0} (j = 0 \land j \leq k) \leftrightarrow \forall k \in ℕ_{0} 0 \leq k)$
18	10 17	bitrd	$⊢ j = 0 \to (\forall k \in ℤ_{\geq j} (j = 0 \land j \leq k) \leftrightarrow \forall k \in ℕ_{0} 0 \leq k)$
19	18	rspcev	$⊢ (0 \in ℕ_{0} \land \forall k \in ℕ_{0} 0 \leq k) \to \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} (j = 0 \land j \leq k)$
20	4 6 19	mp2an	$⊢ \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} (j = 0 \land j \leq k)$
21		nfcv	$⊢ \underline{Ⅎ} j ℕ_{0}$
22	1 21	nfcxfr	$⊢ \underline{Ⅎ} j Z$
23	22 21 1	rexeqif	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (j = 0 \land j \leq k) \leftrightarrow \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} (j = 0 \land j \leq k)$
24	20 23	mpbir	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (j = 0 \land j \leq k)$
25	2	ralbii	$⊢ \forall k \in ℤ_{\geq j} φ \leftrightarrow \forall k \in ℤ_{\geq j} (j = 0 \land j \leq k)$
26	25	rexbii	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} φ \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (j = 0 \land j \leq k)$
27	24 26	mpbir	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} φ$
28		1nn0	$⊢ 1 \in ℕ_{0}$
29		nngt0	$⊢ k \in ℕ \to 0 < k$
30	29	rgen	$⊢ \forall k \in ℕ 0 < k$
31		fveq2	$⊢ j = 1 \to ℤ_{\geq j} = ℤ_{\geq 1}$
32		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
33	31 32	eqtr4di	$⊢ j = 1 \to ℤ_{\geq j} = ℕ$
34	33	raleqdv	$⊢ j = 1 \to (\forall k \in ℤ_{\geq j} 0 < k \leftrightarrow \forall k \in ℕ 0 < k)$
35	34	rspcev	$⊢ (1 \in ℕ_{0} \land \forall k \in ℕ 0 < k) \to \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} 0 < k$
36	28 30 35	mp2an	$⊢ \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} 0 < k$
37	22 21 1	rexeqif	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} 0 < k \leftrightarrow \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} 0 < k$
38	36 37	mpbir	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} 0 < k$
39	3	ralbii	$⊢ \forall k \in ℤ_{\geq j} ψ \leftrightarrow \forall k \in ℤ_{\geq j} 0 < k$
40	39	rexbii	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} ψ \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} 0 < k$
41	38 40	mpbir	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} ψ$
42	27 41	pm3.2i	$⊢ (\exists j \in Z \forall k \in ℤ_{\geq j} φ \land \exists j \in Z \forall k \in ℤ_{\geq j} ψ)$
43		nfv	$⊢ Ⅎ k \neg ((j = 0 \land j \leq j) \land 0 < j)$
44		nfcv	$⊢ \underline{Ⅎ} k j$
45		nfcv	$⊢ \underline{Ⅎ} k ℤ_{\geq j}$
46	8	uzid3	$⊢ j \in ℕ_{0} \to j \in ℤ_{\geq j}$
47	46	adantr	$⊢ (j \in ℕ_{0} \land j = 0) \to j \in ℤ_{\geq j}$
48		0re	$⊢ 0 \in ℝ$
49	48	ltnri	$⊢ \neg 0 < 0$
50	49	a1i	$⊢ j = 0 \to \neg 0 < 0$
51		eqcom	$⊢ j = 0 \leftrightarrow 0 = j$
52	51	biimpi	$⊢ j = 0 \to 0 = j$
53	50 52	brneqtrd	$⊢ j = 0 \to \neg 0 < j$
54	53	intnand	$⊢ j = 0 \to \neg ((j = 0 \land j \leq j) \land 0 < j)$
55	54	adantl	$⊢ (j \in ℕ_{0} \land j = 0) \to \neg ((j = 0 \land j \leq j) \land 0 < j)$
56		breq2	$⊢ k = j \to (j \leq k \leftrightarrow j \leq j)$
57	56	anbi2d	$⊢ k = j \to ((j = 0 \land j \leq k) \leftrightarrow (j = 0 \land j \leq j))$
58	2 57	bitrid	$⊢ k = j \to (φ \leftrightarrow (j = 0 \land j \leq j))$
59		breq2	$⊢ k = j \to (0 < k \leftrightarrow 0 < j)$
60	3 59	bitrid	$⊢ k = j \to (ψ \leftrightarrow 0 < j)$
61	58 60	anbi12d	$⊢ k = j \to ((φ \land ψ) \leftrightarrow ((j = 0 \land j \leq j) \land 0 < j))$
62	61	notbid	$⊢ k = j \to (\neg (φ \land ψ) \leftrightarrow \neg ((j = 0 \land j \leq j) \land 0 < j))$
63	43 44 45 47 55 62	rspced	$⊢ (j \in ℕ_{0} \land j = 0) \to \exists k \in ℤ_{\geq j} \neg (φ \land ψ)$
64	46	adantr	$⊢ (j \in ℕ_{0} \land \neg j = 0) \to j \in ℤ_{\geq j}$
65		id	$⊢ \neg j = 0 \to \neg j = 0$
66	65	intnanrd	$⊢ \neg j = 0 \to \neg (j = 0 \land j \leq j)$
67	66	intnanrd	$⊢ \neg j = 0 \to \neg ((j = 0 \land j \leq j) \land 0 < j)$
68	67	adantl	$⊢ (j \in ℕ_{0} \land \neg j = 0) \to \neg ((j = 0 \land j \leq j) \land 0 < j)$
69	43 44 45 64 68 62	rspced	$⊢ (j \in ℕ_{0} \land \neg j = 0) \to \exists k \in ℤ_{\geq j} \neg (φ \land ψ)$
70	63 69	pm2.61dan	$⊢ j \in ℕ_{0} \to \exists k \in ℤ_{\geq j} \neg (φ \land ψ)$
71		rexnal	$⊢ \exists k \in ℤ_{\geq j} \neg (φ \land ψ) \leftrightarrow \neg \forall k \in ℤ_{\geq j} (φ \land ψ)$
72	70 71	sylib	$⊢ j \in ℕ_{0} \to \neg \forall k \in ℤ_{\geq j} (φ \land ψ)$
73	72	nrex	$⊢ \neg \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} (φ \land ψ)$
74	22 21 1	rexeqif	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (φ \land ψ) \leftrightarrow \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} (φ \land ψ)$
75	73 74	mtbir	$⊢ \neg \exists j \in Z \forall k \in ℤ_{\geq j} (φ \land ψ)$
76	42 75	pm3.2i	$⊢ ((\exists j \in Z \forall k \in ℤ_{\geq j} φ \land \exists j \in Z \forall k \in ℤ_{\geq j} ψ) \land \neg \exists j \in Z \forall k \in ℤ_{\geq j} (φ \land ψ))$
77		annim	$⊢ ((\exists j \in Z \forall k \in ℤ_{\geq j} φ \land \exists j \in Z \forall k \in ℤ_{\geq j} ψ) \land \neg \exists j \in Z \forall k \in ℤ_{\geq j} (φ \land ψ)) \leftrightarrow \neg ((\exists j \in Z \forall k \in ℤ_{\geq j} φ \land \exists j \in Z \forall k \in ℤ_{\geq j} ψ) \to \exists j \in Z \forall k \in ℤ_{\geq j} (φ \land ψ))$
78	76 77	mpbi	$⊢ \neg ((\exists j \in Z \forall k \in ℤ_{\geq j} φ \land \exists j \in Z \forall k \in ℤ_{\geq j} ψ) \to \exists j \in Z \forall k \in ℤ_{\geq j} (φ \land ψ))$
79	78	nimnbi2	$⊢ \neg (\exists j \in Z \forall k \in ℤ_{\geq j} (φ \land ψ) \leftrightarrow (\exists j \in Z \forall k \in ℤ_{\geq j} φ \land \exists j \in Z \forall k \in ℤ_{\geq j} ψ))$

Metamath Proof Explorer

Theorem rexanuz2nf

Proof