Metamath Proof Explorer


Theorem rtrclreclem1

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 φRV
Assertion rtrclreclem1 φRt*recR

Proof

Step Hyp Ref Expression
1 rtrclreclem1.1 φRV
2 1nn0 10
3 ssidd φRR
4 1 relexp1d φRr1=R
5 3 4 sseqtrrd φRRr1
6 oveq2 n=1Rrn=Rr1
7 6 sseq2d n=1RRrnRRr1
8 7 rspcev 10RRr1n0RRrn
9 2 5 8 sylancr φn0RRrn
10 ssiun n0RRrnRn0Rrn
11 9 10 syl φRn0Rrn
12 eqidd φrVn0rrn=rVn0rrn
13 oveq1 r=Rrrn=Rrn
14 13 iuneq2d r=Rn0rrn=n0Rrn
15 14 adantl φr=Rn0rrn=n0Rrn
16 1 elexd φRV
17 nn0ex 0V
18 ovex RrnV
19 17 18 iunex n0RrnV
20 19 a1i φn0RrnV
21 12 15 16 20 fvmptd φrVn0rrnR=n0Rrn
22 11 21 sseqtrrd φRrVn0rrnR
23 df-rtrclrec t*rec=rVn0rrn
24 fveq1 t*rec=rVn0rrnt*recR=rVn0rrnR
25 24 sseq2d t*rec=rVn0rrnRt*recRRrVn0rrnR
26 25 imbi2d t*rec=rVn0rrnφRt*recRφRrVn0rrnR
27 23 26 ax-mp φRt*recRφRrVn0rrnR
28 22 27 mpbir φRt*recR