:: MCART_3 semantic presentation

theorem Th1: :: MCART_3:1

for b₁ being set st b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & ( for b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being set st b₃ in b₄ & b₄ in b₅ & b₅ in b₆ & b₆ in b₇ & b₇ in b₈ & b₈ in b₉ & b₉ in b₁₀ & b₁₀ in b₂ holds
b₃ misses b₁ ) )

proof end;

theorem Th2: :: MCART_3:2

for b₁ being set st b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & ( for b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being set st b₃ in b₄ & b₄ in b₅ & b₅ in b₆ & b₆ in b₇ & b₇ in b₈ & b₈ in b₉ & b₉ in b₁₀ & b₁₀ in b₁₁ & b₁₁ in b₂ holds
b₃ misses b₁ ) )

proof end;

definition

let c₁, c₂, c₃, c₄, c₅, c₆ be set ;
func [c₁,c₂,c₃,c₄,c₅,c₆] -> set equals :: MCART_3:def 1
[[a₁,a₂,a₃,a₄,a₅],a₆];
correctness ;

end;

:: deftheorem Def1 defines [ MCART_3:def 1 :

theorem Th3: :: MCART_3:3

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 Th4: :: MCART_3:4

canceled;

theorem Th5: :: MCART_3:5

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 Th6: :: MCART_3:6

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 Th7: :: MCART_3:7

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 Th8: :: MCART_3:8

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂ being set st [b₁,b₂,b₃,b₄,b₅,b₆] = [b₇,b₈,b₉,b₁₀,b₁₁,b₁₂] holds
( b₁ = b₇ & b₂ = b₈ & b₃ = b₉ & b₄ = b₁₀ & b₅ = b₁₁ & b₆ = b₁₂ )

proof end;

theorem Th9: :: MCART_3:9

for b₁ being set st b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & ( for b₃, b₄, b₅, b₆, b₇, b₈ being set holds
( ( not b₃ in b₁ & not b₄ in b₁ ) or not b₂ = [b₃,b₄,b₅,b₆,b₇,b₈] ) ) )

proof end;

definition

let c₁, c₂, c₃, c₄, c₅, c₆ be set ;
func [:c₁,c₂,c₃,c₄,c₅,c₆:] -> set equals :: MCART_3:def 2
[:[:a₁,a₂,a₃,a₄,a₅:],a₆:];
coherence ;

end;

:: deftheorem Def2 defines [: MCART_3:def 2 :

theorem Th10: :: MCART_3:10

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 Th11: :: MCART_3:11

canceled;

theorem Th12: :: MCART_3:12

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 Th13: :: MCART_3:13

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 Th14: :: MCART_3:14

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 Th15: :: MCART_3:15

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds
( ( b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} ) iff [:b₁,b₂,b₃,b₄,b₅,b₆:] <> {} )

proof end;

theorem Th16: :: MCART_3:16

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & [:b₁,b₂,b₃,b₄,b₅,b₆:] = [:b₇,b₈,b₉,b₁₀,b₁₁,b₁₂:] holds
( b₁ = b₇ & b₂ = b₈ & b₃ = b₉ & b₄ = b₁₀ & b₅ = b₁₁ & b₆ = b₁₂ )

proof end;

theorem Th17: :: MCART_3:17

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂ being set st [:b₁,b₂,b₃,b₄,b₅,b₆:] <> {} & [:b₁,b₂,b₃,b₄,b₅,b₆:] = [:b₇,b₈,b₉,b₁₀,b₁₁,b₁₂:] holds
( b₁ = b₇ & b₂ = b₈ & b₃ = b₉ & b₄ = b₁₀ & b₅ = b₁₁ & b₆ = b₁₂ )

proof end;

theorem Th18: :: MCART_3:18

for b₁, b₂ being set st [:b₁,b₁,b₁,b₁,b₁,b₁:] = [:b₂,b₂,b₂,b₂,b₂,b₂:] holds
b₁ = b₂

proof end;

