:: MCART_1 semantic presentation

theorem Th1: :: MCART_1:1

for b₁ being set st b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & b₂ misses b₁ )

proof end;

theorem Th2: :: MCART_1:2

for b₁ being set st b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & ( for b₃ being set st b₃ in b₂ holds
b₃ misses b₁ ) )

proof end;

theorem Th3: :: MCART_1:3

for b₁ being set st b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & ( for b₃, b₄ being set st b₃ in b₄ & b₄ in b₂ holds
b₃ misses b₁ ) )

proof end;

theorem Th4: :: MCART_1:4

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

proof end;

theorem Th5: :: MCART_1:5

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

proof end;

theorem Th6: :: MCART_1:6

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

proof end;

definition

let c₁ be set ;
given c₂, c₃ being set such that E5: c₁ = [c₂,c₃] ;
func c₁ `1 -> set means :Def1: :: MCART_1:def 1
for b₁, b₂ being set st a₁ = [b₁,b₂] holds
a₂ = b₁;
existence

proof end;

uniqueness

proof end;

func c₁ `2 -> set means :Def2: :: MCART_1:def 2
for b₁, b₂ being set st a₁ = [b₁,b₂] holds
a₂ = b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines `1 MCART_1:def 1 :

:: deftheorem Def2 defines `2 MCART_1:def 2 :

theorem Th7: :: MCART_1:7

for b₁, b₂ being set holds
( [b₁,b₂] `1 = b₁ & [b₁,b₂] `2 = b₂ ) by Def1, Def2;

theorem Th8: :: MCART_1:8

for b₁ being set st ex b₂, b₃ being set st b₁ = [b₂,b₃] holds
[(b₁ `1 ),(b₁ `2 )] = b₁

proof end;

theorem Th9: :: MCART_1:9

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

proof end;

theorem Th10: :: MCART_1:10

for b₁, b₂, b₃ being set st b₁ in [:b₂,b₃:] holds
( b₁ `1 in b₂ & b₁ `2 in b₃ )

proof end;

theorem Th11: :: MCART_1:11

for b₁, b₂, b₃ being set st ex b₄, b₅ being set st b₁ = [b₄,b₅] & b₁ `1 in b₂ & b₁ `2 in b₃ holds
b₁ in [:b₂,b₃:]

proof end;

theorem Th12: :: MCART_1:12

for b₁, b₂, b₃ being set st b₁ in [:{b₂},b₃:] holds
( b₁ `1 = b₂ & b₁ `2 in b₃ )

proof end;

theorem Th13: :: MCART_1:13

for b₁, b₂, b₃ being set st b₁ in [:b₂,{b₃}:] holds
( b₁ `1 in b₂ & b₁ `2 = b₃ )

proof end;

theorem Th14: :: MCART_1:14

for b₁, b₂, b₃ being set st b₁ in [:{b₂},{b₃}:] holds
( b₁ `1 = b₂ & b₁ `2 = b₃ )

proof end;

theorem Th15: :: MCART_1:15

for b₁, b₂, b₃, b₄ being set st b₁ in [:{b₂,b₃},b₄:] holds
( ( b₁ `1 = b₂ or b₁ `1 = b₃ ) & b₁ `2 in b₄ )

proof end;

theorem Th16: :: MCART_1:16

for b₁, b₂, b₃, b₄ being set st b₁ in [:b₂,{b₃,b₄}:] holds
( b₁ `1 in b₂ & ( b₁ `2 = b₃ or b₁ `2 = b₄ ) )

proof end;

theorem Th17: :: MCART_1:17

for b₁, b₂, b₃, b₄ being set st b₁ in [:{b₂,b₃},{b₄}:] holds
( ( b₁ `1 = b₂ or b₁ `1 = b₃ ) & b₁ `2 = b₄ )

proof end;

theorem Th18: :: MCART_1:18

for b₁, b₂, b₃, b₄ being set st b₁ in [:{b₂},{b₃,b₄}:] holds
( b₁ `1 = b₂ & ( b₁ `2 = b₃ or b₁ `2 = b₄ ) )

proof end;

theorem Th19: :: MCART_1:19

for b₁, b₂, b₃, b₄, b₅ being set st b₁ in [:{b₂,b₃},{b₄,b₅}:] holds
( ( b₁ `1 = b₂ or b₁ `1 = b₃ ) & ( b₁ `2 = b₄ or b₁ `2 = b₅ ) )

proof end;

theorem Th20: :: MCART_1:20

