ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0ct Unicode version

Theorem 0ct 6869
Description: The empty set is countable. Remark of [BauerSwan], p. 14:3 which also has the definition of countable used here. (Contributed by Jim Kingdon, 13-Mar-2023.)
Assertion
Ref Expression
0ct  |-  E. f 
f : om -onto-> ( (/) 1o )

Proof of Theorem 0ct
Dummy variables  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0lt1o 6242 . . . . 5  |-  (/)  e.  1o
2 djurcl 6824 . . . . 5  |-  ( (/)  e.  1o  ->  (inr `  (/) )  e.  ( (/) 1o ) )
31, 2ax-mp 7 . . . 4  |-  (inr `  (/) )  e.  ( (/) 1o )
43fconst6 5245 . . 3  |-  ( om 
X.  { (inr `  (/) ) } ) : om --> ( (/) 1o )
5 peano1 4437 . . . . 5  |-  (/)  e.  om
6 rex0 3319 . . . . . . . . 9  |-  -.  E. w  e.  (/)  y  =  (inl `  w )
7 djur 6837 . . . . . . . . . 10  |-  ( y  e.  ( (/) 1o )  ->  ( E. w  e.  (/)  y  =  (inl
`  w )  \/ 
E. w  e.  1o  y  =  (inr `  w
) ) )
87ord 681 . . . . . . . . 9  |-  ( y  e.  ( (/) 1o )  ->  ( -.  E. w  e.  (/)  y  =  (inl `  w )  ->  E. w  e.  1o  y  =  (inr `  w
) ) )
96, 8mpi 15 . . . . . . . 8  |-  ( y  e.  ( (/) 1o )  ->  E. w  e.  1o  y  =  (inr `  w
) )
10 df1o2 6232 . . . . . . . . 9  |-  1o  =  { (/) }
1110rexeqi 2581 . . . . . . . 8  |-  ( E. w  e.  1o  y  =  (inr `  w )  <->  E. w  e.  { (/) } y  =  (inr `  w ) )
129, 11sylib 121 . . . . . . 7  |-  ( y  e.  ( (/) 1o )  ->  E. w  e.  { (/)
} y  =  (inr
`  w ) )
13 0ex 3987 . . . . . . . 8  |-  (/)  e.  _V
14 fveq2 5340 . . . . . . . . 9  |-  ( w  =  (/)  ->  (inr `  w )  =  (inr
`  (/) ) )
1514eqeq2d 2106 . . . . . . . 8  |-  ( w  =  (/)  ->  ( y  =  (inr `  w
)  <->  y  =  (inr
`  (/) ) ) )
1613, 15rexsn 3507 . . . . . . 7  |-  ( E. w  e.  { (/) } y  =  (inr `  w )  <->  y  =  (inr `  (/) ) )
1712, 16sylib 121 . . . . . 6  |-  ( y  e.  ( (/) 1o )  ->  y  =  (inr
`  (/) ) )
183elexi 2645 . . . . . . . 8  |-  (inr `  (/) )  e.  _V
1918fvconst2 5552 . . . . . . 7  |-  ( (/)  e.  om  ->  ( ( om  X.  { (inr `  (/) ) } ) `  (/) )  =  (inr `  (/) ) )
205, 19ax-mp 7 . . . . . 6  |-  ( ( om  X.  { (inr
`  (/) ) } ) `
 (/) )  =  (inr
`  (/) )
2117, 20syl6eqr 2145 . . . . 5  |-  ( y  e.  ( (/) 1o )  ->  y  =  ( ( om  X.  {
(inr `  (/) ) } ) `  (/) ) )
22 fveq2 5340 . . . . . 6  |-  ( z  =  (/)  ->  ( ( om  X.  { (inr
`  (/) ) } ) `
 z )  =  ( ( om  X.  { (inr `  (/) ) } ) `  (/) ) )
2322rspceeqv 2753 . . . . 5  |-  ( (
(/)  e.  om  /\  y  =  ( ( om 
X.  { (inr `  (/) ) } ) `  (/) ) )  ->  E. z  e.  om  y  =  ( ( om  X.  {
(inr `  (/) ) } ) `  z ) )
245, 21, 23sylancr 406 . . . 4  |-  ( y  e.  ( (/) 1o )  ->  E. z  e.  om  y  =  ( ( om  X.  { (inr `  (/) ) } ) `  z ) )
2524rgen 2439 . . 3  |-  A. y  e.  ( (/) 1o ) E. z  e.  om  y  =  ( ( om 
X.  { (inr `  (/) ) } ) `  z )
26 dffo3 5485 . . 3  |-  ( ( om  X.  { (inr
`  (/) ) } ) : om -onto-> ( (/) 1o )  <->  ( ( om 
X.  { (inr `  (/) ) } ) : om --> ( (/) 1o )  /\  A. y  e.  ( (/) 1o ) E. z  e.  om  y  =  ( ( om 
X.  { (inr `  (/) ) } ) `  z ) ) )
274, 25, 26mpbir2an 891 . 2  |-  ( om 
X.  { (inr `  (/) ) } ) : om -onto-> ( (/) 1o )
28 omex 4436 . . . 4  |-  om  e.  _V
2918snex 4041 . . . 4  |-  { (inr
`  (/) ) }  e.  _V
3028, 29xpex 4582 . . 3  |-  ( om 
X.  { (inr `  (/) ) } )  e. 
_V
31 foeq1 5264 . . 3  |-  ( f  =  ( om  X.  { (inr `  (/) ) } )  ->  ( f : om -onto-> ( (/) 1o )  <-> 
( om  X.  {
(inr `  (/) ) } ) : om -onto-> ( (/) 1o ) ) )
3230, 31spcev 2727 . 2  |-  ( ( om  X.  { (inr
`  (/) ) } ) : om -onto-> ( (/) 1o )  ->  E. f 
f : om -onto-> ( (/) 1o ) )
3327, 32ax-mp 7 1  |-  E. f 
f : om -onto-> ( (/) 1o )
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1296   E.wex 1433    e. wcel 1445   A.wral 2370   E.wrex 2371   (/)c0 3302   {csn 3466   omcom 4433    X. cxp 4465   -->wf 5045   -onto->wfo 5047   ` cfv 5049   1oc1o 6212   ⊔ cdju 6810  inlcinl 6817  inrcinr 6818
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-nul 3986  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-iinf 4431
This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-rex 2376  df-v 2635  df-sbc 2855  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-nul 3303  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-int 3711  df-br 3868  df-opab 3922  df-mpt 3923  df-tr 3959  df-id 4144  df-iord 4217  df-on 4219  df-suc 4222  df-iom 4434  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-rn 4478  df-iota 5014  df-fun 5051  df-fn 5052  df-f 5053  df-fo 5055  df-fv 5057  df-1st 5949  df-2nd 5950  df-1o 6219  df-dju 6811  df-inl 6819  df-inr 6820
This theorem is referenced by:  enumct  6873
  Copyright terms: Public domain W3C validator