:: Non-trivial Universes and Sequences of Universes
:: by Roland Coghetto
::
:: Received April 30, 2022
:: Copyright (c) 2022-2024 Association of Mizar Users


theorem Th1: :: CLASSES4:1
for X being set holds
( proj1 X in bool (union (union X)) & proj2 X in bool (union (union X)) )
proof end;

theorem :: CLASSES4:2
REAL * = { X where X is FinSequence of REAL : verum }
proof end;

registration
cluster empty epsilon-transitive subset-closed Tarski power-closed V25() FamUnion-closed universal for set ;
existence
ex b1 being Grothendieck st b1 is empty
proof end;
end;

registration
cluster non empty epsilon-transitive subset-closed Tarski power-closed V25() FamUnion-closed universal for set ;
existence
not for b1 being Grothendieck holds b1 is empty
proof end;
end;

registration
let X be set ;
cluster -> non empty for Grothendieck of X;
coherence
for b1 being Grothendieck of X holds not b1 is empty by CLASSES3:def 4;
end;

definition
let GU be set ;
attr GU is axiom_GU1 means :: CLASSES4:def 1
 for x, y being set st x in GU & y in x holds
y in GU;
attr GU is axiom_GU2 means :: CLASSES4:def 2
 for x, y being set st x in GU & y in GU holds
{x,y} in GU;
attr GU is axiom_GU3 means :: CLASSES4:def 3
 for x being set st x in GU holds
bool x in GU;
end;

:: deftheorem defines axiom_GU1 CLASSES4:def 1 :
for GU being set holds
( GU is axiom_GU1 iff for x, y being set st x in GU & y in x holds
y in GU );

:: deftheorem defines axiom_GU2 CLASSES4:def 2 :
for GU being set holds
( GU is axiom_GU2 iff for x, y being set st x in GU & y in GU holds
{x,y} in GU );

:: deftheorem defines axiom_GU3 CLASSES4:def 3 :
for GU being set holds
( GU is axiom_GU3 iff for x being set st x in GU holds
bool x in GU );

definition
let GU be non empty set ;
attr GU is axiom_GU4 means :: CLASSES4:def 4
 for I being Element of GU
for x being GU -valued ManySortedSet of I holds union (rng x) in GU;
end;

:: deftheorem defines axiom_GU4 CLASSES4:def 4 :
for GU being non empty set holds
( GU is axiom_GU4 iff for I being Element of GU
for x being b1 -valued ManySortedSet of I holds union (rng x) in GU );

theorem Th3: :: CLASSES4:3
for X being set holds
( X is axiom_GU1 iff X is epsilon-transitive )
proof end;

theorem Th4: :: CLASSES4:4
for X being non empty set holds
( X is axiom_GU4 iff X is FamUnion-closed )
proof end;

theorem :: CLASSES4:5
for X being FamUnion-closed set
for f being Function st dom f in X & rng f c= X holds
union (rng f) in X by CLASSES3:def 3;

registration
cluster epsilon-transitive power-closed FamUnion-closed -> axiom_GU1 axiom_GU2 axiom_GU3 for set ;
coherence
for b1 being Grothendieck holds
( b1 is axiom_GU1 & b1 is axiom_GU2 & b1 is axiom_GU3 ) by Th3, CLASSES2:2, CLASSES3:def 1;
end;

registration
cluster non empty epsilon-transitive power-closed FamUnion-closed -> non empty axiom_GU4 for set ;
coherence
for b1 being non empty Grothendieck holds b1 is axiom_GU4 by Th4;
end;

theorem :: CLASSES4:6
for G being non empty set st G is axiom_GU1 & G is axiom_GU2 & G is axiom_GU3 & G is axiom_GU4 holds
G is non empty Grothendieck by Th3, Th4, CLASSES3:def 1;

theorem :: CLASSES4:7
for X being set holds
( X is Universe iff X is non empty Grothendieck ) ;

theorem Th8: :: CLASSES4:8
for X being set holds Tarski-Class (the_transitive-closure_of {X}) is Grothendieck of X
proof end;

theorem :: CLASSES4:9
for X being set holds the_universe_of {X} is Grothendieck of X
proof end;

theorem :: CLASSES4:10
for X being set holds Universe_closure {X} = GrothendieckUniverse X
proof end;

