let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for R being Subset of (CongrLatt A)
for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds
meet |:F:| is MSCongruence of A
let A be non-empty MSAlgebra over S; for R being Subset of (CongrLatt A)
for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds
meet |:F:| is MSCongruence of A
let R be Subset of (CongrLatt A); for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds
meet |:F:| is MSCongruence of A
let F be SubsetFamily of [| the Sorts of A, the Sorts of A|]; ( R = F implies meet |:F:| is MSCongruence of A )
assume A1:
R = F
; meet |:F:| is MSCongruence of A
set R0 = meet |:F:|;
set SF = the Sorts of A;
set I = the carrier of S;
per cases
( not F is empty or F is empty )
;
suppose
not
F is
empty
;
meet |:F:| is MSCongruence of Athen reconsider F1 =
F as non
empty SubsetFamily of
[| the Sorts of A, the Sorts of A|] ;
A2:
F1 c= the
carrier of
(EqRelLatt the Sorts of A)
then A3:
meet |:F:| is
MSEquivalence_Relation-like ManySortedRelation of the
Sorts of
A
by MSUALG_7:8;
reconsider R0 =
meet |:F:| as
ManySortedRelation of
A by A2, MSUALG_7:8;
R0 is
MSEquivalence-like
by A3;
then reconsider R0 =
R0 as
MSEquivalence-like ManySortedRelation of
A ;
now for o being OperSymbol of S
for a, b being Element of Args (o,A) st ( for n being Nat st n in dom a holds
[(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o)let o be
OperSymbol of
S;
for a, b being Element of Args (o,A) st ( for n being Nat st n in dom a holds
[(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o)let a,
b be
Element of
Args (
o,
A);
( ( for n being Nat st n in dom a holds
[(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o) )assume A4:
for
n being
Nat st
n in dom a holds
[(a . n),(b . n)] in R0 . ((the_arity_of o) /. n)
;
[((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o)set r =
the_result_sort_of o;
consider Q being
Subset-Family of
([| the Sorts of A, the Sorts of A|] . (the_result_sort_of o)) such that A5:
Q = |:F1:| . (the_result_sort_of o)
and A6:
R0 . (the_result_sort_of o) = Intersect Q
by MSSUBFAM:def 1;
A7:
Q = { (s . (the_result_sort_of o)) where s is Element of Bool [| the Sorts of A, the Sorts of A|] : s in F1 }
by A5, CLOSURE2:14;
now for Y being set st Y in Q holds
[((Den (o,A)) . a),((Den (o,A)) . b)] in Ylet Y be
set ;
( Y in Q implies [((Den (o,A)) . a),((Den (o,A)) . b)] in Y )assume
Y in Q
;
[((Den (o,A)) . a),((Den (o,A)) . b)] in Ythen consider s being
Element of
Bool [| the Sorts of A, the Sorts of A|] such that A8:
Y = s . (the_result_sort_of o)
and A9:
s in F1
by A7;
reconsider s =
s as
MSCongruence of
A by A1, A9, MSUALG_5:def 6;
now for n being Nat st n in dom a holds
[(a . n),(b . n)] in s . ((the_arity_of o) /. n)let n be
Nat;
( n in dom a implies [(a . n),(b . n)] in s . ((the_arity_of o) /. n) )assume A10:
n in dom a
;
[(a . n),(b . n)] in s . ((the_arity_of o) /. n)set t =
(the_arity_of o) /. n;
consider G being
Subset-Family of
([| the Sorts of A, the Sorts of A|] . ((the_arity_of o) /. n)) such that A11:
G = |:F1:| . ((the_arity_of o) /. n)
and A12:
R0 . ((the_arity_of o) /. n) = Intersect G
by MSSUBFAM:def 1;
G = { (j . ((the_arity_of o) /. n)) where j is Element of Bool [| the Sorts of A, the Sorts of A|] : j in F1 }
by A11, CLOSURE2:14;
then A13:
s . ((the_arity_of o) /. n) in G
by A9;
[(a . n),(b . n)] in Intersect G
by A4, A10, A12;
then
[(a . n),(b . n)] in meet G
by A11, SETFAM_1:def 9;
hence
[(a . n),(b . n)] in s . ((the_arity_of o) /. n)
by A13, SETFAM_1:def 1;
verum end; hence
[((Den (o,A)) . a),((Den (o,A)) . b)] in Y
by A8, MSUALG_4:def 4;
verum end; then
[((Den (o,A)) . a),((Den (o,A)) . b)] in meet Q
by A5, SETFAM_1:def 1;
hence
[((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o)
by A5, A6, SETFAM_1:def 9;
verum end; hence
meet |:F:| is
MSCongruence of
A
by MSUALG_4:def 4;
verum end; end;