From bf17cf9ad6ba82716ab711f3a490e32ddb181747 Mon Sep 17 00:00:00 2001 From: Scott Fenton Date: Wed, 11 Dec 2024 14:38:44 -0500 Subject: [PATCH] eliminate TrPred --- set.mm | 339 --------------------------------------------------------- 1 file changed, 339 deletions(-) diff --git a/set.mm b/set.mm index 413105b502..9b6c41a885 100644 --- a/set.mm +++ b/set.mm @@ -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 $. - $} - $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=