hereby :: thesis: ( ( for o being object of A holds the ObjectMap of F . o,o = [(F . o),(F . o)] ) implies F is reflexive )
assume
F is
reflexive
;
:: thesis: for o being object of A holds the ObjectMap of F . o,o = [(F . o),(F . o)]then A1:
the
ObjectMap of
F .: (id the carrier of A) c= id the
carrier of
B
by Def9;
let o be
object of
A;
:: thesis: the ObjectMap of F . o,o = [(F . o),(F . o)]
[o,o] in id the
carrier of
A
by RELAT_1:def 10;
then A2:
the
ObjectMap of
F . o,
o in the
ObjectMap of
F .: (id the carrier of A)
by FUNCT_2:43;
consider p,
p' being
set such that A3:
the
ObjectMap of
F . o,
o = [p,p']
by RELAT_1:def 1;
F . o = p
by A3, MCART_1:7;
hence
the
ObjectMap of
F . o,
o = [(F . o),(F . o)]
by A1, A2, A3, RELAT_1:def 10;
:: thesis: verum
end;
assume A4:
for o being object of A holds the ObjectMap of F . o,o = [(F . o),(F . o)]
; :: thesis: F is reflexive
let x be set ; :: according to TARSKI:def 3,FUNCTOR0:def 9 :: thesis: ( not x in the ObjectMap of F .: (id the carrier of A) or x in id the carrier of B )
assume
x in the ObjectMap of F .: (id the carrier of A)
; :: thesis: x in id the carrier of B
then consider y being set such that
A5:
y in [:the carrier of A,the carrier of A:]
and
A6:
y in id the carrier of A
and
A7:
x = the ObjectMap of F . y
by FUNCT_2:115;
consider o, o' being Element of A such that
A8:
y = [o,o']
by A5, DOMAIN_1:9;
reconsider o = o as object of A ;
o = o'
by A6, A8, RELAT_1:def 10;
then
x = [(F . o),(F . o)]
by A4, A7, A8;
hence
x in id the carrier of B
by RELAT_1:def 10; :: thesis: verum