theorem :: CLASSES4:11
for U being Grothendieck st omega in U holds
( ( for x, u being set st x in u & u in U holds
x in U ) & ( for u, v being set st u in U & v in U holds
( {u,v} in U & [u,v] in U & [:u,v:] in U ) ) & ( for x being set st x in U holds
( bool x in U & union x in U ) ) & omega in U & ( for a, b being set
for f being Function of a,b st dom f = a & f is onto & a in U & b c= U holds
b in U ) )
proof end;

theorem :: CLASSES4:12
for U being set st ( for x, u being set st x in u & u in U holds
x in U ) & ( for x being set st x in U holds
( bool x in U & union x in U ) ) & omega in U & ( for a, b being set
for f being Function of a,b st dom f = a & f is onto & a in U & b c= U holds
b in U ) holds
U is Grothendieck
proof end;

theorem Th13: :: CLASSES4:13
for X being set st X is axiom_GU1 & X is axiom_GU3 holds
( ( for y being set
for x being Subset of y st y in X holds
x in X ) & ( for x, y being set st x c= y & y in X holds
x in X ) & ( not X is empty implies {} in X ) )
proof end;

definition
let UN be Universe;
func {} UN -> Element of UN equals :: CLASSES4:def 5
 {} ;
coherence
{} is Element of UN by Th13;
end;

:: deftheorem defines {} CLASSES4:def 5 :
for UN being Universe holds {} UN = {} ;

theorem :: CLASSES4:14
for UN being Universe holds UN is Grothendieck of {}
proof end;

theorem :: CLASSES4:15
for UN being Universe
for u, v being Element of UN holds Funcs (u,v) c= { f where f is Function of u,v : verum }
proof end;

definition
let UN be Universe;
let u be Element of UN;
:: original: succ
redefine func succ u -> Element of UN;
coherence
succ u is Element of UN
proof end;
end;

theorem Th16: :: CLASSES4:16
for UN being Universe
for n being Nat holds n in UN
proof end;

theorem :: CLASSES4:17
for UN being Universe holds omega c= UN by Th16;

theorem :: CLASSES4:18
for UN being Universe holds
( NAT in UN or NAT ,UN are_equipotent )
proof end;

registration
cluster non empty universal -> infinite for set ;
coherence
for b1 being Universe holds b1 is infinite
proof end;
end;

theorem Th19: :: CLASSES4:19
FinSETS is denumerable by CLASSES2:62, CLASSES2:64, CARD_3:def 15;

registration
cluster non empty non trivial epsilon-transitive V16() subset-closed Tarski power-closed V25() FamUnion-closed infinite V272() universal denumerable axiom_GU1 axiom_GU2 axiom_GU3 axiom_GU4 for set ;
existence
ex b1 being Universe st b1 is denumerable by Th19;
end;

theorem Th20: :: CLASSES4:20
for UN being Universe holds
( not UN is denumerable iff omega in UN )
proof end;

registration
cluster non empty non trivial epsilon-transitive V16() subset-closed Tarski power-closed V25() FamUnion-closed infinite V272() universal non denumerable axiom_GU1 axiom_GU2 axiom_GU3 axiom_GU4 for set ;
existence
not for b1 being Universe holds b1 is denumerable
proof end;
end;

definition
let UN be Universe;
attr UN is trivial means :Def6: :: CLASSES4:def 6
 not omega in UN;
end;

:: deftheorem Def6 defines trivial CLASSES4:def 6 :
for UN being Universe holds
( UN is trivial iff not omega in UN );

theorem Th21: :: CLASSES4:21
( FinSETS is trivial & not SETS is trivial )
proof end;

registration
cluster non empty non trivial epsilon-transitive V16() subset-closed Tarski power-closed V25() FamUnion-closed infinite V272() universal axiom_GU1 axiom_GU2 axiom_GU3 axiom_GU4 trivial for set ;
existence
ex b1 being Universe st b1 is trivial
proof end;
end;

registration
cluster non empty non trivial epsilon-transitive V16() subset-closed Tarski power-closed V25() FamUnion-closed infinite V272() universal axiom_GU1 axiom_GU2 axiom_GU3 axiom_GU4 non trivial for set ;
existence
not for b1 being Universe holds b1 is trivial by Th21;
end;

registration
cluster non empty universal non trivial -> non denumerable non trivial for set ;
coherence
for b1 being non trivial Universe holds not b1 is denumerable by Def6, Th20;
end;

