let A be category; for a being Object of A
for x being set holds
( x in (Concretized A) -carrier_of a iff ex b being Object of A ex f being Morphism of b,a st
( <^b,a^> <> {} & x = [f,[b,a]] ) )
let a be Object of A; for x being set holds
( x in (Concretized A) -carrier_of a iff ex b being Object of A ex f being Morphism of b,a st
( <^b,a^> <> {} & x = [f,[b,a]] ) )
let x be set ; ( x in (Concretized A) -carrier_of a iff ex b being Object of A ex f being Morphism of b,a st
( <^b,a^> <> {} & x = [f,[b,a]] ) )
set B = Concretized A;
reconsider ac = a as Object of (Concretized A) by Def12;
A1:
( x in the_carrier_of ac iff ( x in Union (disjoin the Arrows of A) & ac = x `22 ) )
by Def12;
A2:
dom the Arrows of A = [: the carrier of A, the carrier of A:]
by PARTFUN1:def 2;
hereby ( ex b being Object of A ex f being Morphism of b,a st
( <^b,a^> <> {} & x = [f,[b,a]] ) implies x in (Concretized A) -carrier_of a )
assume A3:
x in (Concretized A) -carrier_of a
;
ex b being Object of A ex f being Morphism of b,a st
( <^b,a^> <> {} & x = [f,[b,a]] )then A4:
x `2 in dom the
Arrows of
A
by A1, CARD_3:22;
A5:
x `1 in the
Arrows of
A . (x `2)
by A1, A3, CARD_3:22;
A6:
x = [(x `1),(x `2)]
by A1, A3, CARD_3:22;
consider b,
c being
object such that A7:
b in the
carrier of
A
and
c in the
carrier of
A
and A8:
x `2 = [b,c]
by A4, ZFMISC_1:def 2;
reconsider b =
b as
Object of
A by A7;
take b =
b;
ex f being Morphism of b,a st
( <^b,a^> <> {} & x = [f,[b,a]] )reconsider f =
x `1 as
Morphism of
b,
a by A1, A3, A5, A6, A8, MCART_1:85;
take f =
f;
( <^b,a^> <> {} & x = [f,[b,a]] )thus
(
<^b,a^> <> {} &
x = [f,[b,a]] )
by A1, A3, A5, A6, A8, MCART_1:85;
verum
end;
given b being Object of A, f being Morphism of b,a such that A9:
<^b,a^> <> {}
and
A10:
x = [f,[b,a]]
; x in (Concretized A) -carrier_of a
A11:
x `1 = f
by A10;
A12:
x `2 = [b,a]
by A10;
[b,a] in dom the Arrows of A
by A2, ZFMISC_1:def 2;
hence
x in (Concretized A) -carrier_of a
by A1, A9, A10, A11, A12, CARD_3:22, MCART_1:85; verum