for b₁ being set st ex b₂, b₃ being set st b₁ = [b₂,b₃] holds
( b₁ <> b₁ `1 & b₁ <> b₁ `2 )

proof end;

theorem Th21: :: MCART_1:21

canceled;

theorem Th22: :: MCART_1:22

canceled;

theorem Th23: :: MCART_1:23

for b₁, b₂, b₃ being set st b₁ in [:b₂,b₃:] holds
b₁ = [(b₁ `1 ),(b₁ `2 )]

proof end;

theorem Th24: :: MCART_1:24

for b₁, b₂ being set st b₁ <> {} & b₂ <> {} holds
for b₃ being Element of [:b₁,b₂:] holds b₃ = [(b₃ `1 ),(b₃ `2 )]

proof end;

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

proof end;

theorem Th25: :: MCART_1:25

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

proof end;

theorem Th26: :: MCART_1:26

for b₁, b₂ being set st b₁ <> {} & b₂ <> {} holds
for b₃ being Element of [:b₁,b₂:] holds
( b₃ <> b₃ `1 & b₃ <> b₃ `2 )

proof end;

definition

let c₁, c₂, c₃ be set ;
func [c₁,c₂,c₃] -> set equals :: MCART_1:def 3
[[a₁,a₂],a₃];
coherence ;

end;

:: deftheorem Def3 defines [ MCART_1:def 3 :

theorem Th27: :: MCART_1:27

canceled;

theorem Th28: :: MCART_1:28

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

proof end;

theorem Th29: :: MCART_1:29

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

proof end;

definition

let c₁, c₂, c₃, c₄ be set ;
func [c₁,c₂,c₃,c₄] -> set equals :: MCART_1:def 4
[[a₁,a₂,a₃],a₄];
coherence ;

end;

:: deftheorem Def4 defines [ MCART_1:def 4 :

theorem Th30: :: MCART_1:30

canceled;

theorem Th31: :: MCART_1:31

for b₁, b₂, b₃, b₄ being set holds [b₁,b₂,b₃,b₄] = [[[b₁,b₂],b₃],b₄] ;

theorem Th32: :: MCART_1:32

for b₁, b₂, b₃, b₄ being set holds [b₁,b₂,b₃,b₄] = [[b₁,b₂],b₃,b₄] ;

theorem Th33: :: MCART_1:33

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

proof end;

theorem Th34: :: MCART_1:34

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

proof end;

theorem Th35: :: MCART_1:35

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

proof end;

theorem Th36: :: MCART_1:36

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

proof end;

theorem Th37: :: MCART_1:37

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

proof end;

theorem Th38: :: MCART_1:38

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

proof end;

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

proof end;

theorem Th39: :: MCART_1:39

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

proof end;

theorem Th40: :: MCART_1:40

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

proof end;

theorem Th41: :: MCART_1:41

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

proof end;

theorem Th42: :: MCART_1:42

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

proof end;

theorem Th43: :: MCART_1:43

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

proof end;

theorem Th44: :: MCART_1:44

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

proof end;

theorem Th45: :: MCART_1:45

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

proof end;

theorem Th46: :: MCART_1:46

for 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₁,b₄,b₆],[b₂,b₃,b₅],[b₂,b₄,b₅],[b₂,b₃,b₆],[b₂,b₄,b₆]}

proof end;

definition

let c₁, c₂, c₃ be set ;
assume E24: ( c₁ <> {} & c₂ <> {} & c₃ <> {} ) ;
let c₄ be Element of [:c₁,c₂,c₃:];
func c₄ `1 -> Element of a₁ means :Def5: :: MCART_1:def 5
for b₁, b₂, b₃ being set st a₄ = [b₁,b₂,b₃] holds
a₅ = b₁;
existence

proof end;

uniqueness

proof end;

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

proof end;

uniqueness

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines `1 MCART_1:def 5 :

:: deftheorem Def6 defines `2 MCART_1:def 6 :

:: deftheorem Def7 defines `3 MCART_1:def 7 :

theorem Th47: :: MCART_1:47

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

theorem Th48: :: MCART_1:48

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

proof end;

theorem Th49: :: MCART_1:49

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

proof end;

theorem Th50: :: MCART_1:50

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

proof end;

theorem Th51: :: MCART_1:51