theorem :: CLASSES4:22
for UN being Universe
for x being Element of UN
for y, z being object st x = [y,z] holds
( y is Element of UN & z is Element of UN )
proof end;

registration
let UN be Universe;
cluster pair for Element of UN;
existence
ex b1 being Element of UN st b1 is pair
proof end;
end;

theorem :: CLASSES4:23
for UN being Universe
for u, v being Element of UN holds { f where f is Function of u,v : verum } is Element of UN
proof end;

definition
let UN be Universe;
let I be Element of UN;
let x be UN -valued ManySortedSet of I;
:: original: product
redefine func product x -> Element of UN;
coherence
product x is Element of UN
proof end;
end;

Lm1: for x, y, a, b being set holds (x,y) --> (a,b) c= [:{x,y},{a,b}:]
proof end;

definition
let UN be Universe;
let x, y be Element of UN;
func disjoint-union (x,y) -> Element of UN equals :: CLASSES4:def 7
(x,y) --> (({} UN),{({} UN)});
coherence
(x,y) --> (({} UN),{({} UN)}) is Element of UN
proof end;
end;

:: deftheorem defines disjoint-union CLASSES4:def 7 :
for UN being Universe
for x, y being Element of UN holds disjoint-union (x,y) = (x,y) --> (({} UN),{({} UN)});

theorem :: CLASSES4:24
for UN being Universe
for x, y being Element of UN holds disjoint-union (x,y) is Subset of [:{x,y},{{},{{}}}:] by Lm1;

theorem :: CLASSES4:25
for UN being Universe
for u being Element of UN holds disjoint-union (u,u) = {[u,{{}}]}
proof end;

definition
let UN be Universe;
let I be Element of UN;
let x be UN -valued ManySortedSet of I;
:: original: dom
redefine func dom x -> Element of UN;
coherence
dom x is Element of UN by PARTFUN1:def 2;
end;

definition
let UN be Universe;
let I be Element of UN;
let x be UN -valued ManySortedSet of I;
:: original: Union
redefine func Union x -> Element of UN;
coherence
Union x is Element of UN
proof end;
end;

definition
let UN be Universe;
let I be Element of UN;
let x be UN -valued ManySortedSet of I;
:: original: disjoin
redefine func disjoin x -> UN -valued ManySortedSet of I;
coherence
disjoin x is UN -valued ManySortedSet of I
proof end;
end;

definition
let UN be Universe;
let I be Element of UN;
let x be UN -valued ManySortedSet of I;
func disjoint-union x -> Element of UN equals :: CLASSES4:def 8
 Union (disjoin x);
coherence
Union (disjoin x) is Element of UN ;
end;

:: deftheorem defines disjoint-union CLASSES4:def 8 :
for UN being Universe
for I being Element of UN
for x being b1 -valued ManySortedSet of I holds disjoint-union x = Union (disjoin x);

theorem :: CLASSES4:26
for UN being Universe
for I being Element of UN
for x being b1 -valued ManySortedSet of I holds Union (coprod ) is Element of UN
proof end;

theorem :: CLASSES4:27
for UN being Universe
for I being Element of UN
for x being b1 -valued ManySortedSet of I holds disjoint-union x is Subset of [:(union (rng x)),I:]
proof end;

theorem :: CLASSES4:28
for X being set st X is axiom_GU2 holds
for x being set st x in X holds
{x} in X
proof end;

theorem :: CLASSES4:29
for UN being Universe
for u being Element of UN holds card u in UN by CLASSES2:11;

theorem :: CLASSES4:30
for UN being Universe
for u being Element of UN holds
( not u,UN are_equipotent & card u in card UN ) by CLASSES2:1;

theorem Th31: :: CLASSES4:31
for UN being Universe
for u, v being Element of UN holds {[u,{}],[v,{{}}]} = [:{u},{{}}:] \/ [:{v},{{{}}}:]
proof end;

theorem Th32: :: CLASSES4:32
for UN being Universe
for I, a, b, u, v being Element of UN
for x being b1 -valued ManySortedSet of I st I = {a,b} & x . a = u & x . b = v holds
disjoint-union x = [:u,{a}:] \/ [:v,{b}:]
proof end;

