Metamath Proof Explorer

Theorem rnttrcl

Description: The range of a transitive closure is the same as the range of the original class. (Contributed by Scott Fenton, 26-Oct-2024)

Ref Expression
Assertion rnttrcl 
|- ran t++ R = ran R

Proof

Step Hyp Ref Expression
1 df-ttrcl 
 |-  t++ R = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) }
2 1 rneqi 
 |-  ran t++ R = ran { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) }
3 rnopab 
 |-  ran { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) } = { y | E. x E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) }
4 2 3 eqtri 
 |-  ran t++ R = { y | E. x E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) }
5 fveq2 
 |-  ( a = U. n -> ( f ` a ) = ( f ` U. n ) )
6 suceq 
 |-  ( a = U. n -> suc a = suc U. n )
7 6 fveq2d 
 |-  ( a = U. n -> ( f ` suc a ) = ( f ` suc U. n ) )
8 5 7 breq12d 
 |-  ( a = U. n -> ( ( f ` a ) R ( f ` suc a ) <-> ( f ` U. n ) R ( f ` suc U. n ) ) )
9 simpr3 
 |-  ( ( n e. ( _om \ 1o ) /\ ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) -> A. a e. n ( f ` a ) R ( f ` suc a ) )
10 df-1o 
 |-  1o = suc (/)
11 10 difeq2i 
 |-  ( _om \ 1o ) = ( _om \ suc (/) )
12 11 eleq2i 
 |-  ( n e. ( _om \ 1o ) <-> n e. ( _om \ suc (/) ) )
13 peano1 
 |-  (/) e. _om
14 eldifsucnn 
 |-  ( (/) e. _om -> ( n e. ( _om \ suc (/) ) <-> E. x e. ( _om \ (/) ) n = suc x ) )
15 13 14 ax-mp 
 |-  ( n e. ( _om \ suc (/) ) <-> E. x e. ( _om \ (/) ) n = suc x )
16 dif0 
 |-  ( _om \ (/) ) = _om
17 16 rexeqi 
 |-  ( E. x e. ( _om \ (/) ) n = suc x <-> E. x e. _om n = suc x )
18 12 15 17 3bitri 
 |-  ( n e. ( _om \ 1o ) <-> E. x e. _om n = suc x )
19 nnord 
 |-  ( x e. _om -> Ord x )
20 ordunisuc 
 |-  ( Ord x -> U. suc x = x )
21 19 20 syl 
 |-  ( x e. _om -> U. suc x = x )
22 vex 
 |-  x e. _V
23 22 sucid 
 |-  x e. suc x
24 21 23 eqeltrdi 
 |-  ( x e. _om -> U. suc x e. suc x )
25 unieq 
 |-  ( n = suc x -> U. n = U. suc x )
26 id 
 |-  ( n = suc x -> n = suc x )
27 25 26 eleq12d 
 |-  ( n = suc x -> ( U. n e. n <-> U. suc x e. suc x ) )
28 24 27 syl5ibrcom 
 |-  ( x e. _om -> ( n = suc x -> U. n e. n ) )
29 28 rexlimiv 
 |-  ( E. x e. _om n = suc x -> U. n e. n )
30 18 29 sylbi 
 |-  ( n e. ( _om \ 1o ) -> U. n e. n )
31 30 adantr 
 |-  ( ( n e. ( _om \ 1o ) /\ ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) -> U. n e. n )
32 8 9 31 rspcdva 
 |-  ( ( n e. ( _om \ 1o ) /\ ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) -> ( f ` U. n ) R ( f ` suc U. n ) )
33 suceq 
 |-  ( U. suc x = x -> suc U. suc x = suc x )
34 21 33 syl 
 |-  ( x e. _om -> suc U. suc x = suc x )
35 suceq 
 |-  ( U. n = U. suc x -> suc U. n = suc U. suc x )
36 25 35 syl 
 |-  ( n = suc x -> suc U. n = suc U. suc x )
37 36 26 eqeq12d 
 |-  ( n = suc x -> ( suc U. n = n <-> suc U. suc x = suc x ) )
38 34 37 syl5ibrcom 
 |-  ( x e. _om -> ( n = suc x -> suc U. n = n ) )
39 38 rexlimiv 
 |-  ( E. x e. _om n = suc x -> suc U. n = n )
40 18 39 sylbi 
 |-  ( n e. ( _om \ 1o ) -> suc U. n = n )
41 40 fveq2d 
 |-  ( n e. ( _om \ 1o ) -> ( f ` suc U. n ) = ( f ` n ) )
42 41 adantr 
 |-  ( ( n e. ( _om \ 1o ) /\ ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) -> ( f ` suc U. n ) = ( f ` n ) )
43 simpr2r 
 |-  ( ( n e. ( _om \ 1o ) /\ ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) -> ( f ` n ) = y )
44 42 43 eqtrd 
 |-  ( ( n e. ( _om \ 1o ) /\ ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) -> ( f ` suc U. n ) = y )
45 32 44 breqtrd 
 |-  ( ( n e. ( _om \ 1o ) /\ ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) -> ( f ` U. n ) R y )
46 fvex 
 |-  ( f ` U. n ) e. _V
47 vex 
 |-  y e. _V
48 46 47 brelrn 
 |-  ( ( f ` U. n ) R y -> y e. ran R )
49 45 48 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) -> y e. ran R )
50 49 ex 
 |-  ( n e. ( _om \ 1o ) -> ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) -> y e. ran R ) )
51 50 exlimdv 
 |-  ( n e. ( _om \ 1o ) -> ( E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) -> y e. ran R ) )
52 51 rexlimiv 
 |-  ( E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) -> y e. ran R )
53 52 exlimiv 
 |-  ( E. x E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) -> y e. ran R )
54 53 abssi 
 |-  { y | E. x E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) } C_ ran R
55 4 54 eqsstri 
 |-  ran t++ R C_ ran R
56 rnresv 
 |-  ran ( R |` _V ) = ran R
57 relres 
 |-  Rel ( R |` _V )
58 ssttrcl 
 |-  ( Rel ( R |` _V ) -> ( R |` _V ) C_ t++ ( R |` _V ) )
59 57 58 ax-mp 
 |-  ( R |` _V ) C_ t++ ( R |` _V )
60 ttrclresv 
 |-  t++ ( R |` _V ) = t++ R
61 59 60 sseqtri 
 |-  ( R |` _V ) C_ t++ R
62 61 rnssi 
 |-  ran ( R |` _V ) C_ ran t++ R
63 56 62 eqsstrri 
 |-  ran R C_ ran t++ R
64 55 63 eqssi 
 |-  ran t++ R = ran R