:: ENUMSET1 semantic presentation

Show IDV graph for whole article

Lm1: for x, X, y being set holds
( x in union {X,{y}} iff ( x in X or x = y ) )

proof end;

definition

let x1, x2, x3 be set ;
func {x1,x2,x3} -> set means :Def1: :: ENUMSET1:def 1
for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 ) );
existence

proof end;

proof end;

end;

:: deftheorem Def1 defines { ENUMSET1:def 1 :

definition

let x1, x2, x3, x4 be set ;
func {x1,x2,x3,x4} -> set means :Def2: :: ENUMSET1:def 2
for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 ) );
existence

proof end;

proof end;

end;

:: deftheorem Def2 defines { ENUMSET1:def 2 :

definition

let x1, x2, x3, x4, x5 be set ;
func {x1,x2,x3,x4,x5} -> set means :Def3: :: ENUMSET1:def 3
for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) );
existence

proof end;

proof end;

end;

:: deftheorem Def3 defines { ENUMSET1:def 3 :

definition

let x1, x2, x3, x4, x5, x6 be set ;
func {x1,x2,x3,x4,x5,x6} -> set means :Def4: :: ENUMSET1:def 4
for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) );
existence

proof end;

proof end;

end;

:: deftheorem Def4 defines { ENUMSET1:def 4 :

definition

let x1, x2, x3, x4, x5, x6, x7 be set ;
func {x1,x2,x3,x4,x5,x6,x7} -> set means :Def5: :: ENUMSET1:def 5
for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) );
existence

proof end;

proof end;

end;

:: deftheorem Def5 defines { ENUMSET1:def 5 :

definition

let x1, x2, x3, x4, x5, x6, x7, x8 be set ;
func {x1,x2,x3,x4,x5,x6,x7,x8} -> set means :Def6: :: ENUMSET1:def 6
for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) );
existence

proof end;

proof end;

end;

:: deftheorem Def6 defines { ENUMSET1:def 6 :

theorem :: ENUMSET1:1

Show IDV graph

canceled;

theorem :: ENUMSET1:2

Show IDV graph

canceled;

theorem :: ENUMSET1:3

Show IDV graph

canceled;

theorem :: ENUMSET1:4

Show IDV graph

canceled;

theorem :: ENUMSET1:5

Show IDV graph

canceled;

theorem :: ENUMSET1:6

Show IDV graph

canceled;

theorem :: ENUMSET1:7

Show IDV graph

canceled;

theorem :: ENUMSET1:8

Show IDV graph

canceled;

theorem :: ENUMSET1:9

Show IDV graph

canceled;

theorem :: ENUMSET1:10

Show IDV graph

canceled;

theorem :: ENUMSET1:11

Show IDV graph

canceled;

theorem :: ENUMSET1:12

Show IDV graph

canceled;

theorem :: ENUMSET1:13

Show IDV graph

canceled;

theorem :: ENUMSET1:14

Show IDV graph

canceled;

theorem :: ENUMSET1:15

Show IDV graph

canceled;

theorem :: ENUMSET1:16

Show IDV graph

canceled;

theorem :: ENUMSET1:17

Show IDV graph

canceled;

theorem :: ENUMSET1:18

Show IDV graph

canceled;

theorem :: ENUMSET1:19

Show IDV graph

canceled;

theorem :: ENUMSET1:20

Show IDV graph

canceled;

theorem :: ENUMSET1:21

Show IDV graph

canceled;

theorem :: ENUMSET1:22

Show IDV graph

canceled;

theorem :: ENUMSET1:23

Show IDV graph

canceled;

theorem :: ENUMSET1:24

Show IDV graph

canceled;

theorem :: ENUMSET1:25

Show IDV graph

canceled;

theorem :: ENUMSET1:26

Show IDV graph

canceled;

theorem :: ENUMSET1:27

Show IDV graph

canceled;

theorem :: ENUMSET1:28

Show IDV graph

canceled;

theorem :: ENUMSET1:29

Show IDV graph

canceled;

theorem :: ENUMSET1:30

Show IDV graph

canceled;

theorem :: ENUMSET1:31

Show IDV graph

canceled;

theorem :: ENUMSET1:32

Show IDV graph

canceled;

theorem :: ENUMSET1:33

Show IDV graph

canceled;

theorem :: ENUMSET1:34

Show IDV graph

canceled;

theorem :: ENUMSET1:35

Show IDV graph

canceled;

theorem :: ENUMSET1:36

Show IDV graph

canceled;

theorem :: ENUMSET1:37

Show IDV graph

canceled;

theorem :: ENUMSET1:38

Show IDV graph

canceled;

theorem :: ENUMSET1:39

Show IDV graph

canceled;

theorem :: ENUMSET1:40

Show IDV graph

canceled;

theorem Th41: :: ENUMSET1:41

Show IDV graph

for x1, x2 being set holds {x1,x2} = {x1} \/ {x2}

proof end;

theorem Th42: :: ENUMSET1:42

Show IDV graph

for x1, x2, x3 being set holds {x1,x2,x3} = {x1} \/ {x2,x3}

proof end;

theorem Th43: :: ENUMSET1:43

Show IDV graph

for x1, x2, x3 being set holds {x1,x2,x3} = {x1,x2} \/ {x3}

proof end;

Lm2: for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4}

