:: SCHEMS_1 semantic presentation

begin


scheme :: SCHEMS_1:sch 1
Schemat0{ P1[ set ] } :
 ex a being set st P1[a]
provided
A1: for a being set holds P1[a]
proof
set a = the set ;
 P1[ the set ] by A1;
hence  ex a being set st P1[a] ; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 2
Schemat3{ P1[ set , set ] } :
 for b being set ex a being set st P1[a,b]
provided
A1: ex a being set st
for b being set holds P1[a,b]
proof
thus  for b being set ex a being set st P1[a,b] by A1; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 3
Schemat8{ P1[ set ], P2[ set ] } :
 ( ( for a being set holds P1[a] ) implies for a being set holds P2[a] )
provided
A1: for a being set st P1[a] holds
P2[a]
proof
thus  ( ( for a being set holds P1[a] ) implies for a being set holds P2[a] ) by A1; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 4
Schemat9{ P1[ set ], P2[ set ] } :
 ( ( for a being set holds P1[a] ) iff for a being set holds P2[a] )
provided
A1: for a being set holds
( P1[a] iff P2[a] )
proof
thus  ( ( for a being set holds P1[a] ) implies for a being set holds P2[a] ) ::_thesis: ( ( for a being set holds P2[a] ) implies for a being set holds P1[a] )
proof
assume A2: for a being set holds P1[a] ; ::_thesis: for a being set holds P2[a]
now__::_thesis:_for_a_being_set_holds_P2[a]
let a be set ; ::_thesis: P2[a]
 ( P1[a] iff P2[a] ) by A1;
hence  P2[a] by A2; ::_thesis: verum
end;
hence  for a being set holds P2[a] ; ::_thesis: verum
end;
assume A3: for a being set holds P2[a] ; ::_thesis: for a being set holds P1[a]
now__::_thesis:_for_a_being_set_holds_P1[a]
let a be set ; ::_thesis: P1[a]
 ( P1[a] iff P2[a] ) by A1;
hence  P1[a] by A3; ::_thesis: verum
end;
hence  for a being set holds P1[a] ; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 5
Schemat17{ P1[ set ], P2[] } :
 ( ( for a being set holds P1[a] ) implies P2[] )
provided
A1: for a being set st P1[a] holds
P2[]
proof
assume A2: for a being set holds P1[a] ; ::_thesis: P2[]
now__::_thesis:_for_a_being_set_holds_P2[]
let a be set ; ::_thesis: P2[]
 P1[a] by A2;
hence  P2[] by A1; ::_thesis: verum
end;
hence  P2[] ; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 6
Schemat18a{ P1[ set ], P2[ set ] } :
 ex a being set st
for b being set holds
( P1[a] or P2[b] )
provided
A1: ( ex a being set st P1[a] or for b being set holds P2[b] )
proof
now__::_thesis:_ex_a_being_set_st_
for_b_being_set_holds_
(_P1[a]_or_P2[b]_)
A2: now__::_thesis:_(_(_for_b_being_set_holds_P2[b]_)_implies_ex_a_being_set_st_
for_b_being_set_holds_
(_P1[a]_or_P2[b]_)_)
set a = the set ;
assume  for b being set holds P2[b] ; ::_thesis: ex a being set st
for b being set holds
( P1[a] or P2[b] )
then  for b being set holds
( P1[ the set ] or P2[b] ) ;
hence  ex a being set st
for b being set holds
( P1[a] or P2[b] ) ; ::_thesis: verum
end;
now__::_thesis:_(_ex_a_being_set_st_P1[a]_implies_ex_a_being_set_st_
for_b_being_set_holds_
(_P1[a]_or_P2[b]_)_)
given a being set  such that A3: P1[a] ; ::_thesis: ex a being set st
for b being set holds
( P1[a] or P2[b] )
 for b being set holds
( P1[a] or P2[b] ) by A3;
hence  ex a being set st
for b being set holds
( P1[a] or P2[b] ) ; ::_thesis: verum
end;
hence  ex a being set st
for b being set holds
( P1[a] or P2[b] ) by A1, A2; ::_thesis: verum
end;
hence  ex a being set st
for b being set holds
( P1[a] or P2[b] ) ; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 7
Schemat18b{ P1[ set ], P2[ set ] } :
 ( ex a being set st P1[a] or for b being set holds P2[b] )
