:: ENUMSET1 semantic presentation

Lemma1: for b₁, b₂, b₃ being set holds
( b₁ in union {b₂,{b₃}} iff ( b₁ in b₂ or b₁ = b₃ ) )

proof end;

definition

let c₁, c₂, c₃ be set ;
func {c₁,c₂,c₃} -> set means :Def1: :: ENUMSET1:def 1
for b₁ being set holds
( b₁ in a₄ iff ( b₁ = a₁ or b₁ = a₂ or b₁ = a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines { ENUMSET1:def 1 :

definition

let c₁, c₂, c₃, c₄ be set ;
func {c₁,c₂,c₃,c₄} -> set means :Def2: :: ENUMSET1:def 2
for b₁ being set holds
( b₁ in a₅ iff ( b₁ = a₁ or b₁ = a₂ or b₁ = a₃ or b₁ = a₄ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines { ENUMSET1:def 2 :

definition

let c₁, c₂, c₃, c₄, c₅ be set ;
func {c₁,c₂,c₃,c₄,c₅} -> set means :Def3: :: ENUMSET1:def 3
for b₁ being set holds
( b₁ in a₆ iff ( b₁ = a₁ or b₁ = a₂ or b₁ = a₃ or b₁ = a₄ or b₁ = a₅ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines { ENUMSET1:def 3 :

definition

let c₁, c₂, c₃, c₄, c₅, c₆ be set ;
func {c₁,c₂,c₃,c₄,c₅,c₆} -> set means :Def4: :: ENUMSET1:def 4
for b₁ being set holds
( b₁ in a₇ iff ( b₁ = a₁ or b₁ = a₂ or b₁ = a₃ or b₁ = a₄ or b₁ = a₅ or b₁ = a₆ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines { ENUMSET1:def 4 :

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇ be set ;
func {c₁,c₂,c₃,c₄,c₅,c₆,c₇} -> set means :Def5: :: ENUMSET1:def 5
for b₁ being set holds
( b₁ in a₈ iff ( b₁ = a₁ or b₁ = a₂ or b₁ = a₃ or b₁ = a₄ or b₁ = a₅ or b₁ = a₆ or b₁ = a₇ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines { ENUMSET1:def 5 :

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇, c₈ be set ;
func {c₁,c₂,c₃,c₄,c₅,c₆,c₇,c₈} -> set means :Def6: :: ENUMSET1:def 6
for b₁ being set holds
( b₁ in a₉ iff ( b₁ = a₁ or b₁ = a₂ or b₁ = a₃ or b₁ = a₄ or b₁ = a₅ or b₁ = a₆ or b₁ = a₇ or b₁ = a₈ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines { ENUMSET1:def 6 :

theorem Th1: :: ENUMSET1:1

canceled;

theorem Th2: :: ENUMSET1:2

canceled;

theorem Th3: :: ENUMSET1:3

canceled;

theorem Th4: :: ENUMSET1:4

canceled;

theorem Th5: :: ENUMSET1:5

canceled;

theorem Th6: :: ENUMSET1:6

canceled;

theorem Th7: :: ENUMSET1:7

canceled;

theorem Th8: :: ENUMSET1:8

canceled;

theorem Th9: :: ENUMSET1:9

canceled;

theorem Th10: :: ENUMSET1:10

canceled;

theorem Th11: :: ENUMSET1:11

canceled;

theorem Th12: :: ENUMSET1:12

canceled;

theorem Th13: :: ENUMSET1:13

canceled;

theorem Th14: :: ENUMSET1:14

canceled;

theorem Th15: :: ENUMSET1:15

canceled;

theorem Th16: :: ENUMSET1:16

canceled;

theorem Th17: :: ENUMSET1:17

canceled;

theorem Th18: :: ENUMSET1:18

canceled;

theorem Th19: :: ENUMSET1:19

canceled;

theorem Th20: :: ENUMSET1:20

canceled;

theorem Th21: :: ENUMSET1:21

canceled;

theorem Th22: :: ENUMSET1:22

canceled;

theorem Th23: :: ENUMSET1:23

canceled;

theorem Th24: :: ENUMSET1:24

canceled;

theorem Th25: :: ENUMSET1:25

canceled;

theorem Th26: :: ENUMSET1:26

canceled;

theorem Th27: :: ENUMSET1:27

canceled;

theorem Th28: :: ENUMSET1:28

canceled;

theorem Th29: :: ENUMSET1:29

canceled;

theorem Th30: :: ENUMSET1:30

canceled;

theorem Th31: :: ENUMSET1:31

canceled;

theorem Th32: :: ENUMSET1:32

canceled;

theorem Th33: :: ENUMSET1:33

canceled;

theorem Th34: :: ENUMSET1:34

canceled;

theorem Th35: :: ENUMSET1:35

canceled;

theorem Th36: :: ENUMSET1:36

canceled;

theorem Th37: :: ENUMSET1:37

canceled;

theorem Th38: :: ENUMSET1:38

canceled;

theorem Th39: :: ENUMSET1:39

canceled;

theorem Th40: :: ENUMSET1:40

canceled;

theorem Th41: :: ENUMSET1:41

for b₁, b₂ being set holds {b₁,b₂} = {b₁} \/ {b₂}

proof end;

theorem Th42: :: ENUMSET1:42

for b₁, b₂, b₃ being set holds {b₁,b₂,b₃} = {b₁} \/ {b₂,b₃}

proof end;

theorem Th43: :: ENUMSET1:43

for b₁, b₂, b₃ being set holds {b₁,b₂,b₃} = {b₁,b₂} \/ {b₃}

proof end;

Lemma11: for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₁,b₂} \/ {b₃,b₄}

proof end;

theorem Th44: :: ENUMSET1:44

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₁} \/ {b₂,b₃,b₄}

proof end;

theorem Th45: :: ENUMSET1:45

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₁,b₂} \/ {b₃,b₄} by Lemma11;

theorem Th46: :: ENUMSET1:46

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₁,b₂,b₃} \/ {b₄}

proof end;

Lemma14: for b₁, b₂, b₃, b₄, b₅ being set holds {b₁,b₂,b₃,b₄,b₅} = {b₁,b₂,b₃} \/ {b₄,b₅}

proof end;

theorem Th47: :: ENUMSET1:47

for b₁, b₂, b₃, b₄, b₅ being set holds {b₁,b₂,b₃,b₄,b₅} = {b₁} \/ {b₂,b₃,b₄,b₅}

proof end;

theorem Th48: :: ENUMSET1:48

for b₁, b₂, b₃, b₄, b₅ being set holds {b₁,b₂,b₃,b₄,b₅} = {b₁,b₂} \/ {b₃,b₄,b₅}

proof end;

theorem Th49: :: ENUMSET1:49

for b₁, b₂, b₃, b₄, b₅ being set holds {b₁,b₂,b₃,b₄,b₅} = {b₁,b₂,b₃} \/ {b₄,b₅} by Lemma14;

theorem Th50: :: ENUMSET1:50

for b₁, b₂, b₃, b₄, b₅ being set holds {b₁,b₂,b₃,b₄,b₅} = {b₁,b₂,b₃,b₄} \/ {b₅}

proof end;

Lemma18: for b₁, b₂, b₃, b₄, b₅, b₆ being set holds {b₁,b₂,b₃,b₄,b₅,b₆} = {b₁,b₂,b₃} \/ {b₄,b₅,b₆}

proof end;

theorem Th51: :: ENUMSET1:51

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds {b₁,b₂,b₃,b₄,b₅,b₆} = {b₁} \/ {b₂,b₃,b₄,b₅,b₆}

proof end;

theorem Th52: :: ENUMSET1:52

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds {b₁,b₂,b₃,b₄,b₅,b₆} = {b₁,b₂} \/ {b₃,b₄,b₅,b₆}

proof end;

theorem Th53: :: ENUMSET1:53

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds {b₁,b₂,b₃,b₄,b₅,b₆} = {b₁,b₂,b₃} \/ {b₄,b₅,b₆} by Lemma18;

theorem Th54: :: ENUMSET1:54

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds {b₁,b₂,b₃,b₄,b₅,b₆} = {b₁,b₂,b₃,b₄} \/ {b₅,b₆}

proof end;

theorem Th55: :: ENUMSET1:55

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds {b₁,b₂,b₃,b₄,b₅,b₆} = {b₁,b₂,b₃,b₄,b₅} \/ {b₆}

proof end;

Lemma22: for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇} = {b₁,b₂,b₃,b₄} \/ {b₅,b₆,b₇}

proof end;

theorem Th56: :: ENUMSET1:56

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇} = {b₁} \/ {b₂,b₃,b₄,b₅,b₆,b₇}

proof end;

theorem Th57: :: ENUMSET1:57

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇} = {b₁,b₂} \/ {b₃,b₄,b₅,b₆,b₇}

proof end;

theorem Th58: :: ENUMSET1:58

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇} = {b₁,b₂,b₃} \/ {b₄,b₅,b₆,b₇}

proof end;

theorem Th59: :: ENUMSET1:59

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇} = {b₁,b₂,b₃,b₄} \/ {b₅,b₆,b₇} by Lemma22;

theorem Th60: :: ENUMSET1:60

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇} = {b₁,b₂,b₃,b₄,b₅} \/ {b₆,b₇}

proof end;

theorem Th61: :: ENUMSET1:61

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇} = {b₁,b₂,b₃,b₄,b₅,b₆} \/ {b₇}

proof end;

Lemma26: for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇,b₈} = {b₁,b₂,b₃,b₄} \/ {b₅,b₆,b₇,b₈}

proof end;

theorem Th62: :: ENUMSET1:62

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇,b₈} = {b₁} \/ {b₂,b₃,b₄,b₅,b₆,b₇,b₈}

proof end;

theorem Th63: :: ENUMSET1:63

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇,b₈} = {b₁,b₂} \/ {b₃,b₄,b₅,b₆,b₇,b₈}

proof end;

theorem Th64: :: ENUMSET1:64

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇,b₈} = {b₁,b₂,b₃} \/ {b₄,b₅,b₆,b₇,b₈}

proof end;

theorem Th65: :: ENUMSET1:65

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇,b₈} = {b₁,b₂,b₃,b₄} \/ {b₅,b₆,b₇,b₈} by Lemma26;

theorem Th66: :: ENUMSET1:66

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇,b₈} = {b₁,b₂,b₃,b₄,b₅} \/ {b₆,b₇,b₈}

proof end;

theorem Th67: :: ENUMSET1:67

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇,b₈} = {b₁,b₂,b₃,b₄,b₅,b₆} \/ {b₇,b₈}

