Metamath Proof Explorer

Theorem 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 ⊢ 𝑍 = ℕ0
rexanuz2nf.2 ⊢ ( 𝜑 ↔ ( 𝑗 = 0 ∧ 𝑗 ≤ 𝑘 ) )
rexanuz2nf.3 ⊢ ( 𝜓 ↔ 0 < 𝑘 )
Assertion rexanuz2nf ¬ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )

Proof

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