Description: The reflexive, transitive closure is indeed a closure. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | rtrclreclem1.1 | |
|
Assertion | rtrclreclem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rtrclreclem1.1 | |
|
2 | 1nn0 | |
|
3 | ssidd | |
|
4 | 1 | relexp1d | |
5 | 3 4 | sseqtrrd | |
6 | oveq2 | |
|
7 | 6 | sseq2d | |
8 | 7 | rspcev | |
9 | 2 5 8 | sylancr | |
10 | ssiun | |
|
11 | 9 10 | syl | |
12 | eqidd | |
|
13 | oveq1 | |
|
14 | 13 | iuneq2d | |
15 | 14 | adantl | |
16 | 1 | elexd | |
17 | nn0ex | |
|
18 | ovex | |
|
19 | 17 18 | iunex | |
20 | 19 | a1i | |
21 | 12 15 16 20 | fvmptd | |
22 | 11 21 | sseqtrrd | |
23 | df-rtrclrec | |
|
24 | fveq1 | |
|
25 | 24 | sseq2d | |
26 | 25 | imbi2d | |
27 | 23 26 | ax-mp | |
28 | 22 27 | mpbir | |