proof end;

theorem Th68: :: ENUMSET1:68

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set holds {b₁,b₂,b₃,b₄,b₅,b₆,b₇,b₈} = {b₁,b₂,b₃,b₄,b₅,b₆,b₇} \/ {b₈}

proof end;

theorem Th69: :: ENUMSET1:69

for b₁ being set holds {b₁,b₁} = {b₁}

proof end;

theorem Th70: :: ENUMSET1:70

for b₁, b₂ being set holds {b₁,b₁,b₂} = {b₁,b₂}

proof end;

theorem Th71: :: ENUMSET1:71

for b₁, b₂, b₃ being set holds {b₁,b₁,b₂,b₃} = {b₁,b₂,b₃}

proof end;

theorem Th72: :: ENUMSET1:72

for b₁, b₂, b₃, b₄ being set holds {b₁,b₁,b₂,b₃,b₄} = {b₁,b₂,b₃,b₄}

proof end;

theorem Th73: :: ENUMSET1:73

for b₁, b₂, b₃, b₄, b₅ being set holds {b₁,b₁,b₂,b₃,b₄,b₅} = {b₁,b₂,b₃,b₄,b₅}

proof end;

theorem Th74: :: ENUMSET1:74

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds {b₁,b₁,b₂,b₃,b₄,b₅,b₆} = {b₁,b₂,b₃,b₄,b₅,b₆}

