let Y be non empty set ; for G being Subset of (PARTITIONS Y)
for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G))
let G be Subset of (PARTITIONS Y); for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G))
let a, u be Function of Y,BOOLEAN; for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G))
let PA be a_partition of Y; ( u is_independent_of PA,G implies Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G)) )
assume A1:
u is_independent_of PA,G
; Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G))
A2:
Ex ((u 'or' a),PA,G) '<' u 'or' (Ex (a,PA,G))
proof
let z be
Element of
Y;
BVFUNC_1:def 12 ( not (Ex ((u 'or' a),PA,G)) . z = TRUE or (u 'or' (Ex (a,PA,G))) . z = TRUE )
A3:
z in EqClass (
z,
(CompF (PA,G)))
by EQREL_1:def 6;
A4:
(u 'or' (Ex (a,PA,G))) . z = (u . z) 'or' ((Ex (a,PA,G)) . z)
by BVFUNC_1:def 4;
assume
(Ex ((u 'or' a),PA,G)) . z = TRUE
;
(u 'or' (Ex (a,PA,G))) . z = TRUE
then consider x1 being
Element of
Y such that A5:
x1 in EqClass (
z,
(CompF (PA,G)))
and A6:
(u 'or' a) . x1 = TRUE
by BVFUNC_1:def 17;
A7:
(
u . x1 = TRUE or
u . x1 = FALSE )
by XBOOLEAN:def 3;
A8:
(u . x1) 'or' (a . x1) = TRUE
by A6, BVFUNC_1:def 4;
hence
(u 'or' (Ex (a,PA,G))) . z = TRUE
;
verum
end;
u 'or' (Ex (a,PA,G)) '<' Ex ((u 'or' a),PA,G)
proof
let z be
Element of
Y;
BVFUNC_1:def 12 ( not (u 'or' (Ex (a,PA,G))) . z = TRUE or (Ex ((u 'or' a),PA,G)) . z = TRUE )
A10:
z in EqClass (
z,
(CompF (PA,G)))
by EQREL_1:def 6;
assume
(u 'or' (Ex (a,PA,G))) . z = TRUE
;
(Ex ((u 'or' a),PA,G)) . z = TRUE
then A11:
(u . z) 'or' ((Ex (a,PA,G)) . z) = TRUE
by BVFUNC_1:def 4;
A12:
(
(Ex (a,PA,G)) . z = TRUE or
(Ex (a,PA,G)) . z = FALSE )
by XBOOLEAN:def 3;
hence
(Ex ((u 'or' a),PA,G)) . z = TRUE
;
verum
end;
hence
Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G))
by A2, BVFUNC_1:15; verum