theorem Th19: :: MCART_3:19

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} holds
for b₇ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆:] ex b₈ being Element of b₁ex b₉ being Element of b₂ex b₁₀ being Element of b₃ex b₁₁ being Element of b₄ex b₁₂ being Element of b₅ex b₁₃ being Element of b₆ st b₇ = [b₈,b₉,b₁₀,b₁₁,b₁₂,b₁₃]

proof end;

definition

let c₁, c₂, c₃, c₄, c₅, c₆ be set ;
assume E11: ( c₁ <> {} & c₂ <> {} & c₃ <> {} & c₄ <> {} & c₅ <> {} & c₆ <> {} ) ;
let c₇ be Element of [:c₁,c₂,c₃,c₄,c₅,c₆:];
func c₇ `1 -> Element of a₁ means :Def3: :: MCART_3:def 3
for b₁, b₂, b₃, b₄, b₅, b₆ being set st a₇ = [b₁,b₂,b₃,b₄,b₅,b₆] holds
a₈ = b₁;
existence

proof end;

proof end;

func c₇ `2 -> Element of a₂ means :Def4: :: MCART_3:def 4
for b₁, b₂, b₃, b₄, b₅, b₆ being set st a₇ = [b₁,b₂,b₃,b₄,b₅,b₆] holds
a₈ = b₂;
existence

proof end;

proof end;

func c₇ `3 -> Element of a₃ means :Def5: :: MCART_3:def 5
for b₁, b₂, b₃, b₄, b₅, b₆ being set st a₇ = [b₁,b₂,b₃,b₄,b₅,b₆] holds
a₈ = b₃;
existence

proof end;

proof end;

func c₇ `4 -> Element of a₄ means :Def6: :: MCART_3:def 6
for b₁, b₂, b₃, b₄, b₅, b₆ being set st a₇ = [b₁,b₂,b₃,b₄,b₅,b₆] holds
a₈ = b₄;
existence

proof end;

proof end;

func c₇ `5 -> Element of a₅ means :Def7: :: MCART_3:def 7
for b₁, b₂, b₃, b₄, b₅, b₆ being set st a₇ = [b₁,b₂,b₃,b₄,b₅,b₆] holds
a₈ = b₅;
existence

proof end;

proof end;

func c₇ `6 -> Element of a₆ means :Def8: :: MCART_3:def 8
for b₁, b₂, b₃, b₄, b₅, b₆ being set st a₇ = [b₁,b₂,b₃,b₄,b₅,b₆] holds
a₈ = b₆;
existence

proof end;

proof end;

end;

:: deftheorem Def3 defines `1 MCART_3:def 3 :

:: deftheorem Def4 defines `2 MCART_3:def 4 :

:: deftheorem Def5 defines `3 MCART_3:def 5 :

:: deftheorem Def6 defines `4 MCART_3:def 6 :

:: deftheorem Def7 defines `5 MCART_3:def 7 :

:: deftheorem Def8 defines `6 MCART_3:def 8 :

theorem Th20: :: MCART_3:20

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} holds
for b₇ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆:]
for b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃ being set st b₇ = [b₈,b₉,b₁₀,b₁₁,b₁₂,b₁₃] holds
( b₇ `1 = b₈ & b₇ `2 = b₉ & b₇ `3 = b₁₀ & b₇ `4 = b₁₁ & b₇ `5 = b₁₂ & b₇ `6 = b₁₃ ) by Def3, Def4, Def5, Def6, Def7, Def8;

theorem Th21: :: MCART_3:21

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} holds
for b₇ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆:] holds b₇ = [(b₇ `1 ),(b₇ `2 ),(b₇ `3 ),(b₇ `4 ),(b₇ `5 ),(b₇ `6 )]

proof end;