proof end;

theorem Th75: :: ENUMSET1:75

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set holds {b₁,b₁,b₂,b₃,b₄,b₅,b₆,b₇} = {b₁,b₂,b₃,b₄,b₅,b₆,b₇}

proof end;

theorem Th76: :: ENUMSET1:76

for b₁ being set holds {b₁,b₁,b₁} = {b₁}

proof end;

theorem Th77: :: ENUMSET1:77

for b₁, b₂ being set holds {b₁,b₁,b₁,b₂} = {b₁,b₂}

proof end;

theorem Th78: :: ENUMSET1:78

for b₁, b₂, b₃ being set holds {b₁,b₁,b₁,b₂,b₃} = {b₁,b₂,b₃}

proof end;

theorem Th79: :: ENUMSET1:79

for b₁, b₂, b₃, b₄ being set holds {b₁,b₁,b₁,b₂,b₃,b₄} = {b₁,b₂,b₃,b₄}

proof end;

theorem Th80: :: ENUMSET1:80

for b₁, b₂, b₃, b₄, b₅ being set holds {b₁,b₁,b₁,b₂,b₃,b₄,b₅} = {b₁,b₂,b₃,b₄,b₅}

proof end;

theorem Th81: :: ENUMSET1:81

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds {b₁,b₁,b₁,b₂,b₃,b₄,b₅,b₆} = {b₁,b₂,b₃,b₄,b₅,b₆}

