Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dffin1a  Unicode version 
Description: A set is Iafinite iff it is not the union of two Iinfinite sets. Equivalent to definition Ia of [Levy58] p. 2. A Iinfinite Iafinite set is also known as an amorphous set. This is the second of Levy's eight definitions of finite set. Levy's Ifinite is equivalent to our dffin 6753 and not repeated here. These eight definitions are equivalent with Choice but strictly decreasing in strength in models where Choice fails; conversely, they provide a series of increasingly stronger notions of infiniteness. (Contributed by Stefan O'Rear, 12Nov2014.) 
Ref  Expression 

dffin1a  Fin^{Ia} 
Step  Hyp  Ref  Expression 

1  cfin1a 7788  . 2 Fin^{Ia}  
2  vy  . . . . . . 7  
3  2  cv 1618  . . . . . 6 
4  cfn 6749  . . . . . 6  
5  3, 4  wcel 1621  . . . . 5 
6  vx  . . . . . . . 8  
7  6  cv 1618  . . . . . . 7 
8  7, 3  cdif 3075  . . . . . 6 
9  8, 4  wcel 1621  . . . . 5 
10  5, 9  wo 359  . . . 4 
11  7  cpw 3530  . . . 4 
12  10, 2, 11  wral 2509  . . 3 
13  12, 6  cab 2239  . 2 
14  1, 13  wceq 1619  1 Fin^{Ia} 
Colors of variables: wff set class 
This definition is referenced by: isfin1a 7802 
Copyright terms: Public domain  W3C validator 