for b₁, b₂, b₃ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} holds
for b₄ being Element of [:b₁,b₂,b₃:] holds
( b₄ <> b₄ `1 & b₄ <> b₄ `2 & b₄ <> b₄ `3 )

proof end;

theorem Th52: :: MCART_1:52

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

proof end;

theorem Th53: :: MCART_1:53

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

proof end;

theorem Th54: :: MCART_1:54

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

proof end;

theorem Th55: :: MCART_1:55

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

proof end;

theorem Th56: :: MCART_1:56

for 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₈ )

proof end;

theorem Th57: :: MCART_1:57

for 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₈ )

proof end;

theorem Th58: :: MCART_1:58

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

proof end;

Lemma35: for b₁, b₂, b₃, b₄ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} holds
for b₅ being Element of [: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₄ st b₅ = [b₆,b₇,b₈,b₉]

proof end;

definition

let c₁, c₂, c₃, c₄ be set ;
assume E36: ( c₁ <> {} & c₂ <> {} & c₃ <> {} & c₄ <> {} ) ;
let c₅ be Element of [:c₁,c₂,c₃,c₄:];
func c₅ `1 -> Element of a₁ means :Def8: :: MCART_1:def 8
for b₁, b₂, b₃, b₄ being set st a₅ = [b₁,b₂,b₃,b₄] holds
a₆ = b₁;
existence

proof end;

uniqueness

proof end;

func c₅ `2 -> Element of a₂ means :Def9: :: MCART_1:def 9
for b₁, b₂, b₃, b₄ being set st a₅ = [b₁,b₂,b₃,b₄] holds
a₆ = b₂;
existence

proof end;

uniqueness

proof end;

func c₅ `3 -> Element of a₃ means :Def10: :: MCART_1:def 10
for b₁, b₂, b₃, b₄ being set st a₅ = [b₁,b₂,b₃,b₄] holds
a₆ = b₃;
existence

proof end;

uniqueness

proof end;

func c₅ `4 -> Element of a₄ means :Def11: :: MCART_1:def 11
for b₁, b₂, b₃, b₄ being set st a₅ = [b₁,b₂,b₃,b₄] holds
a₆ = b₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines `1 MCART_1:def 8 :

:: deftheorem Def9 defines `2 MCART_1:def 9 :

:: deftheorem Def10 defines `3 MCART_1:def 10 :

:: deftheorem Def11 defines `4 MCART_1:def 11 :

theorem Th59: :: MCART_1:59

for b₁, b₂, b₃, b₄ being set st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} holds
for b₅ being Element of [:b₁,b₂,b₃,b₄:]
for b₆, b₇, b₈, b₉ being set st b₅ = [b₆,b₇,b₈,b₉] holds
( b₅ `1 = b₆ & b₅ `2 = b₇ & b₅ `3 = b₈ & b₅ `4 = b₉ ) by Def8, Def9, Def10, Def11;

theorem Th60: :: MCART_1:60

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

proof end;

theorem Th61: :: MCART_1:61

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

proof end;

theorem Th62: :: MCART_1:62

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

proof end;

theorem Th63: :: MCART_1:63

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

proof end;

theorem Th64: :: MCART_1:64

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

proof end;

theorem Th65: :: MCART_1:65

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

proof end;

theorem Th66: :: MCART_1:66

for b₁, b₂ being set st [:b₁,b₂:] <> {} holds
for b₃ being Element of [:b₁,b₂:] holds
( b₃ <> b₃ `1 & b₃ <> b₃ `2 )

proof end;

theorem Th67: :: MCART_1:67

for b₁, b₂, b₃ being set st b₁ in [:b₂,b₃:] holds
( b₁ <> b₁ `1 & b₁ <> b₁ `2 ) by Th66;

theorem Th68: :: MCART_1:68

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

theorem Th69: :: MCART_1:69

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

proof end;

theorem Th70: :: MCART_1:70

proof end;

theorem Th71: :: MCART_1:71

proof end;

theorem Th72: :: MCART_1:72

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

proof end;

theorem Th73: :: MCART_1:73

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

proof end;

theorem Th74: :: MCART_1:74

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

proof end;

theorem Th75: :: MCART_1:75

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₃:]
for b₈ being Element of [:b₄,b₅,b₆:] st b₇ = b₈ holds
( b₇ `1 = b₈ `1 & b₇ `2 = b₈ `2 & b₇ `3 = b₈ `3 )

proof end;

theorem Th76: :: MCART_1:76

for 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 Element of [:b₁,b₂,b₃:] st b₇ in [:b₄,b₅,b₆:] holds
( b₇ `1 in b₄ & b₇ `2 in b₅ & b₇ `3 in b₆ )