proof end;

theorem Th82: :: ENUMSET1:82

for b₁ being set holds {b₁,b₁,b₁,b₁} = {b₁}

proof end;

theorem Th83: :: ENUMSET1:83

for b₁, b₂ being set holds {b₁,b₁,b₁,b₁,b₂} = {b₁,b₂}

proof end;

theorem Th84: :: ENUMSET1:84

for b₁, b₂, b₃ being set holds {b₁,b₁,b₁,b₁,b₂,b₃} = {b₁,b₂,b₃}

proof end;

theorem Th85: :: ENUMSET1:85

for b₁, b₂, b₃, b₄ being set holds {b₁,b₁,b₁,b₁,b₂,b₃,b₄} = {b₁,b₂,b₃,b₄}

proof end;

theorem Th86: :: ENUMSET1:86

for b₁, b₂, b₃, b₄, b₅ being set holds {b₁,b₁,b₁,b₁,b₂,b₃,b₄,b₅} = {b₁,b₂,b₃,b₄,b₅}

proof end;

theorem Th87: :: ENUMSET1:87

for b₁ being set holds {b₁,b₁,b₁,b₁,b₁} = {b₁}

proof end;

theorem Th88: :: ENUMSET1:88

for b₁, b₂ being set holds {b₁,b₁,b₁,b₁,b₁,b₂} = {b₁,b₂}

proof end;

theorem Th89: :: ENUMSET1:89

for b₁, b₂, b₃ being set holds {b₁,b₁,b₁,b₁,b₁,b₂,b₃} = {b₁,b₂,b₃}

proof end;

theorem Th90: :: ENUMSET1:90

for b₁, b₂, b₃, b₄ being set holds {b₁,b₁,b₁,b₁,b₁,b₂,b₃,b₄} = {b₁,b₂,b₃,b₄}

proof end;

theorem Th91: :: ENUMSET1:91

for b₁ being set holds {b₁,b₁,b₁,b₁,b₁,b₁} = {b₁}

proof end;

theorem Th92: :: ENUMSET1:92

for b₁, b₂ being set holds {b₁,b₁,b₁,b₁,b₁,b₁,b₂} = {b₁,b₂}

