let V, V9, C, C9 be set ; for A being Element of Fin (PFuncs (V,C))
for B being Element of Fin (PFuncs (V9,C9)) st V c= V9 & C c= C9 & A = B holds
mi A = mi B
let A be Element of Fin (PFuncs (V,C)); for B being Element of Fin (PFuncs (V9,C9)) st V c= V9 & C c= C9 & A = B holds
mi A = mi B
let B be Element of Fin (PFuncs (V9,C9)); ( V c= V9 & C c= C9 & A = B implies mi A = mi B )
assume that
A1:
( V c= V9 & C c= C9 )
and
A2:
A = B
; mi A = mi B
hereby TARSKI:def 3,
XBOOLE_0:def 10 mi B c= mi A
let x be
object ;
( x in mi A implies x in mi B )A3:
PFuncs (
V,
C)
c= PFuncs (
V9,
C9)
by A1, PARTFUN1:50;
assume A4:
x in mi A
;
x in mi Bthen
x in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) }
by SUBSTLAT:def 2;
then consider f being
Element of
PFuncs (
V,
C)
such that A5:
f = x
and A6:
f is
finite
and
for
s being
Element of
PFuncs (
V,
C) holds
( (
s in A &
s c= f ) iff
s = f )
;
reconsider f =
f as
Element of
PFuncs (
V9,
C9)
by A3;
for
s being
Element of
PFuncs (
V9,
C9) holds
( (
s in B &
s c= f ) iff
s = f )
by A2, A4, A5, SUBSTLAT:6;
then
x in { t where t is Element of PFuncs (V9,C9) : ( t is finite & ( for s being Element of PFuncs (V9,C9) holds
( ( s in B & s c= t ) iff s = t ) ) ) }
by A5, A6;
hence
x in mi B
by SUBSTLAT:def 2;
verum
end;
let x be object ; TARSKI:def 3 ( not x in mi B or x in mi A )
assume A7:
x in mi B
; x in mi A
then
x in { t where t is Element of PFuncs (V9,C9) : ( t is finite & ( for s being Element of PFuncs (V9,C9) holds
( ( s in B & s c= t ) iff s = t ) ) ) }
by SUBSTLAT:def 2;
then
ex f being Element of PFuncs (V9,C9) st
( f = x & f is finite & ( for s being Element of PFuncs (V9,C9) holds
( ( s in B & s c= f ) iff s = f ) ) )
;
then reconsider x9 = x as finite set ;
( mi B c= B & ( for b being finite set st b in A & b c= x9 holds
b = x9 ) )
by A2, A7, SUBSTLAT:6;
hence
x in mi A
by A2, A7, SUBSTLAT:7; verum