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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frss | |
|
2 | sess2 | |
|
3 | 1 2 | anim12d | |
4 | n0 | |
|
5 | predeq3 | |
|
6 | 5 | eqeq1d | |
7 | 6 | rspcev | |
8 | 7 | ex | |
9 | 8 | adantl | |
10 | setlikespec | |
|
11 | trpredpred | |
|
12 | ssn0 | |
|
13 | 12 | ex | |
14 | 11 13 | syl | |
15 | trpredss | |
|
16 | 14 15 | jctild | |
17 | 10 16 | syl | |
18 | 17 | adantr | |
19 | trpredex | |
|
20 | sseq1 | |
|
21 | neeq1 | |
|
22 | 20 21 | anbi12d | |
23 | predeq2 | |
|
24 | 23 | eqeq1d | |
25 | 24 | rexeqbi1dv | |
26 | 22 25 | imbi12d | |
27 | 26 | imbi2d | |
28 | dffr4 | |
|
29 | sp | |
|
30 | 28 29 | sylbi | |
31 | 19 27 30 | vtocl | |
32 | 10 15 | syl | |
33 | 32 | adantr | |
34 | trpredtr | |
|
35 | 34 | imp | |
36 | sspred | |
|
37 | 33 35 36 | syl2anc | |
38 | 37 | eqeq1d | |
39 | 38 | biimprd | |
40 | 39 | reximdva | |
41 | ssrexv | |
|
42 | 32 40 41 | sylsyld | |
43 | 31 42 | sylan9r | |
44 | 18 43 | syld | |
45 | 44 | an31s | |
46 | 9 45 | pm2.61dne | |
47 | 46 | ex | |
48 | 47 | exlimdv | |
49 | 4 48 | syl5bi | |
50 | 3 49 | syl6com | |
51 | 50 | imp32 | |