Description: If R is set-like over A , then the transitive closure of the restriction of R to A is set-like over A .
This theorem requires the axioms of infinity and replacement for its proof. (Contributed by Scott Fenton, 31-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ttrclse | |- ( R Se A -> t++ ( R |` A ) Se A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brttrcl2 | |- ( y t++ ( R |` A ) x <-> E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc n ) = x ) /\ A. a e. suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) |
|
| 2 | eqid | |- rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) = rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) |
|
| 3 | 2 | ttrclselem2 | |- ( ( n e. _om /\ R Se A /\ x e. A ) -> ( E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc n ) = x ) /\ A. a e. suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) ` n ) ) ) |
| 4 | 3 | 3expb | |- ( ( n e. _om /\ ( R Se A /\ x e. A ) ) -> ( E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc n ) = x ) /\ A. a e. suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) ` n ) ) ) |
| 5 | 4 | ancoms | |- ( ( ( R Se A /\ x e. A ) /\ n e. _om ) -> ( E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc n ) = x ) /\ A. a e. suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) ` n ) ) ) |
| 6 | 5 | rexbidva | |- ( ( R Se A /\ x e. A ) -> ( E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc n ) = x ) /\ A. a e. suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. n e. _om y e. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) ` n ) ) ) |
| 7 | 1 6 | syl5bb | |- ( ( R Se A /\ x e. A ) -> ( y t++ ( R |` A ) x <-> E. n e. _om y e. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) ` n ) ) ) |
| 8 | vex | |- y e. _V |
|
| 9 | 8 | elpred | |- ( x e. _V -> ( y e. Pred ( t++ ( R |` A ) , A , x ) <-> ( y e. A /\ y t++ ( R |` A ) x ) ) ) |
| 10 | 9 | elv | |- ( y e. Pred ( t++ ( R |` A ) , A , x ) <-> ( y e. A /\ y t++ ( R |` A ) x ) ) |
| 11 | resdmss | |- dom ( R |` A ) C_ A |
|
| 12 | vex | |- x e. _V |
|
| 13 | 8 12 | breldm | |- ( y t++ ( R |` A ) x -> y e. dom t++ ( R |` A ) ) |
| 14 | dmttrcl | |- dom t++ ( R |` A ) = dom ( R |` A ) |
|
| 15 | 13 14 | eleqtrdi | |- ( y t++ ( R |` A ) x -> y e. dom ( R |` A ) ) |
| 16 | 11 15 | sselid | |- ( y t++ ( R |` A ) x -> y e. A ) |
| 17 | 16 | pm4.71ri | |- ( y t++ ( R |` A ) x <-> ( y e. A /\ y t++ ( R |` A ) x ) ) |
| 18 | 10 17 | bitr4i | |- ( y e. Pred ( t++ ( R |` A ) , A , x ) <-> y t++ ( R |` A ) x ) |
| 19 | rdgfun | |- Fun rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) |
|
| 20 | eluniima | |- ( Fun rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) -> ( y e. U. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) " _om ) <-> E. n e. _om y e. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) ` n ) ) ) |
|
| 21 | 19 20 | ax-mp | |- ( y e. U. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) " _om ) <-> E. n e. _om y e. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) ` n ) ) |
| 22 | 7 18 21 | 3bitr4g | |- ( ( R Se A /\ x e. A ) -> ( y e. Pred ( t++ ( R |` A ) , A , x ) <-> y e. U. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) " _om ) ) ) |
| 23 | 22 | eqrdv | |- ( ( R Se A /\ x e. A ) -> Pred ( t++ ( R |` A ) , A , x ) = U. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) " _om ) ) |
| 24 | omex | |- _om e. _V |
|
| 25 | 24 | funimaex | |- ( Fun rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) -> ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) " _om ) e. _V ) |
| 26 | 19 25 | ax-mp | |- ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) " _om ) e. _V |
| 27 | 26 | uniex | |- U. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) " _om ) e. _V |
| 28 | 23 27 | eqeltrdi | |- ( ( R Se A /\ x e. A ) -> Pred ( t++ ( R |` A ) , A , x ) e. _V ) |
| 29 | 28 | ralrimiva | |- ( R Se A -> A. x e. A Pred ( t++ ( R |` A ) , A , x ) e. _V ) |
| 30 | dfse3 | |- ( t++ ( R |` A ) Se A <-> A. x e. A Pred ( t++ ( R |` A ) , A , x ) e. _V ) |
|
| 31 | 29 30 | sylibr | |- ( R Se A -> t++ ( R |` A ) Se A ) |