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 
|- ( Rel R -> R C_ t++ R )

Proof

Step Hyp Ref Expression
1 1onn 
 |-  1o e. _om
2 1on 
 |-  1o e. On
3 2 onirri 
 |-  -. 1o e. 1o
4 eldif 
 |-  ( 1o e. ( _om \ 1o ) <-> ( 1o e. _om /\ -. 1o e. 1o ) )
5 1 3 4 mpbir2an 
 |-  1o e. ( _om \ 1o )
6 vex 
 |-  x e. _V
7 vex 
 |-  y e. _V
8 6 7 ifex 
 |-  if ( m = (/) , x , y ) e. _V
9 eqid 
 |-  ( m e. suc 1o |-> if ( m = (/) , x , y ) ) = ( m e. suc 1o |-> if ( m = (/) , x , y ) )
10 8 9 fnmpti 
 |-  ( m e. suc 1o |-> if ( m = (/) , x , y ) ) Fn suc 1o
11 eqid 
 |-  x = x
12 eqid 
 |-  y = y
13 11 12 pm3.2i 
 |-  ( x = x /\ y = y )
14 1oex 
 |-  1o e. _V
15 14 sucex 
 |-  suc 1o e. _V
16 15 mptex 
 |-  ( m e. suc 1o |-> if ( m = (/) , x , y ) ) e. _V
17 fneq1 
 |-  ( f = ( m e. suc 1o |-> if ( m = (/) , x , y ) ) -> ( f Fn suc 1o <-> ( m e. suc 1o |-> if ( m = (/) , x , y ) ) Fn suc 1o ) )
18 fveq1 
 |-  ( f = ( m e. suc 1o |-> if ( m = (/) , x , y ) ) -> ( f ` (/) ) = ( ( m e. suc 1o |-> if ( m = (/) , x , y ) ) ` (/) ) )
19 2 onordi 
 |-  Ord 1o
20 0elsuc 
 |-  ( Ord 1o -> (/) e. suc 1o )
21 19 20 ax-mp 
 |-  (/) e. suc 1o
22 iftrue 
 |-  ( m = (/) -> if ( m = (/) , x , y ) = x )
23 22 9 6 fvmpt 
 |-  ( (/) e. suc 1o -> ( ( m e. suc 1o |-> if ( m = (/) , x , y ) ) ` (/) ) = x )
24 21 23 ax-mp 
 |-  ( ( m e. suc 1o |-> if ( m = (/) , x , y ) ) ` (/) ) = x
25 18 24 eqtrdi 
 |-  ( f = ( m e. suc 1o |-> if ( m = (/) , x , y ) ) -> ( f ` (/) ) = x )
26 25 eqeq1d 
 |-  ( f = ( m e. suc 1o |-> if ( m = (/) , x , y ) ) -> ( ( f ` (/) ) = x <-> x = x ) )
27 fveq1 
 |-  ( f = ( m e. suc 1o |-> if ( m = (/) , x , y ) ) -> ( f ` 1o ) = ( ( m e. suc 1o |-> if ( m = (/) , x , y ) ) ` 1o ) )
28 14 sucid 
 |-  1o e. suc 1o
29 eqeq1 
 |-  ( m = 1o -> ( m = (/) <-> 1o = (/) ) )
30 29 ifbid 
 |-  ( m = 1o -> if ( m = (/) , x , y ) = if ( 1o = (/) , x , y ) )
31 1n0 
 |-  1o =/= (/)
32 31 neii 
 |-  -. 1o = (/)
33 32 iffalsei 
 |-  if ( 1o = (/) , x , y ) = y
34 33 7 eqeltri 
 |-  if ( 1o = (/) , x , y ) e. _V
35 30 9 34 fvmpt 
 |-  ( 1o e. suc 1o -> ( ( m e. suc 1o |-> if ( m = (/) , x , y ) ) ` 1o ) = if ( 1o = (/) , x , y ) )
36 28 35 ax-mp 
 |-  ( ( m e. suc 1o |-> if ( m = (/) , x , y ) ) ` 1o ) = if ( 1o = (/) , x , y )
37 36 33 eqtri 
 |-  ( ( m e. suc 1o |-> if ( m = (/) , x , y ) ) ` 1o ) = y
38 27 37 eqtrdi 
 |-  ( f = ( m e. suc 1o |-> if ( m = (/) , x , y ) ) -> ( f ` 1o ) = y )