proof end;

theorem Th77: :: MCART_1:77

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

proof end;

theorem Th78: :: MCART_1:78

for b₁, b₂, b₃, b₄ being set
for b₅ being Element of [:b₁,b₂,b₃,b₄:] st b₁ <> {} & b₂ <> {} & b₃ <> {} & b₄ <> {} holds
for b₆, b₇, b₈, b₉ being set st b₅ = [b₆,b₇,b₈,b₉] holds
( b₅ `1 = b₆ & b₅ `2 = b₇ & b₅ `3 = b₈ & b₅ `4 = b₉ ) by Def8, Def9, Def10, Def11;

theorem Th79: :: MCART_1:79

for b₁, b₂, b₃, b₄, b₅ being set
for b₆ being Element of [:b₁,b₂,b₃,b₄:] st 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₄ st b₆ = [b₇,b₈,b₉,b₁₀] holds
b₅ = b₇ ) holds
b₅ = b₆ `1

proof end;

theorem Th80: :: MCART_1:80

proof end;

theorem Th81: :: MCART_1:81

proof end;

theorem Th82: :: MCART_1:82

proof end;

theorem Th83: :: MCART_1:83

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

proof end;

theorem Th84: :: MCART_1:84

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

proof end;

theorem Th85: :: MCART_1:85

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

proof end;

theorem Th86: :: MCART_1:86

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

proof end;

theorem Th87: :: MCART_1:87

for 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 Element of [:b₁,b₂,b₃,b₄:] st b₉ in [:b₅,b₆,b₇,b₈:] holds
( b₉ `1 in b₅ & b₉ `2 in b₆ & b₉ `3 in b₇ & b₉ `4 in b₈ )

proof end;

theorem Th88: :: MCART_1:88

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

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Subset of c₁;
let c₄ be Subset of c₂;
redefine func [: as [:c₃,c₄:] -> Subset of [:a₁,a₂:];
coherence by ZFMISC_1:119;

end;

definition

let c₁, c₂, c₃ be set ;
let c₄ be Subset of c₁;
let c₅ be Subset of c₂;
let c₆ be Subset of c₃;
redefine func [: as [:c₄,c₅,c₆:] -> Subset of [:a₁,a₂,a₃:];
coherence by Th77;

end;

definition

let c₁, c₂, c₃, c₄ be set ;
let c₅ be Subset of c₁;
let c₆ be Subset of c₂;
let c₇ be Subset of c₃;
let c₈ be Subset of c₄;
redefine func [: as [:c₅,c₆,c₇,c₈:] -> Subset of [:a₁,a₂,a₃,a₄:];
coherence by Th88;

end;

definition

let c₁ be Function;
func pr1 c₁ -> Function means :: MCART_1:def 12
( dom a₂ = dom a₁ & ( for b₁ being set st b₁ in dom a₁ holds
a₂ . b₁ = (a₁ . b₁) `1 ) );
existence

proof end;

uniqueness

proof end;

func pr2 c₁ -> Function means :: MCART_1:def 13
( dom a₂ = dom a₁ & ( for b₁ being set st b₁ in dom a₁ holds
a₂ . b₁ = (a₁ . b₁) `2 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines pr1 MCART_1:def 12 :

:: deftheorem Def13 defines pr2 MCART_1:def 13 :

definition

let c₁ be set ;
func c₁ `11 -> set equals :: MCART_1:def 14
(a₁ `1 ) `1 ;
coherence ;
func c₁ `12 -> set equals :: MCART_1:def 15
(a₁ `1 ) `2 ;
coherence ;
func c₁ `21 -> set equals :: MCART_1:def 16
(a₁ `2 ) `1 ;
coherence ;
func c₁ `22 -> set equals :: MCART_1:def 17
(a₁ `2 ) `2 ;
coherence ;

end;

:: deftheorem Def14 defines `11 MCART_1:def 14 :

:: deftheorem Def15 defines `12 MCART_1:def 15 :

:: deftheorem Def16 defines `21 MCART_1:def 16 :

:: deftheorem Def17 defines `22 MCART_1:def 17 :

theorem Th89: :: MCART_1:89

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds
( [[b₁,b₂],b₃] `11 = b₁ & [[b₁,b₂],b₃] `12 = b₂ & [b₆,[b₄,b₅]] `21 = b₄ & [b₆,[b₄,b₅]] `22 = b₅ )

proof end;