Add unct to iset.mm

An easy corollary of ctiunct and when we have two sets, rather than
countably many, we don't need to worry about choice.

Author: jkingdon

iset.mm

@@ -129948,6 +129948,28 @@ then the Limited Principle of Omniscience (LPO) implies excluded middle.
       TWJXAYGNXKXSPZJQXNXJJKUIXBUVQXMJENXKXSXLWIXCXDXEXF $.
   $}
 
+  ${
+    $d A f g h j x $.  $d B f g h j x $.
+    $( The union of two countable sets is countable.  (Contributed by Jim
+       Kingdon, 1-Nov-2023.) $)
+    unct $p |- ( ( E. f f : _om -onto-> ( A |_| 1o )
+        /\ E. g g : _om -onto-> ( B |_| 1o ) )
+        -> E. h h : _om -onto-> ( ( A u. B ) |_| 1o ) ) $=
+      ( vj vx com c1o cdju cv wfo wex wa c2o wcel c0 wceq wb djueq1 cun wi 2onn
+      cfn nnfi finct mp2b a1i cpr cif simpr df2o3 foeq3 sylib wo simplll iftrue
+      ciun eqidd syl foeq123d adantl mpbird ex simpllr wn 1n0 neii eqeq1 mtbiri
+      iffalse jaod elpri impel ctiunct 0lt2o 1lt2o iffalsed iunxprg mp2an exbii
+      exlimddv exlimiv exlimdv imp ) HAIJZCKZLZCMZHBIJZDKZLZDMHABUAZIJZEKZLZEMZ
+      WIWLWQDWHWLWQUBCWHWLWQWHWLNZHOIJZFKZLZWQFXAFMZWROHPOUDPXBUCOUEOFUFUGUHWRX
+      ANZHGQIUIZGKZQRZABUJZURZIJZWOLZEMWQXCGXDXGEWTXFWGWKUJZXCXAHXDIJZWTLZWRXAU
+      KOXDRWSXLRXAXMSULOXDITWSXLHWTUMUGUNXCXFXEIRZUOHXGIJZXKLZXEXDPXCXFXPXNXCXF
+      XPXCXFNXPWHWHWLXAXFUPXFXPWHSXCXFHHXOWFXKWGXFWGWKUQXFHUSXFXGARXOWFRXFABUQZ
+      XGAITUTVAVBVCVDXCXNXPXCXNNZXPWLWHWLXAXNVEXRXFVFZXPWLSXNXSXCXNXFIQRIQVGVHX
+      EIQVIVJZVBXSHHXOWJXKWKXFWGWKVKXSHUSXSXGBRXOWJRXFABVKXGBITUTVAUTVCVDVLXEQI
+      VMVNVOXJWPEXHWMRZXIWNRXJWPSQOPIOPYAVPVQGQIXGABOOXQXNXFABXTVRVSVTXHWMITXIW
+      NHWOUMUGWAUNWBVDWCWDWE $.
+  $}
+
 
 $(
 ###############################################################################

mmil.raw.html

@@ -4991,6 +4991,11 @@
   <td>depends on various cardinality theorems we don't have</td>
 </tr>
 
+<tr>
+  <td>unctb</td>
+  <td>~ unct</td>
+</tr>
+
 <tr>
   <td>infdjuabs</td>
   <td><i>none</i></td>