Metamath Proof Explorer


Theorem dfrtrclrec2

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 φRelR
Assertion dfrtrclrec2 φAt*recRBn0ARrnB

Proof

Step Hyp Ref Expression
1 dfrtrclrec2.1 φRelR
2 simpr φRVRV
3 nn0ex 0V
4 ovex RrnV
5 3 4 iunex n0RrnV
6 oveq1 r=Rrrn=Rrn
7 6 iuneq2d r=Rn0rrn=n0Rrn
8 eqid rVn0rrn=rVn0rrn
9 7 8 fvmptg RVn0RrnVrVn0rrnR=n0Rrn
10 2 5 9 sylancl φRVrVn0rrnR=n0Rrn
11 10 ex φRVrVn0rrnR=n0Rrn
12 iun0 n0=
13 12 a1i ¬RVn0=
14 reldmrelexp Reldomr
15 14 ovprc1 ¬RVRrn=
16 15 iuneq2d ¬RVn0Rrn=n0
17 fvprc ¬RVrVn0rrnR=
18 13 16 17 3eqtr4rd ¬RVrVn0rrnR=n0Rrn
19 11 18 pm2.61d1 φrVn0rrnR=n0Rrn
20 breq rVn0rrnR=n0RrnArVn0rrnRBAn0RrnB
21 eliun ABn0Rrnn0ABRrn
22 21 a1i φABn0Rrnn0ABRrn
23 df-br An0RrnBABn0Rrn
24 df-br ARrnBABRrn
25 24 rexbii n0ARrnBn0ABRrn
26 22 23 25 3bitr4g φAn0RrnBn0ARrnB
27 20 26 sylan9bb rVn0rrnR=n0RrnφArVn0rrnRBn0ARrnB
28 19 27 mpancom φArVn0rrnRBn0ARrnB
29 df-rtrclrec t*rec=rVn0rrn
30 fveq1 t*rec=rVn0rrnt*recR=rVn0rrnR
31 30 breqd t*rec=rVn0rrnAt*recRBArVn0rrnRB
32 31 bibi1d t*rec=rVn0rrnAt*recRBn0ARrnBArVn0rrnRBn0ARrnB
33 32 imbi2d t*rec=rVn0rrnφAt*recRBn0ARrnBφArVn0rrnRBn0ARrnB
34 29 33 ax-mp φAt*recRBn0ARrnBφArVn0rrnRBn0ARrnB
35 28 34 mpbir φAt*recRBn0ARrnB