theorem Th33: :: CLASSES4:33
for UN being Universe
for I, u, v being Element of UN
for x being b1 -valued ManySortedSet of I st I = {{},{{}}} & x . {} = u & x . {{}} = v holds
disjoint-union x = [:u,{{}}:] \/ [:v,{{{}}}:]
proof end;

theorem :: CLASSES4:34
for UN being Universe
for I, u, v being Element of UN
for x being b1 -valued ManySortedSet of I st I = {{},{{}}} & x . {} = {u} & x . {{}} = {v} & u <> v holds
disjoint-union x = disjoint-union (u,v)
proof end;

theorem Th35: :: CLASSES4:35
for UN being Universe
for x being Element of UN
for y, z being object st x = [y,z] holds
( y is Element of UN & z is Element of UN )
proof end;

registration
let UN be Universe;
cluster pair for Element of UN;
existence
ex b1 being Element of UN st b1 is pair
proof end;
end;

definition
let UN be Universe;
let u be pair Element of UN;
:: original: `1
redefine func u `1 -> Element of UN;
coherence
u `1 is Element of UN
proof end;
:: original: `2
redefine func u `2 -> Element of UN;
coherence
u `2 is Element of UN
proof end;
end;

theorem Th36: :: CLASSES4:36
for UN being Universe
for X being Element of UN holds
( proj1 X is Element of UN & proj2 X is Element of UN )
proof end;

theorem Th37: :: CLASSES4:37
for UN being Universe
for R being Relation st R in UN holds
( dom R in UN & rng R in UN )
proof end;

theorem :: CLASSES4:38
for UN being Universe
for R being Relation st dom R is Element of UN & rng R is Element of UN holds
R is Element of UN
proof end;

theorem :: CLASSES4:39
for UN being Universe
for X being set
for Y being non empty set
for f being Function of X,Y st f in UN holds
X in UN
proof end;

theorem :: CLASSES4:40
for UN being Universe
for A, B being non empty set st [:A,B:] is Element of UN holds
( A is Element of UN & B is Element of UN )
proof end;

theorem :: CLASSES4:41
for UN being Universe
for X being set st id X is Element of UN holds
X is Element of UN
proof end;

theorem :: CLASSES4:42
for UN being Universe
for x, y, z being Element of UN holds (x,y) .--> z is Element of UN
proof end;

theorem Th43: :: CLASSES4:43
omega c< FinSETS
proof end;

theorem Th44: :: CLASSES4:44
for X being set holds Tarski-Class {} c= Tarski-Class X
proof end;

theorem Th45: :: CLASSES4:45
for X being set
for G being Grothendieck of X holds FinSETS c= G
proof end;

theorem Th46: :: CLASSES4:46
( GrothendieckUniverse {} = FinSETS & GrothendieckUniverse {} = UNIVERSE {} ) by Th45, CLASSES2:65, CLASSES2:56, CLASSES3:21;

theorem :: CLASSES4:47
for X being set
for G being Grothendieck of X holds
( GrothendieckUniverse {} c= GrothendieckUniverse X & GrothendieckUniverse X c= G ) by CLASSES2:56, CLASSES3:21, CLASSES3:def 5;

theorem :: CLASSES4:48
for n being Element of FinSETS holds GrothendieckUniverse n = FinSETS
proof end;

theorem :: CLASSES4:49
( the empty Grothendieck c< omega & omega c< GrothendieckUniverse {} & GrothendieckUniverse {} c< GrothendieckUniverse omega )
proof end;

theorem :: CLASSES4:50
for G being non empty Grothendieck holds
( not G <> GrothendieckUniverse omega or GrothendieckUniverse omega in G or G in GrothendieckUniverse omega ) by CLASSES2:52;

theorem :: CLASSES4:51
Tarski-Class omega = GrothendieckUniverse omega by CLASSES3:22;

theorem Th52: :: CLASSES4:52
for N1, N2 being set st N1 = [:NAT,NAT:] \/ NAT & N2 = N1 \/ (bool N1) holds
REAL c= N2 \/ [:NAT,N2:]
proof end;

theorem Th53: :: CLASSES4:53
for UN being non trivial Universe holds REAL is Element of UN
proof end;

theorem Th54: :: CLASSES4:54
for UN being non trivial Universe holds ExtREAL is Element of UN
proof end;

theorem Th55: :: CLASSES4:55
for UN being non trivial Universe holds COMPLEX in UN
proof end;

