Metamath Proof Explorer


Theorem rtrclreclem2

Description: The reflexive, transitive closure is indeed reflexive. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 13-Jul-2024)

Ref Expression
Hypotheses rtrclreclem2.1 φRelR
rtrclreclem2.2 φRV
Assertion rtrclreclem2 φIRt*recR

Proof

Step Hyp Ref Expression
1 rtrclreclem2.1 φRelR
2 rtrclreclem2.2 φRV
3 0nn0 00
4 ssid IRIR
5 1 2 relexp0d φRr0=IR
6 4 5 sseqtrrid φIRRr0
7 oveq2 n=0Rrn=Rr0
8 7 sseq2d n=0IRRrnIRRr0
9 8 rspcev 00IRRr0n0IRRrn
10 3 6 9 sylancr φn0IRRrn
11 ssiun n0IRRrnIRn0Rrn
12 10 11 syl φIRn0Rrn
13 2 elexd φRV
14 nn0ex 0V
15 ovex RrnV
16 14 15 iunex n0RrnV
17 oveq1 r=Rrrn=Rrn
18 17 iuneq2d r=Rn0rrn=n0Rrn
19 eqid rVn0rrn=rVn0rrn
20 18 19 fvmptg RVn0RrnVrVn0rrnR=n0Rrn
21 13 16 20 sylancl φrVn0rrnR=n0Rrn
22 12 21 sseqtrrd φIRrVn0rrnR
23 df-rtrclrec t*rec=rVn0rrn
24 fveq1 t*rec=rVn0rrnt*recR=rVn0rrnR
25 24 sseq2d t*rec=rVn0rrnIRt*recRIRrVn0rrnR
26 25 imbi2d t*rec=rVn0rrnφIRt*recRφIRrVn0rrnR
27 23 26 ax-mp φIRt*recRφIRrVn0rrnR
28 22 27 mpbir φIRt*recR