proof end;

theorem Th44: :: ENUMSET1:44

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4}

proof end;

theorem :: ENUMSET1:45

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4} by Lm2;

theorem Th46: :: ENUMSET1:46

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4}

proof end;

Lm3: for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5}

proof end;

theorem Th47: :: ENUMSET1:47

Show IDV graph

for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5}

proof end;

theorem Th48: :: ENUMSET1:48

Show IDV graph

for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2} \/ {x3,x4,x5}

proof end;

theorem :: ENUMSET1:49

Show IDV graph

for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} by Lm3;

theorem Th50: :: ENUMSET1:50

Show IDV graph

for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2,x3,x4} \/ {x5}

proof end;

Lm4: for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6}

proof end;

theorem Th51: :: ENUMSET1:51

Show IDV graph

for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6}

proof end;

theorem Th52: :: ENUMSET1:52

Show IDV graph

for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2} \/ {x3,x4,x5,x6}

proof end;

theorem :: ENUMSET1:53

Show IDV graph

for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by Lm4;

theorem Th54: :: ENUMSET1:54

Show IDV graph

for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4} \/ {x5,x6}

proof end;

theorem :: ENUMSET1:55

Show IDV graph

for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6}

proof end;

Lm5: for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7}

proof end;

theorem Th56: :: ENUMSET1:56

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1} \/ {x2,x3,x4,x5,x6,x7}

proof end;

theorem Th57: :: ENUMSET1:57

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2} \/ {x3,x4,x5,x6,x7}

proof end;

theorem Th58: :: ENUMSET1:58

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3} \/ {x4,x5,x6,x7}

proof end;

theorem :: ENUMSET1:59

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5;

theorem :: ENUMSET1:60

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5} \/ {x6,x7}

proof end;

theorem :: ENUMSET1:61

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6} \/ {x7}

proof end;

Lm6: for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8}

proof end;

theorem :: ENUMSET1:62

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8}

proof end;

theorem Th63: :: ENUMSET1:63

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8}

proof end;

theorem :: ENUMSET1:64

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8}

proof end;

theorem :: ENUMSET1:65

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6;

theorem :: ENUMSET1:66

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8}

proof end;

theorem :: ENUMSET1:67

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8}

proof end;

theorem :: ENUMSET1:68

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8}

proof end;

theorem Th69: :: ENUMSET1:69

Show IDV graph

for x1 being set holds {x1,x1} = {x1}

proof end;

theorem Th70: :: ENUMSET1:70

Show IDV graph

for x1, x2 being set holds {x1,x1,x2} = {x1,x2}

proof end;

theorem Th71: :: ENUMSET1:71

Show IDV graph

for x1, x2, x3 being set holds {x1,x1,x2,x3} = {x1,x2,x3}

proof end;

theorem Th72: :: ENUMSET1:72

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x1,x2,x3,x4} = {x1,x2,x3,x4}

proof end;

theorem Th73: :: ENUMSET1:73

Show IDV graph

for x1, x2, x3, x4, x5 being set holds {x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}

proof end;

theorem Th74: :: ENUMSET1:74

Show IDV graph

for x1, x2, x3, x4, x5, x6 being set holds {x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6}

proof end;

theorem Th75: :: ENUMSET1:75

Show IDV graph

for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6,x7}

proof end;

theorem :: ENUMSET1:76

Show IDV graph

for x1 being set holds {x1,x1,x1} = {x1}

proof end;

theorem Th77: :: ENUMSET1:77

Show IDV graph

for x1, x2 being set holds {x1,x1,x1,x2} = {x1,x2}

proof end;

theorem Th78: :: ENUMSET1:78

Show IDV graph

for x1, x2, x3 being set holds {x1,x1,x1,x2,x3} = {x1,x2,x3}

proof end;

theorem Th79: :: ENUMSET1:79

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}

proof end;

theorem Th80: :: ENUMSET1:80

Show IDV graph

for x1, x2, x3, x4, x5 being set holds {x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}

proof end;

theorem Th81: :: ENUMSET1:81

Show IDV graph

for x1, x2, x3, x4, x5, x6 being set holds {x1,x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6}

proof end;

theorem :: ENUMSET1:82

Show IDV graph

for x1 being set holds {x1,x1,x1,x1} = {x1}

proof end;

theorem Th83: :: ENUMSET1:83

