TPTP Problem File: SEU509^1.p

View Solutions - Solve Problem

```%------------------------------------------------------------------------------
% File     : SEU509^1 : TPTP v7.2.0. Released v3.7.0.
% Domain   : Set Theory
% Problem  : Preliminary Notions - Basic Laws of Logic
% Version  : Especial.
% English  : (! A:i.nonempty A -> (? x:i.in x A))

% Refs     : [Bro08] Brown (2008), Email to G. Sutcliffe
% Source   : [Bro08]
% Names    : ZFC011g [Bro08]

% Status   : Theorem
% Rating   : 0.22 v7.2.0, 0.12 v7.1.0, 0.38 v7.0.0, 0.29 v6.4.0, 0.33 v6.3.0, 0.40 v6.2.0, 0.29 v6.1.0, 0.43 v5.5.0, 0.33 v5.4.0, 0.40 v5.1.0, 0.60 v5.0.0, 0.40 v4.1.0, 0.67 v3.7.0
% Syntax   : Number of formulae    :   65 (   0 unit;  36 type;  28 defn)
%            Number of atoms       :  384 (  37 equality; 190 variable)
%            Maximal formula depth :   31 (   6 average)
%            Number of connectives :  288 (   7   ~;   3   |;  18   &; 187   @)
%                                         (   7 <=>;  66  =>;   0  <=;   0 <~>)
%                                         (   0  ~|;   0  ~&)
%            Number of type conns  :   25 (  25   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :   39 (  36   :;   0   =)
%            Number of variables   :   95 (   1 sgn;  67   !;  15   ?;  13   ^)
%                                         (  95   :;   0  !>;   0  ?*)
%                                         (   0  @-;   0  @+)
% SPC      : TH0_THM_EQU_NAR

% Comments : http://mathgate.info/detsetitem.php?id=428
%          :
%------------------------------------------------------------------------------
thf(in_type,type,(
in: \$i > \$i > \$o )).

thf(exu_type,type,(
exu: ( \$i > \$o ) > \$o )).

thf(exu,definition,
( exu
= ( ^ [Xphi: \$i > \$o] :
? [Xx: \$i] :
( ( Xphi @ Xx )
& ! [Xy: \$i] :
( ( Xphi @ Xy )
=> ( Xx = Xy ) ) ) ) )).

thf(setextAx_type,type,(
setextAx: \$o )).

thf(setextAx,definition,
( setextAx
= ( ! [A: \$i,B: \$i] :
( ! [Xx: \$i] :
( ( in @ Xx @ A )
<=> ( in @ Xx @ B ) )
=> ( A = B ) ) ) )).

thf(emptyset_type,type,(
emptyset: \$i )).

thf(emptysetAx_type,type,(
emptysetAx: \$o )).

thf(emptysetAx,definition,
( emptysetAx
= ( ! [Xx: \$i] :
~ ( in @ Xx @ emptyset ) ) )).

setadjoin: \$i > \$i > \$i )).

= ( ! [Xx: \$i,A: \$i,Xy: \$i] :
( ( in @ Xy @ ( setadjoin @ Xx @ A ) )
<=> ( ( Xy = Xx )
| ( in @ Xy @ A ) ) ) ) )).

thf(powerset_type,type,(
powerset: \$i > \$i )).

thf(powersetAx_type,type,(
powersetAx: \$o )).

thf(powersetAx,definition,
( powersetAx
= ( ! [A: \$i,B: \$i] :
( ( in @ B @ ( powerset @ A ) )
<=> ! [Xx: \$i] :
( ( in @ Xx @ B )
=> ( in @ Xx @ A ) ) ) ) )).

thf(setunion_type,type,(
setunion: \$i > \$i )).

thf(setunionAx_type,type,(
setunionAx: \$o )).

thf(setunionAx,definition,
( setunionAx
= ( ! [A: \$i,Xx: \$i] :
( ( in @ Xx @ ( setunion @ A ) )
<=> ? [B: \$i] :
( ( in @ Xx @ B )
& ( in @ B @ A ) ) ) ) )).

thf(omega_type,type,(
omega: \$i )).

thf(omega0Ax_type,type,(
omega0Ax: \$o )).

thf(omega0Ax,definition,
( omega0Ax
= ( in @ emptyset @ omega ) )).

thf(omegaSAx_type,type,(
omegaSAx: \$o )).

thf(omegaSAx,definition,
( omegaSAx
= ( ! [Xx: \$i] :
( ( in @ Xx @ omega )
=> ( in @ ( setadjoin @ Xx @ Xx ) @ omega ) ) ) )).

thf(omegaIndAx_type,type,(
omegaIndAx: \$o )).

thf(omegaIndAx,definition,
( omegaIndAx
= ( ! [A: \$i] :
( ( ( in @ emptyset @ A )
& ! [Xx: \$i] :
( ( ( in @ Xx @ omega )
& ( in @ Xx @ A ) )
=> ( in @ ( setadjoin @ Xx @ Xx ) @ A ) ) )
=> ! [Xx: \$i] :
( ( in @ Xx @ omega )
=> ( in @ Xx @ A ) ) ) ) )).

thf(replAx_type,type,(
replAx: \$o )).

thf(replAx,definition,
( replAx
= ( ! [Xphi: \$i > \$i > \$o,A: \$i] :
( ! [Xx: \$i] :
( ( in @ Xx @ A )
=> ( exu
@ ^ [Xy: \$i] :
( Xphi @ Xx @ Xy ) ) )
=> ? [B: \$i] :
! [Xx: \$i] :
( ( in @ Xx @ B )
<=> ? [Xy: \$i] :
( ( in @ Xy @ A )
& ( Xphi @ Xy @ Xx ) ) ) ) ) )).

thf(foundationAx_type,type,(
foundationAx: \$o )).

thf(foundationAx,definition,
( foundationAx
= ( ! [A: \$i] :
( ? [Xx: \$i] :
( in @ Xx @ A )
=> ? [B: \$i] :
( ( in @ B @ A )
& ~ ( ? [Xx: \$i] :
( ( in @ Xx @ B )
& ( in @ Xx @ A ) ) ) ) ) ) )).

thf(wellorderingAx_type,type,(
wellorderingAx: \$o )).

thf(wellorderingAx,definition,
( wellorderingAx
= ( ! [A: \$i] :
? [B: \$i] :
( ! [C: \$i] :
( ( in @ C @ B )
=> ! [Xx: \$i] :
( ( in @ Xx @ C )
=> ( in @ Xx @ A ) ) )
& ! [Xx: \$i,Xy: \$i] :
( ( ( in @ Xx @ A )
& ( in @ Xy @ A ) )
=> ( ! [C: \$i] :
( ( in @ C @ B )
=> ( ( in @ Xx @ C )
<=> ( in @ Xy @ C ) ) )
=> ( Xx = Xy ) ) )
& ! [C: \$i,D: \$i] :
( ( ( in @ C @ B )
& ( in @ D @ B ) )
=> ( ! [Xx: \$i] :
( ( in @ Xx @ C )
=> ( in @ Xx @ D ) )
| ! [Xx: \$i] :
( ( in @ Xx @ D )
=> ( in @ Xx @ C ) ) ) )
& ! [C: \$i] :
( ( ! [Xx: \$i] :
( ( in @ Xx @ C )
=> ( in @ Xx @ A ) )
& ? [Xx: \$i] :
( in @ Xx @ C ) )
=> ? [D: \$i,Xx: \$i] :
( ( in @ D @ B )
& ( in @ Xx @ C )
& ~ ( ? [Xy: \$i] :
( ( in @ Xy @ D )
& ( in @ Xy @ C ) ) )
& ! [E: \$i] :
( ( in @ E @ B )
=> ( ! [Xy: \$i] :
( ( in @ Xy @ E )
=> ( in @ Xy @ D ) )
| ( in @ Xx @ E ) ) ) ) ) ) ) )).

thf(descr_type,type,(
descr: ( \$i > \$o ) > \$i )).

thf(descrp_type,type,(
descrp: \$o )).

thf(descrp,definition,
( descrp
= ( ! [Xphi: \$i > \$o] :
( ( exu
@ ^ [Xx: \$i] :
( Xphi @ Xx ) )
=> ( Xphi
@ ( descr
@ ^ [Xx: \$i] :
( Xphi @ Xx ) ) ) ) ) )).

thf(dsetconstr_type,type,(
dsetconstr: \$i > ( \$i > \$o ) > \$i )).

thf(dsetconstrI_type,type,(
dsetconstrI: \$o )).

thf(dsetconstrI,definition,
( dsetconstrI
= ( ! [A: \$i,Xphi: \$i > \$o,Xx: \$i] :
( ( in @ Xx @ A )
=> ( ( Xphi @ Xx )
=> ( in @ Xx
@ ( dsetconstr @ A
@ ^ [Xy: \$i] :
( Xphi @ Xy ) ) ) ) ) ) )).

thf(dsetconstrEL_type,type,(
dsetconstrEL: \$o )).

thf(dsetconstrEL,definition,
( dsetconstrEL
= ( ! [A: \$i,Xphi: \$i > \$o,Xx: \$i] :
( ( in @ Xx
@ ( dsetconstr @ A
@ ^ [Xy: \$i] :
( Xphi @ Xy ) ) )
=> ( in @ Xx @ A ) ) ) )).

thf(dsetconstrER_type,type,(
dsetconstrER: \$o )).

thf(dsetconstrER,definition,
( dsetconstrER
= ( ! [A: \$i,Xphi: \$i > \$o,Xx: \$i] :
( ( in @ Xx
@ ( dsetconstr @ A
@ ^ [Xy: \$i] :
( Xphi @ Xy ) ) )
=> ( Xphi @ Xx ) ) ) )).

thf(exuE1_type,type,(
exuE1: \$o )).

thf(exuE1,definition,
( exuE1
= ( ! [Xphi: \$i > \$o] :
( ( exu
@ ^ [Xx: \$i] :
( Xphi @ Xx ) )
=> ? [Xx: \$i] :
( ( Xphi @ Xx )
& ! [Xy: \$i] :
( ( Xphi @ Xy )
=> ( Xx = Xy ) ) ) ) ) )).

thf(prop2set_type,type,(
prop2set: \$o > \$i )).

thf(prop2set,definition,
( prop2set
= ( ^ [Xphi: \$o] :
( dsetconstr @ ( powerset @ emptyset )
@ ^ [Xx: \$i] : Xphi ) ) )).

thf(prop2setE_type,type,(
prop2setE: \$o )).

thf(prop2setE,definition,
( prop2setE
= ( ! [Xphi: \$o,Xx: \$i] :
( ( in @ Xx @ ( prop2set @ Xphi ) )
=> Xphi ) ) )).

thf(emptysetE_type,type,(
emptysetE: \$o )).

thf(emptysetE,definition,
( emptysetE
= ( ! [Xx: \$i] :
( ( in @ Xx @ emptyset )
=> ! [Xphi: \$o] : Xphi ) ) )).

thf(emptysetimpfalse_type,type,(
emptysetimpfalse: \$o )).

thf(emptysetimpfalse,definition,
( emptysetimpfalse
= ( ! [Xx: \$i] :
( ( in @ Xx @ emptyset )
=> \$false ) ) )).

thf(notinemptyset_type,type,(
notinemptyset: \$o )).

thf(notinemptyset,definition,
( notinemptyset
= ( ! [Xx: \$i] :
~ ( in @ Xx @ emptyset ) ) )).

thf(exuE3e_type,type,(
exuE3e: \$o )).

thf(exuE3e,definition,
( exuE3e
= ( ! [Xphi: \$i > \$o] :
( ( exu
@ ^ [Xx: \$i] :
( Xphi @ Xx ) )
=> ? [Xx: \$i] :
( Xphi @ Xx ) ) ) )).

thf(setext_type,type,(
setext: \$o )).

thf(setext,definition,
( setext
= ( ! [A: \$i,B: \$i] :
( ! [Xx: \$i] :
( ( in @ Xx @ A )
=> ( in @ Xx @ B ) )
=> ( ! [Xx: \$i] :
( ( in @ Xx @ B )
=> ( in @ Xx @ A ) )
=> ( A = B ) ) ) ) )).

thf(emptyI_type,type,(
emptyI: \$o )).

thf(emptyI,definition,
( emptyI
= ( ! [A: \$i] :
( ! [Xx: \$i] :
~ ( in @ Xx @ A )
=> ( A = emptyset ) ) ) )).

thf(noeltsimpempty_type,type,(
noeltsimpempty: \$o )).

thf(noeltsimpempty,definition,
( noeltsimpempty
= ( ! [A: \$i] :
( ! [Xx: \$i] :
~ ( in @ Xx @ A )
=> ( A = emptyset ) ) ) )).

thf(setbeta_type,type,(
setbeta: \$o )).

thf(setbeta,definition,
( setbeta
= ( ! [A: \$i,Xphi: \$i > \$o,Xx: \$i] :
( ( in @ Xx @ A )
=> ( ( in @ Xx
@ ( dsetconstr @ A
@ ^ [Xy: \$i] :
( Xphi @ Xy ) ) )
<=> ( Xphi @ Xx ) ) ) ) )).

thf(nonempty_type,type,(
nonempty: \$i > \$o )).

thf(nonempty,definition,
( nonempty
= ( ^ [Xx: \$i] : ( Xx != emptyset ) ) )).

thf(nonemptyE1,conjecture,
( setextAx
=> ( emptysetAx
=> ( powersetAx
=> ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ! [A: \$i] :
( ( nonempty @ A )
=> ? [Xx: \$i] :
( in @ Xx @ A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )).

%------------------------------------------------------------------------------
```