let a, b be set ; ( a <> b iff {[a,b]} misses {[a,a],[b,b]} )
thus
( a <> b implies {[a,b]} misses {[a,a],[b,b]} )
( {[a,b]} misses {[a,a],[b,b]} implies a <> b )proof
assume A0:
a <> b
;
{[a,b]} misses {[a,a],[b,b]}
then A1:
[a,b] <> [a,a]
by XTUPLE_0:1;
A2:
[a,b] <> [b,b]
by A0, XTUPLE_0:1;
set A =
{[a,b]};
set B =
{[a,a],[b,b]};
assume
{[a,b]} meets {[a,a],[b,b]}
;
contradiction
then consider x being
object such that A4:
(
x in {[a,b]} &
x in {[a,a],[b,b]} )
by XBOOLE_0:3;
x = [a,b]
by TARSKI:def 1, A4;
hence
contradiction
by A1, A2, A4, TARSKI:def 2;
verum
end;
assume A0:
{[a,b]} misses {[a,a],[b,b]}
; a <> b
assume
a = b
; contradiction
then
not [a,a] in {[a,a],[b,b]}
by ZFMISC_1:48, A0;
hence
contradiction
by TARSKI:def 2; verum