Skip to content

Commit

Permalink
rewrap
Browse files Browse the repository at this point in the history
  • Loading branch information
@sctfn
sctfn committed Feb 4, 2025
1 parent 13b593b commit 531625b
Showing 1 changed file with 33 additions and 32 deletions.
65 changes: 33 additions & 32 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80129,8 +80129,8 @@ Power Set ( ~ ax-pow ). (Contributed by Mario Carneiro, 20-May-2013.)
ralxp3f.3 $e |- F/ w ph $.
ralxp3f.4 $e |- F/ x ps $.
ralxp3f.5 $e |- ( x = <. y , z , w >. -> ( ph <-> ps ) ) $.
$( Restricted for all over a triple Cartesian product. (Contributed by Scott
Fenton, 22-Aug-2024.) $)
$( Restricted for all over a triple Cartesian product. (Contributed by
Scott Fenton, 22-Aug-2024.) $)
ralxp3f $p |- ( A. x e. ( ( A X. B ) X. C ) ph <->
A. y e. A A. z e. B A. w e. C ps ) $=
( wral cv wi wal wrex ralbii wcel cotp df-ral el2xptp imbi1i r19.23 bitri
Expand All @@ -80145,8 +80145,8 @@ Power Set ( ~ ax-pow ). (Contributed by Mario Carneiro, 20-May-2013.)
$d A w x y z $. $d B w x y z $. $d C w x y z $. $d ph w y z $.
$d ps x $.
ralxp3.1 $e |- ( x = <. y , z , w >. -> ( ph <-> ps ) ) $.
$( Restricted for all over a triple Cartesian product. (Contributed by Scott
Fenton, 2-Feb-2025.) $)
$( Restricted for all over a triple Cartesian product. (Contributed by
Scott Fenton, 2-Feb-2025.) $)
ralxp3 $p |- ( A. x e. ( ( A X. B ) X. C ) ph <->
A. y e. A A. z e. B A. w e. C ps ) $=
( nfv ralxp3f ) ABCDEFGHIADKAEKAFKBCKJL $.
Expand Down Expand Up @@ -80225,8 +80225,8 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
frpoins3xp3g.5 $e |- ( x = X -> ( ph <-> ta ) ) $.
frpoins3xp3g.6 $e |- ( y = Y -> ( ta <-> et ) ) $.
frpoins3xp3g.7 $e |- ( z = Z -> ( et <-> ze ) ) $.
$( Special case of founded partial recursion over a triple Cartesian product.
(Contributed by Scott Fenton, 22-Aug-2024.) $)
$( Special case of founded partial recursion over a triple Cartesian
product. (Contributed by Scott Fenton, 22-Aug-2024.) $)
frpoins3xp3g $p |- ( ( ( R Fr ( ( A X. B ) X. C )
/\ R Po ( ( A X. B ) X. C )
/\ R Se ( ( A X. B ) X. C ) ) /\ ( X e. A /\ Y e. B /\ Z e. C ) )
Expand Down Expand Up @@ -80276,8 +80276,9 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
${
$d A x y $. $d B x y $. $d a x y $. $d b x y $. $d c x y $.
$d d x y $. $d R x y $. $d S x y $.
$( Lemma for Cartesian product ordering. Calculate the value of the Cartesian
product relation. (Contributed by Scott Fenton, 19-Aug-2024.) $)
$( Lemma for Cartesian product ordering. Calculate the value of the
Cartesian product relation. (Contributed by Scott Fenton,
19-Aug-2024.) $)
xpord2lem $p |- ( <. a , b >. T <. c , d >. <->
( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) /\
( ( a R c \/ a = c ) /\ ( b S d \/ b = d ) /\
Expand Down Expand Up @@ -80364,8 +80365,8 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
$d T a b c d e f p q s $. $d ph a b c d e f p q s $.
frxp2.1 $e |- ( ph -> R Fr A ) $.
frxp2.2 $e |- ( ph -> S Fr B ) $.
$( Another way of giving a founded order to a Cartesian product of two
classes. (Contributed by Scott Fenton, 19-Aug-2024.) $)
$( Another way of giving a well-founded order to a Cartesian product of
two classes. (Contributed by Scott Fenton, 19-Aug-2024.) $)
frxp2 $p |- ( ph -> T Fr ( A X. B ) ) $=
( va vc ve cv c0 wa wn wi wcel vs vq vp vb vd cxp wss wne wbr wral wrex
vf wal wfr cdm dmss ad2antrl dmxpss sstrdi simprr wrel wceq relxp relss
Expand Down Expand Up @@ -80455,8 +80456,8 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
$d S a b p x y $. $d T a b p $.
sexp2.1 $e |- ( ph -> R Se A ) $.
sexp2.2 $e |- ( ph -> S Se B ) $.
$( Condition for the relation in ~ frxp2 to be set-like.
(Contributed by Scott Fenton, 19-Aug-2024.) $)
$( Condition for the relation in ~ frxp2 to be set-like. (Contributed by
Scott Fenton, 19-Aug-2024.) $)
sexp2 $p |- ( ph -> T Se ( A X. B ) ) $=
( vp va vb cv cpred cvv wcel wse csn cxp wral cop wceq wrex wa cun cdif
elxp2 xpord2pred adantl setlikespec sylan adantrr vsnex a1i unexd xpexd
Expand Down Expand Up @@ -80577,8 +80578,8 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
poxp3.1 $e |- ( ph -> R Po A ) $.
poxp3.2 $e |- ( ph -> S Po B ) $.
poxp3.3 $e |- ( ph -> T Po C ) $.
$( Triple Cartesian product partial ordering. (Contributed by Scott Fenton,
21-Aug-2024.) $)
$( Triple Cartesian product partial ordering. (Contributed by Scott
Fenton, 21-Aug-2024.) $)
poxp3 $p |- ( ph -> U Po ( ( A X. B ) X. C ) ) $=
( va vb wbr wrex w3a wa vp vq vr vc vd ve vf vg vh vi cv wcel cotp wceq
cxp wn el2xptp weq wo wne w3o neirr 3pm3.2ni intnan simp3 mto wb breq12
Expand Down Expand Up @@ -80650,8 +80651,8 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
frxp3.1 $e |- ( ph -> R Fr A ) $.
frxp3.2 $e |- ( ph -> S Fr B ) $.
frxp3.3 $e |- ( ph -> T Fr C ) $.
$( Give well-foundedness over a triple Cartesian product. (Contributed by Scott
Fenton, 21-Aug-2024.) $)
$( Give well-foundedness over a triple Cartesian product. (Contributed
by Scott Fenton, 21-Aug-2024.) $)
frxp3 $p |- ( ph -> U Fr ( ( A X. B ) X. C ) ) $=
( cv wss c0 wa wn wcel vs vq vp vd va ve vb vf vc vg vh vi cxp wne wral
wbr wrex wi wal wfr cdm cvv vex dmex adantr dmss ad2antrl dmxpss sstrdi
Expand Down Expand Up @@ -102967,11 +102968,11 @@ a Cantor normal form (and injectivity, together with coherence

${
$d R f n m x y $.
$( Define the transitive closure of a class. This is the smallest
relation containing ` R ` (or more precisely, the relation
` ( R |`` _V ) ` induced by ` R ` ) and having the transitive property.
Definition from [Levy] p. 59, who denotes it as ` R * ` and calls it the
"ancestral" of ` R ` . (Contributed by Scott Fenton, 17-Oct-2024.) $)
$( Define the transitive closure of a class. This is the smallest relation
containing ` R ` (or more precisely, the relation ` ( R |`` _V ) `
induced by ` R ` ) and having the transitive property. Definition from
[Levy] p. 59, who denotes it as ` R * ` and calls it the "ancestral" of
` R ` . (Contributed by Scott Fenton, 17-Oct-2024.) $)
df-ttrcl $a |- t++ R = { <. x , y >. | E. n e. ( _om \ 1o )
E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\
A. m e. n ( f ` m ) R ( f ` suc m ) ) } $.
Expand Down Expand Up @@ -103212,16 +103213,16 @@ a Cantor normal form (and injectivity, together with coherence
CTDEABFCTUP $.
$}

$( Composition law for the transitive closure of a relation.
(Contributed by Scott Fenton, 20-Oct-2024.) $)
$( Composition law for the transitive closure of a relation. (Contributed by
Scott Fenton, 20-Oct-2024.) $)
ttrclco $p |- ( t++ R o. R ) C_ t++ R $=
( cvv cres cttrcl ccom wrel wss ssttrcl coss2 mp2b ttrcltr sstri wceq relco
relres dfrel3 mpbi resco ttrclresv coeq1i 3eqtr3i 3sstr3i ) ABCZDZUCEZUDADZ
AEZUFUEUDUDEZUDUCFUCUDGUEUHGABOUCHUCUDUDIJUCKLUDAEZBCZUIUEUGUIFUJUIMUDANUIP
QUDABRUDUFAASZTUAUKUB $.

$( Composition law for the transitive closure of a relation.
(Contributed by Scott Fenton, 20-Oct-2024.) $)
$( Composition law for the transitive closure of a relation. (Contributed by
Scott Fenton, 20-Oct-2024.) $)
cottrcl $p |- ( R o. t++ R ) C_ t++ R $=
( cvv cres cttrcl ccom wss wrel relres ssttrcl ax-mp coss1 ttrcltr crn wceq
sstri ssv cores ttrclresv coeq2i eqtri 3sstr3i ) ABCZUBDZEZUCAADZEZUEUDUCUC
Expand Down Expand Up @@ -103346,8 +103347,8 @@ a Cantor normal form (and injectivity, together with coherence

${
$d R z $.
$( When ` R ` is a set and a relation, then its transitive closure can
be defined by an intersection. (Contributed by Scott Fenton,
$( When ` R ` is a set and a relation, then its transitive closure can be
defined by an intersection. (Contributed by Scott Fenton,
26-Oct-2024.) $)
dfttrcl2 $p |- ( ( R e. V /\ Rel R ) -> t++ R =
|^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } ) $=
Expand Down Expand Up @@ -104009,9 +104010,9 @@ a Cantor normal form (and injectivity, together with coherence

${
$d R w z $. $d A w z $.
$( Lemma for general well-founded recursion. Establish a subset
relation. (Contributed by Scott Fenton, 11-Sep-2023.) Revised
notion of transitive closure. (Revised by Scott Fenton, 1-Dec-2024.) $)
$( Lemma for general well-founded recursion. Establish a subset relation.
(Contributed by Scott Fenton, 11-Sep-2023.) Revised notion of
transitive closure. (Revised by Scott Fenton, 1-Dec-2024.) $)
frrlem16 $p |- ( ( ( R Fr A /\ R Se A ) /\ z e. A ) ->
A. w e. Pred ( t++ ( R |` A ) , A , z )
Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) ) $=
Expand Down Expand Up @@ -538741,8 +538742,8 @@ Real and complex numbers (cont.)
${
$d a b $. $d a ph $. $d a ps $. $d a x $. $d a y $. $d b ph $.
$d b ps $. $d b x $. $d b y $. $d ph y $. $d ps x $. $d x y $.
$( Cartesian product of two class abstractions. (Contributed by Scott Fenton,
19-Aug-2024.) $)
$( Cartesian product of two class abstractions. (Contributed by Scott
Fenton, 19-Aug-2024.) $)
xpab $p |- ( { x | ph } X. { y | ps } ) = { <. x , y >. | ( ph /\ ps ) } $=
( va vb cab cxp wa copab wcel wsbc wbr wsb df-clab sban sbsbc sbv 3bitr3i
cv relxp relopabv anbi12i anbi1i sbbii anbi2i bitri bitr4i brabsb 3bitr4i
Expand Down

0 comments on commit 531625b

Please sign in to comment.