defpred S1[ Nat] means Mycielskian n is irreflexive ;
P0:
S1[ 0 ]
by Mycn1;
P1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
set cMRn = the
carrier of
(Mycielskian n);
set iMRn = the
InternalRel of
(Mycielskian n);
set cMRn1 = the
carrier of
(Mycielskian (n + 1));
set iMRn1 = the
InternalRel of
(Mycielskian (n + 1));
assume A1:
S1[
n]
;
S1[n + 1]
assume
not
S1[
n + 1]
;
contradiction
then consider x being
set such that C1:
x in the
carrier of
(Mycielskian (n + 1))
and D1:
[x,x] in the
InternalRel of
(Mycielskian (n + 1))
by NECKLACE:def 6;
E1:
Mycielskian (n + 1) = Mycielskian (Mycielskian n)
by Mycn1;
set N =
(3 * (2 |^ n)) -' 1;
F1:
the
carrier of
(Mycielskian (n + 1)) = (2 * ((3 * (2 |^ n)) -' 1)) + 1
by E1, LNRS;
G1:
the
carrier of
(Mycielskian n) = (3 * (2 |^ n)) -' 1
by LNRS;
reconsider x =
x as
Nat by F1, C1, NECKLACE:4;
( (
x < (3 * (2 |^ n)) -' 1 &
x < (3 * (2 |^ n)) -' 1 ) or (
x < (3 * (2 |^ n)) -' 1 &
(3 * (2 |^ n)) -' 1
<= x &
x < 2
* ((3 * (2 |^ n)) -' 1) ) or (
(3 * (2 |^ n)) -' 1
<= x &
x < 2
* ((3 * (2 |^ n)) -' 1) &
x < (3 * (2 |^ n)) -' 1 ) or (
x = 2
* ((3 * (2 |^ n)) -' 1) &
(3 * (2 |^ n)) -' 1
<= x &
x < 2
* ((3 * (2 |^ n)) -' 1) ) or (
(3 * (2 |^ n)) -' 1
<= x &
x < 2
* ((3 * (2 |^ n)) -' 1) &
x = 2
* ((3 * (2 |^ n)) -' 1) ) )
by E1, D1, iMR0;
then H1:
x in (3 * (2 |^ n)) -' 1
by NAT_1:45;
then
[x,x] in the
InternalRel of
(Mycielskian n)
by D1, E1, iMR1b;
hence
contradiction
by A1, G1, H1, NECKLACE:def 6;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(P0, P1);
hence
Mycielskian n is irreflexive
; verum