:: Predicate Calculus for Boolean Valued Functions, II
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Copyright (c) 1999-2021 Association of Mizar Users

theorem :: BVFUNC_4:1
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a '<' b 'imp' c holds
a '&' b '<' c
proof end;

theorem :: BVFUNC_4:2
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds
a '<' b 'imp' c
proof end;

theorem :: BVFUNC_4:3
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' (a '&' b) = a
proof end;

theorem :: BVFUNC_4:4
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' (a 'or' b) = a
proof end;

theorem Th5: :: BVFUNC_4:5
for Y being non empty set
for a being Function of Y,BOOLEAN holds a '&' () = O_el Y
proof end;

theorem :: BVFUNC_4:6
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'or' () = I_el Y
proof end;

theorem Th7: :: BVFUNC_4:7
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'imp' b) '&' (b 'imp' a)
proof end;

theorem Th8: :: BVFUNC_4:8
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' b = () 'or' b
proof end;

theorem :: BVFUNC_4:9
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = (() '&' b) 'or' (a '&' ())
proof end;

theorem Th10: :: BVFUNC_4:10
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a 'eqv' b = I_el Y iff ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) )
proof end;

theorem :: BVFUNC_4:11
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a 'eqv' b = I_el Y holds
() 'eqv' () = I_el Y
proof end;

theorem :: BVFUNC_4:12
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a '&' c) 'eqv' (b '&' d) = I_el Y
proof end;

theorem :: BVFUNC_4:13
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a 'imp' c) 'eqv' (b 'imp' d) = I_el Y
proof end;

theorem :: BVFUNC_4:14
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a 'or' c) 'eqv' (b 'or' d) = I_el Y
proof end;

theorem :: BVFUNC_4:15
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds
(a 'eqv' c) 'eqv' (b 'eqv' d) = I_el Y
proof end;

::Chap. 2 Predicate Calculus
theorem :: BVFUNC_4:16
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of ()
for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))
proof end;

theorem :: BVFUNC_4:17
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of ()
for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G)
proof end;

theorem :: BVFUNC_4:18
for Y being non empty set
for a, u being Function of Y,BOOLEAN
for G being Subset of ()
for PA being a_partition of Y st a 'imp' u = I_el Y holds
(All (a,PA,G)) 'imp' u = I_el Y
proof end;

theorem :: BVFUNC_4:19
for Y being non empty set
for u being Function of Y,BOOLEAN
for G being Subset of ()
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex (u,PA,G) '<' u
proof end;

theorem :: BVFUNC_4:20
for Y being non empty set
for u being Function of Y,BOOLEAN
for G being Subset of ()
for PA being a_partition of Y st u is_independent_of PA,G holds
u '<' All (u,PA,G)
proof end;

theorem :: BVFUNC_4:21
for Y being non empty set
for u being Function of Y,BOOLEAN
for G being Subset of ()
for PA, PB being a_partition of Y st u is_independent_of PB,G holds
All (u,PA,G) '<' All (u,PB,G)
proof end;

theorem :: BVFUNC_4:22
for Y being non empty set
for u being Function of Y,BOOLEAN
for G being Subset of ()
for PA, PB being a_partition of Y st u is_independent_of PA,G holds
Ex (u,PA,G) '<' Ex (u,PB,G)
proof end;

theorem :: BVFUNC_4:23
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of ()
for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) '<' (All (a,PA,G)) 'eqv' (All (b,PA,G))
proof end;

theorem :: BVFUNC_4:24
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of ()
for PA being a_partition of Y holds All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G))
proof end;

theorem :: BVFUNC_4:25
for Y being non empty set
for a, u being Function of Y,BOOLEAN
for G being Subset of ()
for PA being a_partition of Y holds (All (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G)
proof end;

theorem :: BVFUNC_4:26
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of ()
for PA being a_partition of Y st a 'eqv' b = I_el Y holds
(All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y
proof end;

theorem :: BVFUNC_4:27
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of ()
for PA being a_partition of Y st a 'eqv' b = I_el Y holds
(Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y
proof end;