Show IDV graph

for x1, x2 being set holds {x1,x1,x1,x1,x2} = {x1,x2}

proof end;

theorem Th84: :: ENUMSET1:84

Show IDV graph

for x1, x2, x3 being set holds {x1,x1,x1,x1,x2,x3} = {x1,x2,x3}

proof end;

theorem Th85: :: ENUMSET1:85

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}

proof end;

theorem Th86: :: ENUMSET1:86

Show IDV graph

for x1, x2, x3, x4, x5 being set holds {x1,x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}

proof end;

theorem :: ENUMSET1:87

Show IDV graph

for x1 being set holds {x1,x1,x1,x1,x1} = {x1}

proof end;

theorem Th88: :: ENUMSET1:88

Show IDV graph

for x1, x2 being set holds {x1,x1,x1,x1,x1,x2} = {x1,x2}

proof end;

theorem Th89: :: ENUMSET1:89

Show IDV graph

for x1, x2, x3 being set holds {x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}

proof end;

theorem Th90: :: ENUMSET1:90

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}

proof end;

theorem :: ENUMSET1:91

Show IDV graph

for x1 being set holds {x1,x1,x1,x1,x1,x1} = {x1}

proof end;

theorem Th92: :: ENUMSET1:92

Show IDV graph

for x1, x2 being set holds {x1,x1,x1,x1,x1,x1,x2} = {x1,x2}

proof end;

theorem Th93: :: ENUMSET1:93

Show IDV graph

for x1, x2, x3 being set holds {x1,x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}

proof end;

theorem :: ENUMSET1:94

Show IDV graph

for x1 being set holds {x1,x1,x1,x1,x1,x1,x1} = {x1}

proof end;

theorem Th95: :: ENUMSET1:95

Show IDV graph

for x1, x2 being set holds {x1,x1,x1,x1,x1,x1,x1,x2} = {x1,x2}

proof end;

theorem :: ENUMSET1:96

Show IDV graph

for x1 being set holds {x1,x1,x1,x1,x1,x1,x1,x1} = {x1}

proof end;

theorem :: ENUMSET1:97

Show IDV graph

canceled;

theorem Th98: :: ENUMSET1:98

Show IDV graph

for x1, x2, x3 being set holds {x1,x2,x3} = {x1,x3,x2}

proof end;

theorem Th99: :: ENUMSET1:99

Show IDV graph

for x1, x2, x3 being set holds {x1,x2,x3} = {x2,x1,x3}

proof end;

theorem Th100: :: ENUMSET1:100

Show IDV graph

for x1, x2, x3 being set holds {x1,x2,x3} = {x2,x3,x1}

proof end;

theorem :: ENUMSET1:101

Show IDV graph

canceled;

theorem Th102: :: ENUMSET1:102

Show IDV graph

for x1, x2, x3 being set holds {x1,x2,x3} = {x3,x2,x1}

proof end;

theorem Th103: :: ENUMSET1:103

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2,x4,x3}

proof end;

theorem :: ENUMSET1:104

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x3,x2,x4}

proof end;

theorem Th105: :: ENUMSET1:105

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x3,x4,x2}

proof end;

theorem :: ENUMSET1:106

Show IDV graph

canceled;

theorem Th107: :: ENUMSET1:107

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x4,x3,x2}

proof end;

theorem Th108: :: ENUMSET1:108

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x1,x3,x4}

proof end;

Lm7: for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x3,x1,x4}

proof end;

theorem :: ENUMSET1:109

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x1,x4,x3}

proof end;

theorem :: ENUMSET1:110

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x3,x1,x4} by Lm7;

theorem :: ENUMSET1:111

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x3,x4,x1}

proof end;

theorem :: ENUMSET1:112

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x4,x1,x3}

proof end;

theorem :: ENUMSET1:113

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x4,x3,x1}

proof end;

Lm8: for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x2,x1,x4}

proof end;

theorem :: ENUMSET1:114

Show IDV graph

canceled;

theorem :: ENUMSET1:115

Show IDV graph

canceled;

theorem :: ENUMSET1:116

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x2,x1,x4} by Lm8;

theorem :: ENUMSET1:117

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x2,x4,x1}

proof end;

theorem :: ENUMSET1:118

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x4,x1,x2}

proof end;

theorem Th119: :: ENUMSET1:119

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x4,x2,x1}

proof end;

theorem :: ENUMSET1:120

Show IDV graph

canceled;

theorem :: ENUMSET1:121

Show IDV graph

canceled;

theorem :: ENUMSET1:122

Show IDV graph

canceled;

theorem :: ENUMSET1:123

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x4,x2,x3,x1}

proof end;

theorem :: ENUMSET1:124

Show IDV graph

canceled;

theorem :: ENUMSET1:125

Show IDV graph

for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x4,x3,x2,x1}

proof end;