Metamath Proof Explorer


Theorem ssttrcl

Description: If R is a relation, then it is a subclass of its transitive closure. (Contributed by Scott Fenton, 17-Oct-2024)

Ref Expression
Assertion ssttrcl Could not format assertion : No typesetting found for |- ( Rel R -> R C_ t++ R ) with typecode |-

Proof

Step Hyp Ref Expression
1 1onn 1𝑜ω
2 1on 1𝑜On
3 2 onirri ¬1𝑜1𝑜
4 eldif 1𝑜ω1𝑜1𝑜ω¬1𝑜1𝑜
5 1 3 4 mpbir2an 1𝑜ω1𝑜
6 vex xV
7 vex yV
8 6 7 ifex ifm=xyV
9 eqid msuc1𝑜ifm=xy=msuc1𝑜ifm=xy
10 8 9 fnmpti msuc1𝑜ifm=xyFnsuc1𝑜
11 eqid x=x
12 eqid y=y
13 11 12 pm3.2i x=xy=y
14 1oex 1𝑜V
15 14 sucex suc1𝑜V
16 15 mptex msuc1𝑜ifm=xyV
17 fneq1 f=msuc1𝑜ifm=xyfFnsuc1𝑜msuc1𝑜ifm=xyFnsuc1𝑜
18 fveq1 f=msuc1𝑜ifm=xyf=msuc1𝑜ifm=xy
19 2 onordi Ord1𝑜
20 0elsuc Ord1𝑜suc1𝑜
21 19 20 ax-mp suc1𝑜
22 iftrue m=ifm=xy=x
23 22 9 6 fvmpt suc1𝑜msuc1𝑜ifm=xy=x
24 21 23 ax-mp msuc1𝑜ifm=xy=x
25 18 24 eqtrdi f=msuc1𝑜ifm=xyf=x
26 25 eqeq1d f=msuc1𝑜ifm=xyf=xx=x
27 fveq1 f=msuc1𝑜ifm=xyf1𝑜=msuc1𝑜ifm=xy1𝑜
28 14 sucid 1𝑜suc1𝑜
29 eqeq1 m=1𝑜m=1𝑜=
30 29 ifbid m=1𝑜ifm=xy=if1𝑜=xy
31 1n0 1𝑜
32 31 neii ¬1𝑜=
33 32 iffalsei if1𝑜=xy=y
34 33 7 eqeltri if1𝑜=xyV
35 30 9 34 fvmpt 1𝑜suc1𝑜msuc1𝑜ifm=xy1𝑜=if1𝑜=xy
36 28 35 ax-mp msuc1𝑜ifm=xy1𝑜=if1𝑜=xy
37 36 33 eqtri msuc1𝑜ifm=xy1𝑜=y
38 27 37 eqtrdi f=msuc1𝑜ifm=xyf1𝑜=y
39 38 eqeq1d f=msuc1𝑜ifm=xyf1𝑜=yy=y
40 26 39 anbi12d f=msuc1𝑜ifm=xyf=xf1𝑜=yx=xy=y
41 25 38 breq12d f=msuc1𝑜ifm=xyfRf1𝑜xRy
42 17 40 41 3anbi123d f=msuc1𝑜ifm=xyfFnsuc1𝑜f=xf1𝑜=yfRf1𝑜msuc1𝑜ifm=xyFnsuc1𝑜x=xy=yxRy
43 16 42 spcev msuc1𝑜ifm=xyFnsuc1𝑜x=xy=yxRyffFnsuc1𝑜f=xf1𝑜=yfRf1𝑜
44 10 13 43 mp3an12 xRyffFnsuc1𝑜f=xf1𝑜=yfRf1𝑜
45 suceq n=1𝑜sucn=suc1𝑜
46 45 fneq2d n=1𝑜fFnsucnfFnsuc1𝑜
47 fveqeq2 n=1𝑜fn=yf1𝑜=y
48 47 anbi2d n=1𝑜f=xfn=yf=xf1𝑜=y
49 raleq n=1𝑜mnfmRfsucmm1𝑜fmRfsucm
50 df1o2 1𝑜=
51 50 raleqi m1𝑜fmRfsucmmfmRfsucm
52 0ex V
53 fveq2 m=fm=f
54 suceq m=sucm=suc
55 df-1o 1𝑜=suc
56 54 55 eqtr4di m=sucm=1𝑜
57 56 fveq2d m=fsucm=f1𝑜
58 53 57 breq12d m=fmRfsucmfRf1𝑜
59 52 58 ralsn mfmRfsucmfRf1𝑜
60 51 59 bitri m1𝑜fmRfsucmfRf1𝑜
61 49 60 bitrdi n=1𝑜mnfmRfsucmfRf1𝑜
62 46 48 61 3anbi123d n=1𝑜fFnsucnf=xfn=ymnfmRfsucmfFnsuc1𝑜f=xf1𝑜=yfRf1𝑜
63 62 exbidv n=1𝑜ffFnsucnf=xfn=ymnfmRfsucmffFnsuc1𝑜f=xf1𝑜=yfRf1𝑜
64 63 rspcev 1𝑜ω1𝑜ffFnsuc1𝑜f=xf1𝑜=yfRf1𝑜nω1𝑜ffFnsucnf=xfn=ymnfmRfsucm
65 5 44 64 sylancr xRynω1𝑜ffFnsucnf=xfn=ymnfmRfsucm
66 df-br xRyxyR
67 brttrcl Could not format ( x t++ R y <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) ) : No typesetting found for |- ( x t++ R y <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) ) with typecode |-
68 df-br Could not format ( x t++ R y <-> <. x , y >. e. t++ R ) : No typesetting found for |- ( x t++ R y <-> <. x , y >. e. t++ R ) with typecode |-
69 67 68 bitr3i Could not format ( E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) <-> <. x , y >. e. t++ R ) : No typesetting found for |- ( E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) <-> <. x , y >. e. t++ R ) with typecode |-
70 65 66 69 3imtr3i Could not format ( <. x , y >. e. R -> <. x , y >. e. t++ R ) : No typesetting found for |- ( <. x , y >. e. R -> <. x , y >. e. t++ R ) with typecode |-
71 70 gen2 Could not format A. x A. y ( <. x , y >. e. R -> <. x , y >. e. t++ R ) : No typesetting found for |- A. x A. y ( <. x , y >. e. R -> <. x , y >. e. t++ R ) with typecode |-
72 ssrel Could not format ( Rel R -> ( R C_ t++ R <-> A. x A. y ( <. x , y >. e. R -> <. x , y >. e. t++ R ) ) ) : No typesetting found for |- ( Rel R -> ( R C_ t++ R <-> A. x A. y ( <. x , y >. e. R -> <. x , y >. e. t++ R ) ) ) with typecode |-
73 71 72 mpbiri Could not format ( Rel R -> R C_ t++ R ) : No typesetting found for |- ( Rel R -> R C_ t++ R ) with typecode |-