theorem Th56: :: CLASSES4:56
for UN being non trivial Universe holds QUATERNION in UN
proof end;

theorem Th57: :: CLASSES4:57
for UN being Universe
for n being Nat holds Seg n in UN
proof end;

theorem Th58: :: CLASSES4:58
for UN being Universe
for D being set st D in UN holds
for n being Nat holds n -tuples_on D in UN
proof end;

theorem :: CLASSES4:59
for UN being non trivial Universe
for n being Nat holds REAL n in UN
proof end;

theorem :: CLASSES4:60
for UN being Universe
for X being set st X in UN holds
for n being Nat holds n -tuples_on X in UN
proof end;

theorem :: CLASSES4:61
for X being set
for n being Nat holds n -tuples_on X c= X * by FINSEQ_2:90;

theorem Th62: :: CLASSES4:62
for X being non empty set
for x being object st x in X * holds
ex n being Nat st x in n -tuples_on X
proof end;

theorem Th63: :: CLASSES4:63
for X being non empty set ex f being Function st
( dom f = NAT & ( for n being Nat holds f . n = n -tuples_on X ) & union (rng f) = X * )
proof end;

theorem Th64: :: CLASSES4:64
for UN being non trivial Universe
for X being non empty set st X in UN holds
X * in UN
proof end;

theorem :: CLASSES4:65
for UN being non trivial Universe holds REAL * in UN
proof end;

theorem :: CLASSES4:66
for UN being non trivial Universe holds ExtREAL * in UN
proof end;

theorem :: CLASSES4:67
for UN being non trivial Universe holds COMPLEX * in UN by Th64, Th55;

theorem :: CLASSES4:68
for UN being non trivial Universe holds QUATERNION * in UN by Th64, Th56;

theorem Th69: :: CLASSES4:69
for UN being Universe
for X being set st X in UN holds
for s being FinSequence of X holds s in UN
proof end;

theorem :: CLASSES4:70
for X being empty set
for f being FinSequence of X * holds f = (len f) |-> 0 by FUNCT_7:17, MSSUBLAT:5;

theorem :: CLASSES4:71
for UN being non trivial Universe
for D being non empty set st D in UN holds
for M being Matrix of D holds M in UN by Th64, Th69;

theorem Th72: :: CLASSES4:72
( FinSETS in SETS & NAT in SETS & REAL in SETS & ExtREAL in SETS )
proof end;

theorem Th73: :: CLASSES4:73
for X being set
for U1 being Universe st U1 in Tarski-Class X holds
Tarski-Class U1 c= Tarski-Class X
proof end;

theorem Th74: :: CLASSES4:74
FinSETS in Tarski-Class omega
proof end;

theorem Th75: :: CLASSES4:75
SETS = Tarski-Class omega
proof end;

theorem :: CLASSES4:76
GrothendieckUniverse omega = SETS by CLASSES3:22, Th75;

theorem Th77: :: CLASSES4:77
( GrothendieckUniverse omega = GrothendieckUniverse FinSETS & GrothendieckUniverse FinSETS = SETS )
proof end;

theorem Th78: :: CLASSES4:78
for X being non empty set
for GX being Grothendieck of X
for G being Universe st X misses G holds
GX <> G
proof end;

theorem :: CLASSES4:79
for X being non empty set
for GX being Grothendieck of X
for G being Universe holds
( not X misses G or GX in G or G in GX ) by Th78, CLASSES2:52;

theorem :: CLASSES4:80
for UN1, UN2 being Universe
for a being Element of UN1 st not a in UN2 holds
UN2 in UN1
proof end;

theorem Th81: :: CLASSES4:81
for G being Grothendieck holds union G = G
proof end;

registration
cluster epsilon-transitive power-closed FamUnion-closed -> limit_ordinal for set ;
coherence
for b1 being Grothendieck holds b1 is limit_ordinal by Th81;
end;

theorem :: CLASSES4:82
for UN being Universe
for V being non empty Element of UN holds Funcs V is Subset of UN
proof end;

theorem :: CLASSES4:83
for UN being Universe holds
not for a being set holds a in UN
proof end;

theorem :: CLASSES4:84
for UN being Universe holds
not for A being Subset of UN holds A in UN
proof end;