theorem Th22: :: MCART_3:22

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} holds
for b₇ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆:] holds
( b₇ `1 = ((((b₇ `1 ) `1 ) `1 ) `1 ) `1 & b₇ `2 = ((((b₇ `1 ) `1 ) `1 ) `1 ) `2 & b₇ `3 = (((b₇ `1 ) `1 ) `1 ) `2 & b₇ `4 = ((b₇ `1 ) `1 ) `2 & b₇ `5 = (b₇ `1 ) `2 & b₇ `6 = b₇ `2 )

proof end;

theorem Th23: :: MCART_3:23

for b₁, b₂, b₃, b₄, b₅, b₆ being set st ( b₁ c= [:b₁,b₂,b₃,b₄,b₅,b₆:] or b₁ c= [:b₂,b₃,b₄,b₅,b₆,b₁:] or b₁ c= [:b₃,b₄,b₅,b₆,b₁,b₂:] or b₁ c= [:b₄,b₅,b₆,b₁,b₂,b₃:] or b₁ c= [:b₅,b₆,b₁,b₂,b₃,b₄:] or b₁ c= [:b₆,b₁,b₂,b₃,b₄,b₅:] ) holds
b₁ = {}

proof end;

theorem Th24: :: MCART_3:24

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂ being set st [:b₁,b₂,b₃,b₄,b₅,b₆:] meets [:b₇,b₈,b₉,b₁₀,b₁₁,b₁₂:] holds
( b₁ meets b₇ & b₂ meets b₈ & b₃ meets b₉ & b₄ meets b₁₀ & b₅ meets b₁₁ & b₆ meets b₁₂ )

proof end;

theorem Th25: :: MCART_3:25

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 Th26: :: MCART_3:26

for b₁, b₂, b₃, b₄, b₅, b₆ being set
for b₇ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} holds
for b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃ being set st b₇ = [b₈,b₉,b₁₀,b₁₁,b₁₂,b₁₃] holds
( b₇ `1 = b₈ & b₇ `2 = b₉ & b₇ `3 = b₁₀ & b₇ `4 = b₁₁ & b₇ `5 = b₁₂ & b₇ `6 = b₁₃ ) by Def3, Def4, Def5, Def6, Def7, Def8;

theorem Th27: :: MCART_3:27

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set
for b₈ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & ( for b₉ being Element of b₁
for b₁₀ being Element of b₂
for b₁₁ being Element of b₃
for b₁₂ being Element of b₄
for b₁₃ being Element of b₅
for b₁₄ being Element of b₆ st b₈ = [b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄] holds
b₇ = b₉ ) holds
b₇ = b₈ `1

proof end;

theorem Th28: :: MCART_3:28

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set
for b₈ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & ( for b₉ being Element of b₁
for b₁₀ being Element of b₂
for b₁₁ being Element of b₃
for b₁₂ being Element of b₄
for b₁₃ being Element of b₅
for b₁₄ being Element of b₆ st b₈ = [b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄] holds
b₇ = b₁₀ ) holds
b₇ = b₈ `2

proof end;

theorem Th29: :: MCART_3:29

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set
for b₈ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & ( for b₉ being Element of b₁
for b₁₀ being Element of b₂
for b₁₁ being Element of b₃
for b₁₂ being Element of b₄
for b₁₃ being Element of b₅
for b₁₄ being Element of b₆ st b₈ = [b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄] holds
b₇ = b₁₁ ) holds
b₇ = b₈ `3

proof end;

theorem Th30: :: MCART_3:30

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set
for b₈ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & ( for b₉ being Element of b₁
for b₁₀ being Element of b₂
for b₁₁ being Element of b₃
for b₁₂ being Element of b₄
for b₁₃ being Element of b₅
for b₁₄ being Element of b₆ st b₈ = [b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄] holds
b₇ = b₁₂ ) holds
b₇ = b₈ `4

proof end;

theorem Th31: :: MCART_3:31

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set
for b₈ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & ( for b₉ being Element of b₁
for b₁₀ being Element of b₂
for b₁₁ being Element of b₃
for b₁₂ being Element of b₄
for b₁₃ being Element of b₅
for b₁₄ being Element of b₆ st b₈ = [b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄] holds
b₇ = b₁₃ ) holds
b₇ = b₈ `5

proof end;

theorem Th32: :: MCART_3:32

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set
for b₈ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & ( for b₉ being Element of b₁
for b₁₀ being Element of b₂
for b₁₁ being Element of b₃
for b₁₂ being Element of b₄
for b₁₃ being Element of b₅
for b₁₄ being Element of b₆ st b₈ = [b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄] holds
b₇ = b₁₄ ) holds
b₇ = b₈ `6