39 38 eqeq1d 
 |-  ( f = ( m e. suc 1o |-> if ( m = (/) , x , y ) ) -> ( ( f ` 1o ) = y <-> y = y ) )
40 26 39 anbi12d 
 |-  ( f = ( m e. suc 1o |-> if ( m = (/) , x , y ) ) -> ( ( ( f ` (/) ) = x /\ ( f ` 1o ) = y ) <-> ( x = x /\ y = y ) ) )
41 25 38 breq12d 
 |-  ( f = ( m e. suc 1o |-> if ( m = (/) , x , y ) ) -> ( ( f ` (/) ) R ( f ` 1o ) <-> x R y ) )
42 17 40 41 3anbi123d 
 |-  ( f = ( m e. suc 1o |-> if ( m = (/) , x , y ) ) -> ( ( f Fn suc 1o /\ ( ( f ` (/) ) = x /\ ( f ` 1o ) = y ) /\ ( f ` (/) ) R ( f ` 1o ) ) <-> ( ( m e. suc 1o |-> if ( m = (/) , x , y ) ) Fn suc 1o /\ ( x = x /\ y = y ) /\ x R y ) ) )
43 16 42 spcev 
 |-  ( ( ( m e. suc 1o |-> if ( m = (/) , x , y ) ) Fn suc 1o /\ ( x = x /\ y = y ) /\ x R y ) -> E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = x /\ ( f ` 1o ) = y ) /\ ( f ` (/) ) R ( f ` 1o ) ) )
44 10 13 43 mp3an12 
 |-  ( x R y -> E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = x /\ ( f ` 1o ) = y ) /\ ( f ` (/) ) R ( f ` 1o ) ) )
45 suceq 
 |-  ( n = 1o -> suc n = suc 1o )
46 45 fneq2d 
 |-  ( n = 1o -> ( f Fn suc n <-> f Fn suc 1o ) )
47 fveqeq2 
 |-  ( n = 1o -> ( ( f ` n ) = y <-> ( f ` 1o ) = y ) )
48 47 anbi2d 
 |-  ( n = 1o -> ( ( ( f ` (/) ) = x /\ ( f ` n ) = y ) <-> ( ( f ` (/) ) = x /\ ( f ` 1o ) = y ) ) )
49 raleq 
 |-  ( n = 1o -> ( A. m e. n ( f ` m ) R ( f ` suc m ) <-> A. m e. 1o ( f ` m ) R ( f ` suc m ) ) )
50 df1o2 
 |-  1o = { (/) }
51 50 raleqi 
 |-  ( A. m e. 1o ( f ` m ) R ( f ` suc m ) <-> A. m e. { (/) } ( f ` m ) R ( f ` suc m ) )
52 0ex 
 |-  (/) e. _V
53 fveq2 
 |-  ( m = (/) -> ( f ` m ) = ( f ` (/) ) )
54 suceq 
 |-  ( m = (/) -> suc m = suc (/) )
55 df-1o 
 |-  1o = suc (/)
56 54 55 eqtr4di 
 |-  ( m = (/) -> suc m = 1o )
57 56 fveq2d 
 |-  ( m = (/) -> ( f ` suc m ) = ( f ` 1o ) )
58 53 57 breq12d 
 |-  ( m = (/) -> ( ( f ` m ) R ( f ` suc m ) <-> ( f ` (/) ) R ( f ` 1o ) ) )
59 52 58 ralsn 
 |-  ( A. m e. { (/) } ( f ` m ) R ( f ` suc m ) <-> ( f ` (/) ) R ( f ` 1o ) )
60 51 59 bitri 
 |-  ( A. m e. 1o ( f ` m ) R ( f ` suc m ) <-> ( f ` (/) ) R ( f ` 1o ) )
61 49 60 bitrdi 
 |-  ( n = 1o -> ( A. m e. n ( f ` m ) R ( f ` suc m ) <-> ( f ` (/) ) R ( f ` 1o ) ) )
62 46 48 61 3anbi123d 
 |-  ( n = 1o -> ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) <-> ( f Fn suc 1o /\ ( ( f ` (/) ) = x /\ ( f ` 1o ) = y ) /\ ( f ` (/) ) R ( f ` 1o ) ) ) )
63 62 exbidv 
 |-  ( n = 1o -> ( E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) <-> E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = x /\ ( f ` 1o ) = y ) /\ ( f ` (/) ) R ( f ` 1o ) ) ) )
64 63 rspcev 
 |-  ( ( 1o e. ( _om \ 1o ) /\ E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = x /\ ( f ` 1o ) = y ) /\ ( f ` (/) ) R ( f ` 1o ) ) ) -> 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 ) ) )
65 5 44 64 sylancr 
 |-  ( x 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 ) ) )
66 df-br 
 |-  ( x R y <-> <. x , y >. e. R )
67 brttrcl 
 |-  ( 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 ) ) )
68 df-br 
 |-  ( x t++ R y <-> <. x , y >. e. t++ R )
69 67 68 bitr3i 
 |-  ( 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 )
70 65 66 69 3imtr3i 
 |-  ( <. x , y >. e. R -> <. x , y >. e. t++ R )
71 70 gen2 
 |-  A. x A. y ( <. x , y >. e. R -> <. x , y >. e. t++ R )
72 ssrel 
 |-  ( Rel R -> ( R C_ t++ R <-> A. x A. y ( <. x , y >. e. R -> <. x , y >. e. t++ R ) ) )
73 71 72 mpbiri 
 |-  ( Rel R -> R C_ t++ R )