:: 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;