let p, q be Element of HP-WFF ; :: thesis: for V being SetValuation
for P being Permutation of V st ex f being set st f is_a_fixpoint_of Perm P,p & ( for f being set holds not f is_a_fixpoint_of Perm P,q ) holds
not p => q is pseudo-canonical
let V be SetValuation; :: thesis: for P being Permutation of V st ex f being set st f is_a_fixpoint_of Perm P,p & ( for f being set holds not f is_a_fixpoint_of Perm P,q ) holds
not p => q is pseudo-canonical
let P be Permutation of V; :: thesis: ( ex f being set st f is_a_fixpoint_of Perm P,p & ( for f being set holds not f is_a_fixpoint_of Perm P,q ) implies not p => q is pseudo-canonical )
given x being set such that A1: x is_a_fixpoint_of Perm P,p ; :: thesis: ( ex f being set st f is_a_fixpoint_of Perm P,q or not p => q is pseudo-canonical )
assume A2: for x being set holds not x is_a_fixpoint_of Perm P,q ; :: thesis: not p => q is pseudo-canonical
assume p => q is pseudo-canonical ; :: thesis: contradiction
then consider f being set such that
A3: f is_a_fixpoint_of Perm P,(p => q) by Def8;
f in dom (Perm P,(p => q)) by A3, ABIAN:def 3;
then f in SetVal V,(p => q) by FUNCT_2:def 1;
then reconsider f = f as Function ;
f . x is_a_fixpoint_of Perm P,q by A1, A3, Th40;
hence contradiction by A2; :: thesis: verum