let A, B be set ; (id A) | B = (id A) /\ [:B,B:]
thus
(id A) | B c= (id A) /\ [:B,B:]
XBOOLE_0:def 10 (id A) /\ [:B,B:] c= (id A) | Bproof
let a be
object ;
TARSKI:def 3 ( not a in (id A) | B or a in (id A) /\ [:B,B:] )
assume A1:
a in (id A) | B
;
a in (id A) /\ [:B,B:]
(id A) | B is
Relation of
B,
A
by RELSET_1:18;
then consider x,
y being
object such that A2:
a = [x,y]
and A3:
x in B
and
y in A
by A1, RELSET_1:2;
A4:
[x,y] in id A
by A1, A2, RELAT_1:def 11;
then
x = y
by RELAT_1:def 10;
then
[x,y] in [:B,B:]
by A3, ZFMISC_1:87;
hence
a in (id A) /\ [:B,B:]
by A2, A4, XBOOLE_0:def 4;
verum
end;
let a be object ; TARSKI:def 3 ( not a in (id A) /\ [:B,B:] or a in (id A) | B )
assume A5:
a in (id A) /\ [:B,B:]
; a in (id A) | B
then
a in [:B,B:]
by XBOOLE_0:def 4;
then A6:
ex x1, y1 being object st
( x1 in B & y1 in B & a = [x1,y1] )
by ZFMISC_1:def 2;
a in id A
by A5, XBOOLE_0:def 4;
hence
a in (id A) | B
by A6, RELAT_1:def 11; verum