Metamath Proof Explorer


Theorem frminOLD

Description: Obsolete proof of frmin as of 27-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 4-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion frminOLD RFrARSeABAByBPredRBy=

Proof

Step Hyp Ref Expression
1 frss BARFrARFrB
2 sess2 BARSeARSeB
3 1 2 anim12d BARFrARSeARFrBRSeB
4 n0 BbbB
5 predeq3 y=bPredRBy=PredRBb
6 5 eqeq1d y=bPredRBy=PredRBb=
7 6 rspcev bBPredRBb=yBPredRBy=
8 7 ex bBPredRBb=yBPredRBy=
9 8 adantl RFrBRSeBbBPredRBb=yBPredRBy=
10 setlikespec bBRSeBPredRBbV
11 trpredpred PredRBbVPredRBbTrPredRBb
12 ssn0 PredRBbTrPredRBbPredRBbTrPredRBb
13 12 ex PredRBbTrPredRBbPredRBbTrPredRBb
14 11 13 syl PredRBbVPredRBbTrPredRBb
15 trpredss PredRBbVTrPredRBbB
16 14 15 jctild PredRBbVPredRBbTrPredRBbBTrPredRBb
17 10 16 syl bBRSeBPredRBbTrPredRBbBTrPredRBb
18 17 adantr bBRSeBRFrBPredRBbTrPredRBbBTrPredRBb
19 trpredex TrPredRBbV
20 sseq1 c=TrPredRBbcBTrPredRBbB
21 neeq1 c=TrPredRBbcTrPredRBb
22 20 21 anbi12d c=TrPredRBbcBcTrPredRBbBTrPredRBb
23 predeq2 c=TrPredRBbPredRcy=PredRTrPredRBby
24 23 eqeq1d c=TrPredRBbPredRcy=PredRTrPredRBby=
25 24 rexeqbi1dv c=TrPredRBbycPredRcy=yTrPredRBbPredRTrPredRBby=
26 22 25 imbi12d c=TrPredRBbcBcycPredRcy=TrPredRBbBTrPredRBbyTrPredRBbPredRTrPredRBby=
27 26 imbi2d c=TrPredRBbRFrBcBcycPredRcy=RFrBTrPredRBbBTrPredRBbyTrPredRBbPredRTrPredRBby=
28 dffr4 RFrBccBcycPredRcy=
29 sp ccBcycPredRcy=cBcycPredRcy=
30 28 29 sylbi RFrBcBcycPredRcy=
31 19 27 30 vtocl RFrBTrPredRBbBTrPredRBbyTrPredRBbPredRTrPredRBby=
32 10 15 syl bBRSeBTrPredRBbB
33 32 adantr bBRSeByTrPredRBbTrPredRBbB
34 trpredtr bBRSeByTrPredRBbPredRByTrPredRBb
35 34 imp bBRSeByTrPredRBbPredRByTrPredRBb
36 sspred TrPredRBbBPredRByTrPredRBbPredRBy=PredRTrPredRBby
37 33 35 36 syl2anc bBRSeByTrPredRBbPredRBy=PredRTrPredRBby
38 37 eqeq1d bBRSeByTrPredRBbPredRBy=PredRTrPredRBby=
39 38 biimprd bBRSeByTrPredRBbPredRTrPredRBby=PredRBy=
40 39 reximdva bBRSeByTrPredRBbPredRTrPredRBby=yTrPredRBbPredRBy=
41 ssrexv TrPredRBbByTrPredRBbPredRBy=yBPredRBy=
42 32 40 41 sylsyld bBRSeByTrPredRBbPredRTrPredRBby=yBPredRBy=
43 31 42 sylan9r bBRSeBRFrBTrPredRBbBTrPredRBbyBPredRBy=
44 18 43 syld bBRSeBRFrBPredRBbyBPredRBy=
45 44 an31s RFrBRSeBbBPredRBbyBPredRBy=
46 9 45 pm2.61dne RFrBRSeBbByBPredRBy=
47 46 ex RFrBRSeBbByBPredRBy=
48 47 exlimdv RFrBRSeBbbByBPredRBy=
49 4 48 syl5bi RFrBRSeBByBPredRBy=
50 3 49 syl6com RFrARSeABAByBPredRBy=
51 50 imp32 RFrARSeABAByBPredRBy=