theorem :: CLASSES4:85
for UN being Universe holds { u where u is Element of UN : verum } is not Element of UN
proof end;

theorem Th86: :: CLASSES4:86
for UN being Universe
for X being Element of UN holds UN \ X is not Element of UN
proof end;

theorem :: CLASSES4:87
for UN being Universe holds not bool UN in UN by ZFMISC_1:def 1;

theorem Th88: :: CLASSES4:88
for X being set ex f being Function st
( dom f = NAT & f . 0 = X & ( for n being Nat holds f . (n + 1) = GrothendieckUniverse (f . n) ) )
proof end;

definition
let X be set ;
func sequence_univers X -> Function means :Def9: :: CLASSES4:def 9
( dom it = NAT & it . 0 = X & ( for n being Nat holds it . (n + 1) = GrothendieckUniverse (it . n) ) );
existence
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = X & ( for n being Nat holds b1 . (n + 1) = GrothendieckUniverse (b1 . n) ) ) by Th88;
uniqueness
for b1, b2 being Function st dom b1 = NAT & b1 . 0 = X & ( for n being Nat holds b1 . (n + 1) = GrothendieckUniverse (b1 . n) ) & dom b2 = NAT & b2 . 0 = X & ( for n being Nat holds b2 . (n + 1) = GrothendieckUniverse (b2 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines sequence_univers CLASSES4:def 9 :
for X being set
for b2 being Function holds
( b2 = sequence_univers X iff ( dom b2 = NAT & b2 . 0 = X & ( for n being Nat holds b2 . (n + 1) = GrothendieckUniverse (b2 . n) ) ) );

theorem :: CLASSES4:89
for X being set holds sequence_univers X is Sequence
proof end;

theorem Th90: :: CLASSES4:90
for X being set
for S being Sequence st dom S = NAT holds
last S = S . NAT
proof end;

theorem Th91: :: CLASSES4:91
for S being Sequence st dom S = NAT holds
( S . NAT = {} & last S = {} )
proof end;

theorem :: CLASSES4:92
for X being set
for S being Sequence st S = sequence_univers X holds
( last S = {} & S . NAT = {} )
proof end;

definition
let X be set ;
func union_sequence_univers X -> non empty set equals :: CLASSES4:def 10
 union (rng (sequence_univers X));
coherence
union (rng (sequence_univers X)) is non empty set
proof end;
end;

:: deftheorem defines union_sequence_univers CLASSES4:def 10 :
for X being set holds union_sequence_univers X = union (rng (sequence_univers X));

theorem Th93: :: CLASSES4:93
for X being set holds rng (sequence_univers X) c= union_sequence_univers X
proof end;

definition
func sequence_univers -> sequence of (union_sequence_univers {}) equals :: CLASSES4:def 11
 sequence_univers {};
coherence
sequence_univers {} is sequence of (union_sequence_univers {})
proof end;
end;

:: deftheorem defines sequence_univers CLASSES4:def 11 :
sequence_univers = sequence_univers {};

theorem Th94: :: CLASSES4:94
( {} in rng sequence_univers & FinSETS in rng sequence_univers & SETS in rng sequence_univers )
proof end;

theorem :: CLASSES4:95
union (rng sequence_univers) is not Grothendieck
proof end;

theorem :: CLASSES4:96
( Tarski-Class FinSETS = GrothendieckUniverse FinSETS & Tarski-Class SETS = GrothendieckUniverse SETS ) by CLASSES3:22;

theorem :: CLASSES4:97
for X being set
for n being Nat holds
( (sequence_univers X) . (n + 1) is epsilon-transitive & Tarski-Class ((sequence_univers X) . (n + 1)) = GrothendieckUniverse ((sequence_univers X) . (n + 1)) )
proof end;

theorem Th98: :: CLASSES4:98
for n being Nat holds Tarski-Class ((sequence_univers FinSETS) . n) = GrothendieckUniverse ((sequence_univers FinSETS) . n)
proof end;

theorem Th99: :: CLASSES4:99
for n being Nat holds UNIVERSE n in UNIVERSE (n + 1)
proof end;

theorem Th100: :: CLASSES4:100
for n being Nat holds (sequence_univers FinSETS) . n = UNIVERSE n
proof end;

theorem Th101: :: CLASSES4:101
for n being Nat holds GrothendieckUniverse ((sequence_univers {}) . n) = (sequence_univers (GrothendieckUniverse {})) . n
proof end;

theorem Th102: :: CLASSES4:102
for n being Nat holds sequence_univers . (n + 1) = UNIVERSE n
proof end;

registration
cluster non empty for Element of union (rng sequence_univers);
existence
not for b1 being Element of union (rng sequence_univers) holds b1 is empty by Th94;
end;

theorem Th103: :: CLASSES4:103
( FinSETS in GrothendieckUniverse sequence_univers & SETS in GrothendieckUniverse sequence_univers )
proof end;

theorem Th104: :: CLASSES4:104
for n being Nat holds sequence_univers . (n + 1) in GrothendieckUniverse sequence_univers
proof end;

definition
func super_univers -> non trivial Universe equals :: CLASSES4:def 12
 GrothendieckUniverse sequence_univers;
coherence
GrothendieckUniverse sequence_univers is non trivial Universe
proof end;
end;

:: deftheorem defines super_univers CLASSES4:def 12 :
super_univers = GrothendieckUniverse sequence_univers;

theorem Th105: :: CLASSES4:105
for n being Nat holds sequence_univers . n c= sequence_univers . (n + 1)
proof end;

definition
let X be Element of union (rng sequence_univers);
func rank_univers X -> Nat means :Def13: :: CLASSES4:def 13
( X in sequence_univers . it & ( for n being Nat st n < it holds
not X in sequence_univers . n ) );
existence
ex b1 being Nat st
( X in sequence_univers . b1 & ( for n being Nat st n < b1 holds
not X in sequence_univers . n ) )
proof end;
uniqueness
for b1, b2 being Nat st X in sequence_univers . b1 & ( for n being Nat st n < b1 holds
not X in sequence_univers . n ) & X in sequence_univers . b2 & ( for n being Nat st n < b2 holds
not X in sequence_univers . n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines rank_univers CLASSES4:def 13 :
for X being Element of union (rng sequence_univers)
for b2 being Nat holds
( b2 = rank_univers X iff ( X in sequence_univers . b2 & ( for n being Nat st n < b2 holds
not X in sequence_univers . n ) ) );

theorem :: CLASSES4:106
for X being Element of union (rng sequence_univers)
for n being Nat st rank_univers X <= n holds
X in sequence_univers . n
proof end;

theorem :: CLASSES4:107
for i being Nat ex x being set st x in (sequence_univers . (i + 1)) \ (sequence_univers . i)
proof end;

theorem :: CLASSES4:108
for n being Nat holds not (UNIVERSE (n + 1)) \ (UNIVERSE n) in UNIVERSE (n + 1)
proof end;

definition
func ComplUniverse -> Function of NAT,(union (rng sequence_univers)) means :Def14: :: CLASSES4:def 14
 for n being Nat holds it . n = (UNIVERSE (n + 1)) \ (UNIVERSE n);
existence
ex b1 being Function of NAT,(union (rng sequence_univers)) st
for n being Nat holds b1 . n = (UNIVERSE (n + 1)) \ (UNIVERSE n)
proof end;
uniqueness
for b1, b2 being Function of NAT,(union (rng sequence_univers)) st ( for n being Nat holds b1 . n = (UNIVERSE (n + 1)) \ (UNIVERSE n) ) & ( for n being Nat holds b2 . n = (UNIVERSE (n + 1)) \ (UNIVERSE n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines ComplUniverse CLASSES4:def 14 :
for b1 being Function of NAT,(union (rng sequence_univers)) holds
( b1 = ComplUniverse iff for n being Nat holds b1 . n = (UNIVERSE (n + 1)) \ (UNIVERSE n) );

theorem Th109: :: CLASSES4:109
for n being Nat holds not ComplUniverse . n is empty
proof end;

theorem :: CLASSES4:110
for n being Nat holds ComplUniverse . n c= UNIVERSE (n + 1)
proof end;

theorem :: CLASSES4:111
ex f being Function of NAT,(union (union (rng sequence_univers))) st
for i being Nat holds f . i in ComplUniverse . i
proof end;

theorem :: CLASSES4:112
for f being Function of NAT,(union (rng sequence_univers)) holds f in super_univers
proof end;

theorem :: CLASSES4:113
for f being Function of NAT,(union (union (rng sequence_univers))) holds f in super_univers
proof end;