diff --git a/.unreleased/bug-fixes/fixSetInclusionwithArrays.md b/.unreleased/bug-fixes/fixSetInclusionwithArrays.md
new file mode 100644
index 0000000000..199ff50873
--- /dev/null
+++ b/.unreleased/bug-fixes/fixSetInclusionwithArrays.md
@@ -0,0 +1 @@
+fix crash on the arrays encoding when having a subset relation containing infinite sets, see #2810
\ No newline at end of file
diff --git a/test/tla/FunInInfiniteSubset.tla b/test/tla/FunInInfiniteSubset.tla
new file mode 100644
index 0000000000..93e4f1c137
--- /dev/null
+++ b/test/tla/FunInInfiniteSubset.tla
@@ -0,0 +1,22 @@
+--------------- MODULE FunInInfiniteSubset -----------------
+
+EXTENDS Integers
+
+P == {"P1_OF_P"}
+
+VARIABLE
+    \* @type: P -> Set(Int);
+    myVariable
+
+Init ==
+    myVariable = [p \in P |-> {0}]
+
+Step(p) ==
+    myVariable' = [q \in P |-> {0}]
+
+Next == \E p \in P : Step(p)
+
+TypeOkay == myVariable \in [P -> SUBSET Int]
+TypeOkay_ == TypeOkay
+
+=============================================
diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
index 958054cb4a..0695446c29 100644
--- a/test/tla/cli-integration-tests.md
+++ b/test/tla/cli-integration-tests.md
@@ -2812,6 +2812,18 @@ $ apalache-mc check --inv=Sanity FunExcept3.tla | sed 's/[IEW]@.*//'
 EXITCODE: OK
 ```
 
+### check FunInInfiniteSubset (array-encoding)
+
+A regression test for function membership in the presence of infinite sets.
+
+See https://github.com/informalsystems/apalache/issues/2810
+
+```sh
+$ apalache-mc check --init=TypeOkay_ --inv=TypeOkay --length=1 FunInInfiniteSubset.tla | sed 's/[IEW]@.*//'
+...
+EXITCODE: OK
+```
+
 ### check ERC20.tla
 
 ```sh
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithArrays.scala
index fe74c3017c..912d5ef8dc 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithArrays.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithArrays.scala
@@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules
 
 import at.forsyte.apalache.tla.bmcmt.implicitConversions.Crossable
 import at.forsyte.apalache.tla.bmcmt.rewriter.ConstSimplifierForSmt
-import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, PowSetT, UnknownT}
+import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, InfSetT, PowSetT, UnknownT}
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, RewriterException, RewritingRule, SymbState, SymbStateRewriter}
 import at.forsyte.apalache.tla.lir.{BoolT1, OperEx, RecT1, SetT1, TlaEx, TupT1}
 import at.forsyte.apalache.tla.lir.convenience._
@@ -35,6 +35,9 @@ class SetInclusionRuleWithArrays(rewriter: SymbStateRewriter) extends RewritingR
           case (CellTFrom(SetT1(_)), CellTFrom(SetT1(_))) =>
             subset(rightState, leftCell, rightCell, false)
 
+          case (CellTFrom(SetT1(_)), InfSetT(_)) =>
+            subset(rightState, leftCell, rightCell, false)
+
           case (CellTFrom(SetT1(SetT1(t1))), PowSetT(SetT1(t2))) =>
             if (t1 != t2) {
               throw new RewriterException("Unexpected set types: %s and %s in %s"
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithFunArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithFunArrays.scala
index f052a5931f..3346521a83 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithFunArrays.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithFunArrays.scala
@@ -1,7 +1,7 @@
 package at.forsyte.apalache.tla.bmcmt.rules
 
 import at.forsyte.apalache.tla.bmcmt._
-import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, PowSetT}
+import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, InfSetT, PowSetT}
 import at.forsyte.apalache.tla.lir.{OperEx, SetT1}
 import at.forsyte.apalache.tla.lir.convenience._
 import at.forsyte.apalache.tla.lir.UntypedPredefs._
@@ -31,6 +31,9 @@ class SetInclusionRuleWithFunArrays(rewriter: SymbStateRewriter) extends Rewriti
           case (CellTFrom(SetT1(_)), CellTFrom(SetT1(_))) =>
             rewriter.lazyEq.subsetEq(rightState, leftCell, rightCell)
 
+          case (CellTFrom(SetT1(_)), InfSetT(_)) =>
+            rewriter.lazyEq.subsetEq(rightState, leftCell, rightCell)
+
           case (CellTFrom(SetT1(SetT1(t1))), PowSetT(SetT1(t2))) =>
             if (t1 != t2) {
               throw new RewriterException("Unexpected set types: %s and %s in %s"