consider G0 being Element of V;
set M = Morphs G0,G0;
set S = { (Morphs G,H) where G, H is Element of V : G <= H } ;
A1:
ID G0 is Element of Morphs G0,G0
by Def15;
Morphs G0,G0 in { (Morphs G,H) where G, H is Element of V : G <= H }
;
then reconsider T = union { (Morphs G,H) where G, H is Element of V : G <= H } as non empty set by A1, TARSKI:def 4;
A2:
for x being set holds
( x in T iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) )
proof
let x be
set ;
:: thesis: ( x in T iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) )
thus
(
x in T implies ex
G,
H being
Element of
V st
(
G <= H &
x is
Morphism of
G,
H ) )
:: thesis: ( ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) implies x in T )proof
assume
x in T
;
:: thesis: ex G, H being Element of V st
( G <= H & x is Morphism of G,H )
then consider Y being
set such that A3:
x in Y
and A4:
Y in { (Morphs G,H) where G, H is Element of V : G <= H }
by TARSKI:def 4;
consider G,
H being
Element of
V such that A5:
Y = Morphs G,
H
and A6:
G <= H
by A4;
A7:
x is
Element of
Morphs G,
H
by A3, A5;
take
G
;
:: thesis: ex H being Element of V st
( G <= H & x is Morphism of G,H )
take
H
;
:: thesis: ( G <= H & x is Morphism of G,H )
thus
(
G <= H &
x is
Morphism of
G,
H )
by A6, A7;
:: thesis: verum
end;
thus
( ex
G,
H being
Element of
V st
(
G <= H &
x is
Morphism of
G,
H ) implies
x in T )
:: thesis: verumproof
given G,
H being
Element of
V such that A8:
G <= H
and A9:
x is
Morphism of
G,
H
;
:: thesis: x in T
set M =
Morphs G,
H;
A10:
x in Morphs G,
H
by A8, A9, Def15;
Morphs G,
H in { (Morphs G,H) where G, H is Element of V : G <= H }
by A8;
hence
x in T
by A10, TARSKI:def 4;
:: thesis: verum
end;
end;
then reconsider T' = T as RingMorphism_DOMAIN by Def13;
take
T'
; :: thesis: for x being set holds
( x in T' iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) )
thus
for x being set holds
( x in T' iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) )
by A2; :: thesis: verum