set F = { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_isomorphism } ;
A1: id the carrier of UA in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_isomorphism }
proof
set I = id the carrier of UA;
( id the carrier of UA in Funcs ( the carrier of UA, the carrier of UA) & id the carrier of UA is_isomorphism ) by Th1, FUNCT_2:8;
hence id the carrier of UA in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_isomorphism } ; :: thesis: verum
end;
reconsider F = { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_isomorphism } as set ;
F is functional
proof
let q be object ; :: according to FUNCT_1:def 13 :: thesis: ( not q in F or q is set )
assume q in F ; :: thesis: q is set
then ex x being Element of Funcs ( the carrier of UA, the carrier of UA) st
( q = x & x is_isomorphism ) ;
hence q is set ; :: thesis: verum
end;
then reconsider F = F as functional non empty set by A1;
F is FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
proof
let a be Element of F; :: according to FUNCT_2:def 12 :: thesis: a is Element of bool [: the carrier of UA, the carrier of UA:]
a in F ;
then ex x being Element of Funcs ( the carrier of UA, the carrier of UA) st
( a = x & x is_isomorphism ) ;
hence a is Element of bool [: the carrier of UA, the carrier of UA:] ; :: thesis: verum
end;
then reconsider F = F as FUNCTION_DOMAIN of the carrier of UA, the carrier of UA ;
take F ; :: thesis: for h being Function of UA,UA holds
( h in F iff h is_isomorphism )
let h be Function of UA,UA; :: thesis: ( h in F iff h is_isomorphism )
thus ( h in F implies h is_isomorphism ) :: thesis: ( h is_isomorphism implies h in F )
proof
assume h in F ; :: thesis: h is_isomorphism
then ex f being Element of Funcs ( the carrier of UA, the carrier of UA) st
( f = h & f is_isomorphism ) ;
hence h is_isomorphism ; :: thesis: verum
end;
A2: h is Element of Funcs ( the carrier of UA, the carrier of UA) by FUNCT_2:8;
assume h is_isomorphism ; :: thesis: h in F
hence h in F by A2; :: thesis: verum