Description: If two elements are connected by a reflexive, transitive closure, then they are connected via n instances the relation, for some n . (Contributed by Drahflow, 12-Nov-2015) (Revised by AV, 13-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | dfrtrclrec2.1 | |
|
Assertion | dfrtrclrec2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfrtrclrec2.1 | |
|
2 | simpr | |
|
3 | nn0ex | |
|
4 | ovex | |
|
5 | 3 4 | iunex | |
6 | oveq1 | |
|
7 | 6 | iuneq2d | |
8 | eqid | |
|
9 | 7 8 | fvmptg | |
10 | 2 5 9 | sylancl | |
11 | 10 | ex | |
12 | iun0 | |
|
13 | 12 | a1i | |
14 | reldmrelexp | |
|
15 | 14 | ovprc1 | |
16 | 15 | iuneq2d | |
17 | fvprc | |
|
18 | 13 16 17 | 3eqtr4rd | |
19 | 11 18 | pm2.61d1 | |
20 | breq | |
|
21 | eliun | |
|
22 | 21 | a1i | |
23 | df-br | |
|
24 | df-br | |
|
25 | 24 | rexbii | |
26 | 22 23 25 | 3bitr4g | |
27 | 20 26 | sylan9bb | |
28 | 19 27 | mpancom | |
29 | df-rtrclrec | |
|
30 | fveq1 | |
|
31 | 30 | breqd | |
32 | 31 | bibi1d | |
33 | 32 | imbi2d | |
34 | 29 33 | ax-mp | |
35 | 28 34 | mpbir | |