proof end;

theorem Th33: :: MCART_3:33

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st b₁ in [:b₂,b₃,b₄,b₅,b₆,b₇:] holds
ex b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃ being set st
( b₈ in b₂ & b₉ in b₃ & b₁₀ in b₄ & b₁₁ in b₅ & b₁₂ in b₆ & b₁₃ in b₇ & b₁ = [b₈,b₉,b₁₀,b₁₁,b₁₂,b₁₃] )

proof end;

theorem Th34: :: MCART_3:34

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂ being set holds
( [b₁,b₂,b₃,b₄,b₅,b₆] in [:b₇,b₈,b₉,b₁₀,b₁₁,b₁₂:] iff ( b₁ in b₇ & b₂ in b₈ & b₃ in b₉ & b₄ in b₁₀ & b₅ in b₁₁ & b₆ in b₁₂ ) )

proof end;

theorem Th35: :: MCART_3:35

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st ( for b₈ being set holds
( b₈ in b₁ iff ex b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄ being set st
( b₉ in b₂ & b₁₀ in b₃ & b₁₁ in b₄ & b₁₂ in b₅ & b₁₃ in b₆ & b₁₄ in b₇ & b₈ = [b₉,b₁₀,b₁₁,b₁₂,b₁₃,b₁₄] ) ) ) holds
b₁ = [:b₂,b₃,b₄,b₅,b₆,b₇:]

proof end;

theorem Th36: :: MCART_3:36

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} & b₅ <> {} & b₆ <> {} & b₇ <> {} & b₈ <> {} & b₉ <> {} & b₁₀ <> {} & b₁₁ <> {} & b₁₂ <> {} holds
for b₁₃ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆:]
for b₁₄ being Element of [:b₇,b₈,b₉,b₁₀,b₁₁,b₁₂:] st b₁₃ = b₁₄ holds
( b₁₃ `1 = b₁₄ `1 & b₁₃ `2 = b₁₄ `2 & b₁₃ `3 = b₁₄ `3 & b₁₃ `4 = b₁₄ `4 & b₁₃ `5 = b₁₄ `5 & b₁₃ `6 = b₁₄ `6 )

proof end;

theorem Th37: :: MCART_3:37

for b₁, b₂, b₃, b₄, b₅, b₆ being set
for b₇ being Subset of b₁
for b₈ being Subset of b₂
for b₉ being Subset of b₃
for b₁₀ being Subset of b₄
for b₁₁ being Subset of b₅
for b₁₂ being Subset of b₆
for b₁₃ being Element of [:b₁,b₂,b₃,b₄,b₅,b₆:] st b₁₃ in [:b₇,b₈,b₉,b₁₀,b₁₁,b₁₂:] holds
( b₁₃ `1 in b₇ & b₁₃ `2 in b₈ & b₁₃ `3 in b₉ & b₁₃ `4 in b₁₀ & b₁₃ `5 in b₁₁ & b₁₃ `6 in b₁₂ )

proof end;

theorem Th38: :: MCART_3:38

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂ being set st b₁ c= b₂ & b₃ c= b₄ & b₅ c= b₆ & b₇ c= b₈ & b₉ c= b₁₀ & b₁₁ c= b₁₂ holds
[:b₁,b₃,b₅,b₇,b₉,b₁₁:] c= [:b₂,b₄,b₆,b₈,b₁₀,b₁₂:]

proof end;

theorem Th39: :: MCART_3:39

for b₁, b₂, b₃, b₄, b₅, b₆ being set
for b₇ being Subset of b₁
for b₈ being Subset of b₂
for b₉ being Subset of b₃
for b₁₀ being Subset of b₄
for b₁₁ being Subset of b₅
for b₁₂ being Subset of b₆ holds [:b₇,b₈,b₉,b₁₀,b₁₁,b₁₂:] is Subset of [:b₁,b₂,b₃,b₄,b₅,b₆:] by Th38;