Metamath Proof Explorer

Theorem dmttrcl

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

Ref Expression
Assertion dmttrcl 
|- dom t++ R = dom 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 dmeqi 
 |-  dom t++ R = dom { <. 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 dmopab 
 |-  dom { <. 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 ) ) } = { x | E. 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 ) ) }
4 2 3 eqtri 
 |-  dom t++ R = { x | E. 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 ) ) }
5 simpr2l 
 |-  ( ( n e. ( _om \ 1o ) /\ ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) -> ( f ` (/) ) = x )
6 fveq2 
 |-  ( a = (/) -> ( f ` a ) = ( f ` (/) ) )
7 suceq 
 |-  ( a = (/) -> suc a = suc (/) )
8 df-1o 
 |-  1o = suc (/)
9 7 8 eqtr4di 
 |-  ( a = (/) -> suc a = 1o )
10 9 fveq2d 
 |-  ( a = (/) -> ( f ` suc a ) = ( f ` 1o ) )
11 6 10 breq12d 
 |-  ( a = (/) -> ( ( f ` a ) R ( f ` suc a ) <-> ( f ` (/) ) R ( f ` 1o ) ) )
12 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 ) )
13 eldif 
 |-  ( n e. ( _om \ 1o ) <-> ( n e. _om /\ -. n e. 1o ) )
14 0ex 
 |-  (/) e. _V
15 nnord 
 |-  ( n e. _om -> Ord n )
16 ordelsuc 
 |-  ( ( (/) e. _V /\ Ord n ) -> ( (/) e. n <-> suc (/) C_ n ) )
17 14 15 16 sylancr 
 |-  ( n e. _om -> ( (/) e. n <-> suc (/) C_ n ) )
18 8 sseq1i 
 |-  ( 1o C_ n <-> suc (/) C_ n )
19 1on 
 |-  1o e. On
20 19 onordi 
 |-  Ord 1o
21 ordtri1 
 |-  ( ( Ord 1o /\ Ord n ) -> ( 1o C_ n <-> -. n e. 1o ) )
22 20 15 21 sylancr 
 |-  ( n e. _om -> ( 1o C_ n <-> -. n e. 1o ) )
23 18 22 bitr3id 
 |-  ( n e. _om -> ( suc (/) C_ n <-> -. n e. 1o ) )
24 17 23 bitr2d 
 |-  ( n e. _om -> ( -. n e. 1o <-> (/) e. n ) )
25 24 biimpa 
 |-  ( ( n e. _om /\ -. n e. 1o ) -> (/) e. n )
26 13 25 sylbi 
 |-  ( n e. ( _om \ 1o ) -> (/) e. n )
27 26 adantr 
 |-  ( ( n e. ( _om \ 1o ) /\ ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) -> (/) e. n )
28 11 12 27 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 ` (/) ) R ( f ` 1o ) )
29 5 28 eqbrtrrd 
 |-  ( ( n e. ( _om \ 1o ) /\ ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) -> x R ( f ` 1o ) )
30 vex 
 |-  x e. _V
31 fvex 
 |-  ( f ` 1o ) e. _V
32 30 31 breldm 
 |-  ( x R ( f ` 1o ) -> x e. dom R )
33 29 32 syl 
 |-  ( ( n e. ( _om \ 1o ) /\ ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) -> x e. dom R )
34 33 ex 
 |-  ( n e. ( _om \ 1o ) -> ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) -> x e. dom R ) )
35 34 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 ) ) -> x e. dom R ) )
36 35 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 ) ) -> x e. dom R )
37 36 exlimiv 
 |-  ( E. 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 ) ) -> x e. dom R )
38 37 abssi 
 |-  { x | E. 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 ) ) } C_ dom R
39 4 38 eqsstri 
 |-  dom t++ R C_ dom R
40 dmresv 
 |-  dom ( R |` _V ) = dom R
41 relres 
 |-  Rel ( R |` _V )
42 ssttrcl 
 |-  ( Rel ( R |` _V ) -> ( R |` _V ) C_ t++ ( R |` _V ) )
43 41 42 ax-mp 
 |-  ( R |` _V ) C_ t++ ( R |` _V )
44 ttrclresv 
 |-  t++ ( R |` _V ) = t++ R
45 43 44 sseqtri 
 |-  ( R |` _V ) C_ t++ R
46 dmss 
 |-  ( ( R |` _V ) C_ t++ R -> dom ( R |` _V ) C_ dom t++ R )
47 45 46 ax-mp 
 |-  dom ( R |` _V ) C_ dom t++ R
48 40 47 eqsstrri 
 |-  dom R C_ dom t++ R
49 39 48 eqssi 
 |-  dom t++ R = dom R