proof end;

theorem Th93: :: ENUMSET1:93

for b₁, b₂, b₃ being set holds {b₁,b₁,b₁,b₁,b₁,b₁,b₂,b₃} = {b₁,b₂,b₃}

proof end;

theorem Th94: :: ENUMSET1:94

for b₁ being set holds {b₁,b₁,b₁,b₁,b₁,b₁,b₁} = {b₁}

proof end;

theorem Th95: :: ENUMSET1:95

for b₁, b₂ being set holds {b₁,b₁,b₁,b₁,b₁,b₁,b₁,b₂} = {b₁,b₂}

proof end;

theorem Th96: :: ENUMSET1:96

for b₁ being set holds {b₁,b₁,b₁,b₁,b₁,b₁,b₁,b₁} = {b₁}

proof end;

theorem Th97: :: ENUMSET1:97

canceled;

theorem Th98: :: ENUMSET1:98

for b₁, b₂, b₃ being set holds {b₁,b₂,b₃} = {b₁,b₃,b₂}

proof end;

theorem Th99: :: ENUMSET1:99

for b₁, b₂, b₃ being set holds {b₁,b₂,b₃} = {b₂,b₁,b₃}

proof end;

theorem Th100: :: ENUMSET1:100

for b₁, b₂, b₃ being set holds {b₁,b₂,b₃} = {b₂,b₃,b₁}

proof end;

theorem Th101: :: ENUMSET1:101

canceled;

theorem Th102: :: ENUMSET1:102

for b₁, b₂, b₃ being set holds {b₁,b₂,b₃} = {b₃,b₂,b₁}

proof end;

theorem Th103: :: ENUMSET1:103

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₁,b₂,b₄,b₃}

proof end;

theorem Th104: :: ENUMSET1:104

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₁,b₃,b₂,b₄}

proof end;

theorem Th105: :: ENUMSET1:105

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₁,b₃,b₄,b₂}

proof end;

theorem Th106: :: ENUMSET1:106

canceled;

theorem Th107: :: ENUMSET1:107

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₁,b₄,b₃,b₂}

proof end;

theorem Th108: :: ENUMSET1:108

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₂,b₁,b₃,b₄}

proof end;

Lemma58: for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₂,b₃,b₁,b₄}

proof end;

theorem Th109: :: ENUMSET1:109

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₂,b₁,b₄,b₃}

proof end;

theorem Th110: :: ENUMSET1:110

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₂,b₃,b₁,b₄} by Lemma58;

theorem Th111: :: ENUMSET1:111

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₂,b₃,b₄,b₁}

proof end;

theorem Th112: :: ENUMSET1:112

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₂,b₄,b₁,b₃}

proof end;

theorem Th113: :: ENUMSET1:113

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₂,b₄,b₃,b₁}

proof end;

Lemma59: for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₃,b₂,b₁,b₄}

proof end;

theorem Th114: :: ENUMSET1:114

canceled;

theorem Th115: :: ENUMSET1:115

canceled;

theorem Th116: :: ENUMSET1:116

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₃,b₂,b₁,b₄} by Lemma59;

theorem Th117: :: ENUMSET1:117

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₃,b₂,b₄,b₁}

proof end;

theorem Th118: :: ENUMSET1:118

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₃,b₄,b₁,b₂}

proof end;

theorem Th119: :: ENUMSET1:119

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₃,b₄,b₂,b₁}

proof end;

theorem Th120: :: ENUMSET1:120

canceled;

theorem Th121: :: ENUMSET1:121

canceled;

theorem Th122: :: ENUMSET1:122

canceled;

theorem Th123: :: ENUMSET1:123

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₄,b₂,b₃,b₁}

proof end;

theorem Th124: :: ENUMSET1:124

canceled;

theorem Th125: :: ENUMSET1:125

for b₁, b₂, b₃, b₄ being set holds {b₁,b₂,b₃,b₄} = {b₄,b₃,b₂,b₁}

proof end;