Skip to content

Commit

Permalink
eliminate TrPred
Browse files Browse the repository at this point in the history
  • Loading branch information
@sctfn
sctfn committed Dec 11, 2024
1 parent 81b20d9 commit bf17cf9
Showing 1 changed file with 0 additions and 339 deletions.
339 changes: 0 additions & 339 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100940,345 +100940,6 @@ a Cantor normal form (and injectivity, together with coherence
QXPWQMNXQWPQVSVTVOWAWBWCCAWHWDWE $.
$}

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Transitive closure under a relationship
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

$c TrPred $.
$( Define the transitive predecessor class as a class. $)
ctrpred $a class TrPred ( R , A , X ) $.

${
$d R a y $. $d A a y $. $d X a y $.
$( Define the transitive predecessors of a class ` X ` under a relation
` R ` in a class ` A ` . This class can be thought of as the "smallest"
class containing all elements of ` A ` that are linked to ` X ` by an
` R ` -chain (see ~ trpredtr and ~ trpredmintr ). Definition based on
Theorem 8.4 of Don Monk's notes for Advanced Set Theory, which can be
found at ~ https://euclid.colorado.edu/~~monkd/setth.pdf . (Contributed
by Scott Fenton, 2-Feb-2011.) $)
df-trpred $a |- TrPred ( R , A , X ) =
U. ran ( rec ( ( a e. _V |->
U_ y e. a Pred ( R , A , y ) ) ,
Pred ( R , A , X ) ) |` _om ) $.
$}

${
$d R a i y $. $d A a i y $. $d X a i y $.
$( A definition of the transitive predecessors of a class in terms of
indexed union. (Contributed by Scott Fenton, 28-Apr-2012.) $)
dftrpred2 $p |- TrPred ( R , A , X ) =
U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) ,
Pred ( R , A , X ) ) |` _om ) ` i ) $=
( ctrpred cvv cv cpred ciun cmpt crdg com cres crn cuni cfv df-trpred wfn
wceq frfnom fniunfv ax-mp eqtr4i ) BCEGFHAFIBCAIJKLZBCEJZMNOZPQZDNDIUHRKZ
ABCEFSUHNTUJUIUAUGUFUBDNUHUCUDUE $.
$}

${
$d R a y $. $d S a y $. $d A a y $. $d B a y $. $d X a y $.
$d Y a y $.

$( Equality theorem for transitive predecessors. (Contributed by Scott
Fenton, 2-Feb-2011.) $)
trpredeq1 $p |- ( R = S -> TrPred ( R , A , X ) = TrPred ( S , A , X ) ) $=
( va vy wceq cvv cpred ciun cmpt crdg com cres crn cuni ctrpred df-trpred
cv predeq1 iuneq2d mpteq2dv rdgeq12 syl2anc reseq1d rneqd unieqd 3eqtr4g
) BCGZEHFESZABFSZIZJZKZABDIZLZMNZOZPEHFUJACUKIZJZKZACDIZLZMNZOZPABDQACDQU
IURVEUIUQVDUIUPVCMUIUNVAGUOVBGUPVCGUIEHUMUTUIFUJULUSABCUKTUAUBABCDTUOVBUN
VAUCUDUEUFUGFABDERFACDERUH $.

$( Equality theorem for transitive predecessors. (Contributed by Scott
Fenton, 2-Feb-2011.) $)
trpredeq2 $p |- ( A = B -> TrPred ( R , A , X ) = TrPred ( R , B , X ) ) $=
( va vy wceq cvv cpred ciun cmpt crdg com cres crn cuni ctrpred df-trpred
cv predeq2 iuneq2d mpteq2dv rdgeq12 reseq1d syl2anc rneqd unieqd 3eqtr4g
wa ) ABGZEHFESZACFSZIZJZKZACDIZLZMNZOZPEHFUKBCULIZJZKZBCDIZLZMNZOZPACDQBC
DQUJUSVFUJURVEUJUOVBGZUPVCGZURVEGUJEHUNVAUJFUKUMUTABCULTUAUBABCDTVGVHUIUQ
VDMUPVCUOVBUCUDUEUFUGFACDERFBCDERUH $.

$( Equality theorem for transitive predecessors. (Contributed by Scott
Fenton, 2-Feb-2011.) $)
trpredeq3 $p |- ( X = Y -> TrPred ( R , A , X ) = TrPred ( R , A , Y ) ) $=
( va vy wceq cvv cpred ciun cmpt crdg com cres crn cuni ctrpred df-trpred
cv predeq3 rdgeq2 syl reseq1d rneqd unieqd 3eqtr4g ) CDGZEHFESABFSIJKZABC
IZLZMNZOZPUHABDIZLZMNZOZPABCQABDQUGULUPUGUKUOUGUJUNMUGUIUMGUJUNGABCDTUIUM
UHUAUBUCUDUEFABCERFABDERUF $.
$}

${
trpredeq1d.1 $e |- ( ph -> R = S ) $.
$( Equality deduction for transitive predecessors. (Contributed by Scott
Fenton, 2-Feb-2011.) $)
trpredeq1d $p |- ( ph -> TrPred ( R , A , X ) = TrPred ( S , A , X ) ) $=
( wceq ctrpred trpredeq1 syl ) ACDGBCEHBDEHGFBCDEIJ $.
$}

${
trpredeq2d.1 $e |- ( ph -> A = B ) $.
$( Equality deduction for transitive predecessors. (Contributed by Scott
Fenton, 2-Feb-2011.) $)
trpredeq2d $p |- ( ph -> TrPred ( R , A , X ) = TrPred ( R , B , X ) ) $=
( wceq ctrpred trpredeq2 syl ) ABCGBDEHCDEHGFBCDEIJ $.
$}

${
trpredeq3d.1 $e |- ( ph -> X = Y ) $.
$( Equality deduction for transitive predecessors. (Contributed by Scott
Fenton, 2-Feb-2011.) $)
trpredeq3d $p |- ( ph -> TrPred ( R , A , X ) = TrPred ( R , A , Y ) ) $=
( wceq ctrpred trpredeq3 syl ) ADEGBCDHBCEHGFBCDEIJ $.
$}

${
$d R a y i $. $d A a y i $. $d X a y i $. $d Y a y i $.
$( A class is a transitive predecessor iff it is in some value of the
underlying function. This theorem is not meant to be used directly; use
~ trpredpred and ~ trpredmintr instead. (Contributed by Scott Fenton,
28-Apr-2012.) $)
eltrpred $p |- ( Y e. TrPred ( R , A , X ) <->
E. i e. _om Y e. ( ( rec ( ( a e. _V |->
U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) $=
( ctrpred wcel com cv cvv cpred ciun cmpt crdg cres cfv wrex dftrpred2
eleq2i eliun bitri ) FBCEHZIFDJDKGLAGKBCAKMNOBCEMPJQRZNZIFUEIDJSUDUFFABCD
EGTUADFJUEUBUC $.
$}

${
$d A a e j $. $d A a e y $. $d B j $. $d i j $. $d j y $.
$d R a e j $. $d R y $. $d X a e j $.
$( Technical lemma for transitive predecessors properties. All values of
the transitive predecessors' underlying function are subclasses of the
base class. (Contributed by Scott Fenton, 28-Apr-2012.) $)
trpredlem1 $p |- ( Pred ( R , A , X ) e. B ->
( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) ,
Pred ( R , A , X ) ) |` _om ) ` i ) C_ A ) $=
( vj ve cv com wcel cpred cvv cfv wss c0 wceq eqsstrdi nfcv nn0suc predss
ciun cmpt crdg cres wi csuc wrex wo fr0g fveq2 sseq1d syl5ibr nfrdg nfres
wa nfmpt1 nffv predeq3 cbviunv mpteq2i rdgeq1 reseq1 mp2b iuneq1 frsucmpt
nfiun iunss a1i mprgbir wn frsucmptn adantl pm2.61dan adantr wb rexlimiva
0ss mpbird a1d jaoi syl nfvres pm2.61i ) EJZKLZBDFMZCLZWFGNAGJZBDAJZMZUCZ
UDZWHUEZKUFZOZBPZUGZWGWFQRZWFHJZUHZRZHKUIZUJWSHWFUAWTWSXDWIWRWTQWPOZBPWIX
EWHBWHCWNUKBDFUBSWTWQXEBWFQWPULUMUNXDWRWIXCWRHKXAKLZXCUQWRXBWPOZBPZXFXHXC
XFIXAWPOZBDIJZMZUCZNLZXHXFXMUQXGXLBGWHXAIWJXKUCZXLWPNGWHTZGXATZIGXIXKGXAW
PGWOKGWHWNGNWMURXOUOGKTUPXPUSGXKTVHZWNGNXNUDZRWOXRWHUEZRWPXSKUFRGNWMXNAIW
JWLXKBDWKXJUTVAVBWHWNXRVCWOXSKVDVEZIWJXIXKVFZVGXLBPXKBPZIXIIXIXKBVIYBXJXI
LBDXJUBVJVKSXFXMVLZUQXGQBYCXGQRXFGWHXAXNXLWPXOXPXQXTYAVMVNBVSZSVOVPXCWRXH
VQXFXCWQXGBWFXBWPULUMVNVTVRWAWBWCWGVLZWRWIYEWQQBWFKWOWDYDSWAWE $.
$}

${
$d R a y z $. $d A a y z $. $d X a y z $.
$( Assuming it is a set, the predecessor class is a subset of the class of
transitive predecessors. (Contributed by Scott Fenton, 18-Feb-2011.) $)
trpredpred $p |- ( Pred ( R , A , X ) e. B
-> Pred ( R , A , X ) C_ TrPred ( R , A , X ) ) $=
( va vy vz cpred wcel cvv cv ciun cmpt crdg com cres crn wbr c0 syl mp2an
cuni ctrpred wss wex cfv wceq fr0g wfn wb frfnom peano1 fnbrfvb sylib 0ex
breq1 spcev elrng mpbird elssuni df-trpred sseqtrrdi ) ACDHZBIZVCEJFEKACF
KHLMZVCNOPZQZUBZACDUCVDVCVGIZVCVHUDVDVIGKZVCVFRZGUEZVDSVCVFRZVLVDSVFUFVCU
GZVMVCBVEUHVFOUISOIVNVMUJVCVEUKULOSVCVFUMUAUNVKVMGSUOVJSVCVFUPUQTGVCVFBUR
USVCVGUTTFACDEVAVB $.
$}

${
$d R a i y $. $d A a i y $. $d B i $. $d X a i y $.
$( The transitive predecessors form a subclass of the base class.
(Contributed by Scott Fenton, 20-Feb-2011.) $)
trpredss $p |- ( Pred ( R , A , X ) e. B -> TrPred ( R , A , X ) C_ A ) $=
( vi va vy cpred wcel ctrpred com cv cvv ciun cmpt crdg cfv dftrpred2 wss
cres wral trpredlem1 ralrimivw iunss sylibr eqsstrid ) ACDHZBIZACDJEKELFM
GFLACGLHNOUGPKTQZNZAGACEDFRUHUIASZEKUAUJASUHUKEKGABCEDFUBUCEKUIAUDUEUF $.
$}

${
$d A a f i j t y $. $d R a f i j t y $. $d X a f i j t y $.
$d Y a f i j t y $.
$( Predecessors of a transitive predecessor are transitive predecessors.
(Contributed by Scott Fenton, 20-Feb-2011.) (Revised by Mario Carneiro,
26-Jun-2015.) $)
trpredtr $p |- ( ( X e. A /\ R Se A ) -> ( Y e. TrPred ( R , A , X )
-> Pred ( R , A , Y ) C_ TrPred ( R , A , X ) ) ) $=
( vi va vy vt vf vj wcel cv cvv cpred ciun com wa wss syl wceq cfv simplr
ctrpred cmpt crdg cres wrex wse eltrpred csuc peano2 simpr predeq3 sseq2d
ssid rspcev ssiun sylancl wral setlikespec trpredlem1 sseld expcom adantl
fvex wi syld ralrimiv ad2antrr iunexg sylancr nfcv cbviunv iuneq1 cbvmptv
eqtrid rdgeq1 reseq1 frsucmpt syl2anc sseqtrrd fveq2 dftrpred2 rexlimdva2
mp2b sseqtrrdi syl5bi ) DABCUCZKDELZFMGFLZABGLZNZOZUDZABCNZUEZPUFZUAZKZEP
UGCAKZABUHZQZABDNZWHRZGABECDFUIXBWSXDEPXBWIPKZQZWSQZWIUJZPKZXCXHWQUAZRZXD
XGXEXIXBXEWSUBZWIUKSXGXCHWRABHLZNZOZXJXGWSXCXCRZXCXORZXFWSULXCUOWSXPQXCXN
RZHWRUGXQXRXPHDWRXMDTXNXCXCABXMDUMUNUPHWRXNXCUQSURXGXEXOMKZXJXOTXLXGWRMKX
NMKZHWRUSZXSWIWQVEXBYAXEWSXBXTHWRXBXMWRKXMAKZXTXBWRAXMXBWOMKWRARABCUTGAMB
ECFVASVBXAYBXTVFWTYBXAXTABXMUTVCVDVGVHVIHWRXNMMVJVKIWOWIHILZXNOZXOWQMIWOV
LIWIVLIXOVLWNIMYDUDZTWPYEWOUEZTWQYFPUFTFIMWMYDWJYCTWMHWJXNOYDGHWJWLXNABWK
XMUMVMHWJYCXNVNVPVOWOWNYEVQWPYFPVRWEHYCWRXNVNVSVTWAXIXKQZXCJPJLZWQUAZOZWH
YGXCYIRZJPUGXCYJRYKXKJXHPYHXHTYIXJXCYHXHWQWBUNUPJPYIXCUQSGABJCFWCWFVTWDWG
$.
$}

${
$d A y a c d i j k $. $d B y i j k $. $d R y a c d i j k $.
$d X y a c i j k $.
$( The transitive predecessors form the smallest superclass of predecessors
closed under taking predecessors. (Contributed by Scott Fenton,
25-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.) $)
trpredmintr $p |- ( ( ( X e. A /\ R Se A ) /\
( A. y e. B Pred ( R , A , y ) C_ B /\
Pred ( R , A , X ) C_ B ) ) ->
TrPred ( R , A , X ) C_ B ) $=
( vi va vc vd wcel wa cv wss wral com cvv ciun cfv wi wceq vj wse ctrpred
vk cpred cmpt crdg cres dftrpred2 c0 csuc fveq2 sseq1d imbi2d setlikespec
fr0g syl adantr simprr eqsstrd fvex trpredlem1 sseld expcom syld ralrimiv
adantl ad2antrr iunexg sylancr nfcv predeq3 cbviunv iuneq1 eqtrid cbvmptv
eqid rdgeq1 reseq1 mp2b fveq1i eqeq2i sylbi frsucmpt sylan2 sseq1i anbi2i
nfv nfra1 nfan ssel rsp ad2antrl sylan9r ralrimi sylan2b iunss sylibr a2d
exp32 finds com12 eqsstrid ) EBJZBDUBZKZBDALZUEZCMZACNZBDEUEZCMZKZKZBDEUC
FOFLZGPAGLZXHQZUFZXKUGZOUHZRZQZCABDFEGUIXNYACMZFONYBCMXNYCFOXOOJXNYCXNUAL
ZXTRZCMZSXNUJXTRZCMZSXNUDLZXTRZCMZSXNYIUKZXTRZCMZSXNYCSUAUDXOYDUJTZYFYHXN
YOYEYGCYDUJXTULUMUNYDYITZYFYKXNYPYEYJCYDYIXTULUMUNYDYLTZYFYNXNYQYEYMCYDYL
XTULUMUNYDXOTZYFYCXNYRYEYACYDXOXTULUMUNXNYGXKCXFYGXKTZXMXFXKPJZYSBDEUOZXK
PXRUPUQURXFXJXLUSUTYIOJZXNYKYNUUBXNYKYNUUBXNYKKZKZYMAYIHPIHLZBDILZUEZQZUF
ZXKUGZOUHZRZXHQZCUUCUUBUUMPJZYMUUMTUUCUULPJXHPJZAUULNZUUNYIUUKVAXFUUPXMYK
XFUUOAUULXFXGUULJZXGBJZUUOXFUULBXGXFYTUULBMUUAIBPDUDEHVBUQVCXEUURUUOSXDUU
RXEUUOBDXGUOVDVGVEVFVHAUULXHPPVIVJGXKYIXQUUMXTPGXKVKGYIVKGUUMVKXTVQXPYJTX
PUULTXQUUMTYJUULXPYIXTUUKXRUUITXSUUJTXTUUKTGHPXQUUHXPUUETXQIXPUUGQUUHAIXP
XHUUGBDXGUUFVLVMIXPUUEUUGVNVOVPXKXRUUIVRXSUUJOVSVTWAZWBAXPUULXHVNWCWDWEUU
DXIAUULNZUUMCMUUCUUBXNUULCMZKZUUTYKUVAXNYJUULCUUSWFWGUVBUUTUUBUVBXIAUULXN
UVAAXFXMAXFAWHXJXLAXIACWIXLAWHWJWJUVAAWHWJUVAUUQXGCJZXNXIUULCXGWKXJUVCXIS
XFXLXIACWLWMWNWOVGWPAUULXHCWQWRUTWTWSXAXBVFFOYACWQWRXC $.
$}

${
$d R a i j y $. $d X a i j y $.
$( The class of transitive predecessors is empty when ` A ` is empty.
(Contributed by Scott Fenton, 30-Apr-2012.) $)
trpred0 $p |- TrPred ( R , (/) , X ) = (/) $=
( vi va vy vj c0 com cv cvv cpred ciun cmpt crdg cres cfv wcel wceq pred0
iuneq2i ctrpred dftrpred2 iun0 eqtri mpteq2i rdgeq12 mp2an reseq1i fveq1i
a1i csuc wrex nn0suc fveq2 0ex fr0g ax-mp eqtrdi nfcv eqid eqidd frsucmpt
wo mpan2 fveqeq2 syl5ibrcom rexlimiv jaoi syl eqtrid 3eqtri ) GABUACHCIZD
JEDIZGAEIZKZLZMZGABKZNZHOZPZLCHGLGEGACBDUBCHWAGVLHQZWAVLDJGMZGNZHOZPZGVLV
TWEVSWDHVQWCRVRGRVSWDRDJVPGVPEVMGLGEVMVOGVOGRVNVMQAVNSUJTEVMUCUDUEABSVRGV
QWCUFUGUHUIWBVLGRZVLFIZUKZRZFHULZVCWFGRZFVLUMWGWLWKWGWFGWEPZGVLGWEUNGJQZW
MGRUOGJWCUPUQURWJWLFHWHHQZWLWJWIWEPGRZWOWNWPUODGWHGGWEJDGUSZDWHUSWQWEUTVM
WHWEPRGVAVBVDVLWIGWEVEVFVGVHVIVJTCHUCVK $.
$}

${
$d A y $. $d R y $. $d X y $. $d Y y $.
$( Given a transitive predecessor ` Y ` of ` X ` , the transitive
predecessors of ` Y ` form a subclass of the transitive predecessors of
` X ` . (Contributed by Scott Fenton, 25-Apr-2012.) (Revised by Mario
Carneiro, 26-Jun-2015.) $)
trpredelss $p |- ( ( X e. A /\ R Se A ) ->
( Y e. TrPred ( R , A , X ) ->
TrPred ( R , A , Y ) C_ TrPred ( R , A , X ) ) ) $=
( vy wcel wse wa ctrpred wss cv cpred cvv setlikespec trpredss syl sselda
wral simplr trpredtr ralrimiv adantr imp trpredmintr syl22anc ex ) CAFZAB
GZHZDABCIZFZABDIUJJZUIUKHDAFUHABEKZLUJJZEUJRZABDLUJJZULUIUJADUIABCLMFUJAJ
ABCNAMBCOPQUGUHUKSUIUOUKUIUNEUJABCUMTUAUBUIUKUPABCDTUCEAUJBDUDUEUF $.
$}

${
$d A y z $. $d R y z $. $d X y z $.
$( The transitive predecessors of ` X ` are equal to the predecessors of
` X ` together with their transitive predecessors. (Contributed by
Scott Fenton, 26-Apr-2012.) (Revised by Mario Carneiro,
26-Jun-2015.) $)
dftrpred3g $p |- ( ( X e. A /\ R Se A ) ->
TrPred ( R , A , X ) =
( Pred ( R , A , X ) u.
U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) ) $=
( vz wcel wa ctrpred cpred wss wral predel cvv setlikespec trpredpred syl
cv wi expcom syl6 wse ciun cun wo elun adantl syl5 ancld trpredeq3 sseq2d
wrex rspcev ssiun eliun ancoms adantll trpredss sseld ad2antlr syld simpr
weq imp simplr trpredelss syl2anc sstrd exp31 reximdvai syl5bi jaod ssun4
ralrimiv ssun1 jctir trpredmintr mpdan iunss sylibr unssd eqssd ) DBFZBCU
AZGZBCDHZBCDIZAWFBCAQZHZUBZUCZWDBCEQZIZWJJZEWJKZWFWJJZGWEWJJWDWNWOWDWMEWJ
WKWJFWKWFFZWKWIFZUDZWDWMWKWFWIUEWDWRWLWIJZWMWDWPWSWQWDWPWPWLBCWKHZJZGZWSW
DWPXAWPWKBFZWDXABCDWKLWCXCXARWBXCWCXAXCWCGWLMFZXABCWKNZBMCWKOZPSUFUGUHXBW
LWHJZAWFUKZWSXGXAAWKWFAEVBWHWTWLBCWGWKUIUJULAWFWHWLUMZPTWQWKWHFZAWFUKZWDW
SAWKWFWHUNWDXKXHWSWDXJXGAWFWGWFFZWGBFZWDXJXGRBCDWGLWDXMXJXGWDXMGZXJGZWLWT
WHXOXDXAXNXJXDXNXJXCXDXNWHBWKXNBCWGIMFZWHBJWCXMXPWBXMWCXPBCWGNUOUPBMCWGUQ
PURWCXCXDRWBXMXCWCXDXESUSUTVCXFPXNXJWTWHJZXNXMWCXJXQRWDXMVAWBWCXMVDBCWGWK
VEVFVCVGVHUGVIXITVJVKWLWIWFVLTVJVMWFWIVNVOEBWJCDVPVQWDWFWIWEWDWFMFWFWEJBC
DNBMCDOPZWDWHWEJZAWFKWIWEJWDXSAWFWDXLWGWEFXSWDWFWEWGXRURBCDWGVEUTVMAWFWHW
EVRVSVTWA $.
$}

${
$d A y $. $d R y $. $d X y $.
$( Another recursive expression for the transitive predecessors.
(Contributed by Scott Fenton, 27-Apr-2012.) (Revised by Mario Carneiro,
26-Jun-2015.) $)
dftrpred4g $p |- ( ( X e. A /\ R Se A ) ->
TrPred ( R , A , X ) =
U_ y e. Pred ( R , A , X ) ( { y } u. TrPred ( R , A , y ) ) ) $=
( wcel wse wa ctrpred cpred cv ciun cun csn dftrpred3g iunun iunid uneq1i
eqtri eqtr4di ) DBEBCFGBCDHBCDIZATBCAJZHZKZLZATUAMZUBLKZABCDNUFATUEKZUCLU
DATUEUBOUGTUCATPQRS $.
$}

${
$d A y $. $d R y $. $d X y $.
$( If ` R ` partially orders ` A ` , then the transitive predecessors are
the same as the immediate predecessors . (Contributed by Scott Fenton,
28-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.) $)
trpredpo $p |- ( ( R Po A /\ X e. A /\ R Se A ) ->
TrPred ( R , A , X ) = Pred ( R , A , X ) ) $=
( vy wpo wcel wse w3a ctrpred cpred cv wss simp2 simp3 wa predpo ralrimiv
wral 3adant3 cvv ssidd trpredmintr syl22anc setlikespec syl 3adant1 eqssd
trpredpred ) ABEZCAFZABGZHZABCIZABCJZULUJUKABDKZJUNLZDUNRZUNUNLUMUNLUIUJU
KMUIUJUKNUIUJUQUKUIUJOUPDUNABCUOPQSULUNUADAUNBCUBUCUJUKUNUMLZUIUJUKOUNTFU
RABCUDATBCUHUEUFUG $.
$}

${
$d A z $. $d R z $. $d X z $. $d Y z $. $d A a i j y z $.
$d R a i j y $. $d X a i j y $. $d Y a i j y $.
$( A transitive predecessor of ` X ` is either an immediate predecessor of
` X ` or an immediate predecessor of a transitive predecessor of ` X ` .
(Contributed by Scott Fenton, 9-May-2012.) (Revised by Mario Carneiro,
26-Jun-2015.) $)
trpredrec $p |- ( ( X e. A /\ R Se A ) ->
( Y e. TrPred ( R , A , X ) -> ( Y e. Pred ( R , A , X ) \/
E. z e. TrPred ( R , A , X ) Y R z ) ) ) $=
( vi va vy vj wcel cv cvv ciun com cfv wrex wa wceq wi eleq2d ctrpred wse
cpred cmpt crdg cres wbr wo eltrpred csuc nn0suc fveq2 anbi2d setlikespec
c0 biimpd fr0g syl biimpa syl6com wral wss trpredlem1 sseld expcom adantl
fvex syld ralrimiv iunexg sylancr nfcv nfmpt1 nfrdg nfres nffv nfiun eqid
predeq3 cbviunv iuneq1 eqtrid frsucmpt sylan2 expimpd dftrpred2 sseqtrrdi
eliun ssiun2 vex elpredim a1i anim12d reximdv2 com12 sylbi com23 rexlimdv
pm2.43d orim12d ex syl5 syl5bi ) EBCDUAZJEFKZGLHGKZBCHKZUCZMZUDZBCDUCZUEZ
NUFZOZJZFNPDBJZBCUBZQZEXKJZEAKZCUGZAXDPZUHZHBCFDEGUIXRXOYCFNXENJXEUORZXEI
KZUJZRZINPZUHZXRXOYCSIXEUKXRXOYIYCXRXOYIYCSXRXOQZYDXSYHYBYDYJXREUOXMOZJZQ
ZXSYDYJYMYDXOYLXRYDXNYKEXEUOXMULTUMUPXRYLXSXRYKXKEXRXKLJZYKXKRBCDUNZXKLXJ
UQURTUSUTYJYGYBINYJYGYENJZYBYGYJXREYFXMOZJZQZYPYBSZYGYJYSYGXOYRXRYGXNYQEX
EYFXMULTUMUPYSYPYBYPYSEAYEXMOZBCXTUCZMZJZYTYPXRYRUUDYPXRQZYRUUDUUEYQUUCEX
RYPUUCLJZYQUUCRXRUUALJUUBLJZAUUAVAUUFYEXMVGXRUUGAUUAXRXTUUAJZXTBJZUUGXRUU
ABXTXRYNUUABVBYOHBLCIDGVCURVDXQUUIUUGSXPUUIXQUUGBCXTUNVEVFVHVIAUUAUUBLLVJ
VKGXKYEXIUUCXMLGXKVLZGYEVLZAGUUAUUBGYEXMGXLNGXKXJGLXIVMUUJVNGNVLVOUUKVPGU
UBVLVQXMVRXFUUARXIAXFUUBMUUCHAXFXHUUBBCXGXTVSVTAXFUUAUUBWAWBWCWDTUPWEUUDE
UUBJZAUUAPZYTAEUUAUUBWHYPUUMYBYPUULYAAUUAXDYPUUHXTXDJUULYAYPUUAXDXTYPUUAI
NUUAMXDINUUAWIHBCIDGWFWGVDUULYASYPBCXTEAWJWKWLWMWNWOWPUTWSUTWQWRWTXAWQXBW
RXC $.
$}

${
$d R a y $. $d A a y $. $d X a y $.
$( The transitive predecessors under a relation form a set.

This is the first theorem in the transitive predecessor series that
requires the axiom of infinity. (Contributed by Scott Fenton,
18-Feb-2011.) $)
trpredex $p |- TrPred ( R , A , X ) e. _V $=
( va vy ctrpred cvv cpred ciun cmpt crdg com cres crn cuni df-trpred wcel
cv wfn frfnom omex fnex mp2an rnex uniex eqeltri ) ABCFDGEDRABERHIJZABCHZ
KLMZNZOGEABCDPUJUIUILSLGQUIGQUHUGTUALGUIUBUCUDUEUF $.
$}


$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Expand Down

0 comments on commit bf17cf9

Please sign in to comment.