provided
A1: ex a being set st
for b being set holds
( P1[a] or P2[b] )
proof
thus  ( ex a being set st P1[a] or for b being set holds P2[b] ) by A1; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 8
Schemat20b{ P1[ set ], P2[ set ] } :
 ex a being set st
for b being set holds
( P1[a] or P2[b] )
provided
A1: for b being set ex a being set st
( P1[a] or P2[b] )
proof
A2: ( ex a being set st P1[a] or for b being set holds P2[b] ) by A1;
 ex a being set st
for b being set holds
( P1[a] or P2[b] ) from SCHEMS_1:sch_6(A2);
hence  ex a being set st
for b being set holds
( P1[a] or P2[b] ) ; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 9
Schemat22a{ P1[ set ], P2[ set ] } :
 for b being set ex a being set st
( P1[a] & P2[b] )
provided
A1: ( ex a being set st P1[a] & ( for b being set holds P2[b] ) )
proof
thus  for b being set ex a being set st
( P1[a] & P2[b] ) by A1; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 10
Schemat22b{ P1[ set ], P2[ set ] } :
 ( ex a being set st P1[a] & ( for b being set holds P2[b] ) )
provided
A1: for b being set ex a being set st
( P1[a] & P2[b] )
proof
assume A2: ( for a being set holds P1[a] or ex b being set st P2[b] ) ; ::_thesis: contradiction
percases ( ex b being set st P2[b] or for a being set holds P1[a] ) by A2;
suppose not for b being set holds P2[b] ; ::_thesis: contradiction
then consider b being set  such that
A3: P2[b] ;
now__::_thesis:_for_d_being_set_holds_not_d_=_b
let d be set ; ::_thesis: not d = b
assume  d = b ; ::_thesis: contradiction
 ex a being set st
( P1[a] & P2[b] ) by A1;
hence  contradiction by A3; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;
supposeA4: for a being set holds P1[a] ; ::_thesis: contradiction
now__::_thesis:_for_b_being_set_holds_contradiction
let b be set ; ::_thesis: contradiction
 ex a being set st
( P1[a] & P2[b] ) by A1;
hence  contradiction by A4; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;

scheme :: SCHEMS_1:sch 11
Schemat23b{ P1[ set ], P2[ set ] } :
 ex a being set st
for b being set holds
( P1[a] & P2[b] )
provided
A1: for b being set ex a being set st
( P1[a] & P2[b] )
proof
A2: for b being set ex a being set st
( P1[a] & P2[b] ) by A1;
 ( ex a being set st P1[a] & ( for b being set holds P2[b] ) ) from SCHEMS_1:sch_10(A2);
hence  ex a being set st
for b being set holds
( P1[a] & P2[b] ) ; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 12
Schemat28{ P1[ set , set ] } :
 ex b being set st
for a being set holds P1[a,b]
provided
A1: for a, b being set holds P1[a,b]
proof
now__::_thesis:_for_b_being_set_ex_b_being_set_st_
for_a_being_set_holds_P1[a,b]
let b be set ; ::_thesis: ex b being set st
for a being set holds P1[a,b]
 for a being set holds P1[a,b] by A1;
hence  ex b being set st
for a being set holds P1[a,b] ; ::_thesis: verum
end;
hence  ex b being set st
for a being set holds P1[a,b] ; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 13
Schemat30{ P1[ set , set ] } :
 ex a being set st P1[a,a]
provided
A1: ex a being set st
for b being set holds P1[a,b]
proof
thus  ex a being set st P1[a,a] by A1; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 14
Schemat31{ P1[ set , set ] } :
 for a being set ex b being set st P1[b,a]
provided
A1: for a being set holds P1[a,a]
proof
thus  for a being set ex b being set st P1[b,a] by A1; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 15
Schemat33{ P1[ set , set ] } :
 for a being set ex b being set st P1[a,b]
provided
A1: for a being set holds P1[a,a]
proof
thus  for a being set ex b being set st P1[a,b] by A1; ::_thesis: verum
end;

scheme :: SCHEMS_1:sch 16
Schemat36{ P1[ set , set ] } :
 ex a, b being set st P1[a,b]
provided
A1: for b being set ex a being set st P1[a,b]
proof
set b = the set ;
 ex a being set st P1[a, the set ] by A1;
hence  ex a, b being set st P1[a,b] ; ::_thesis: verum
end;