Metamath Proof Explorer

Theorem ttrclselem1

Description: Lemma for ttrclse . Show that all finite ordinal function values of F are subsets of A . (Contributed by Scott Fenton, 31-Oct-2024)

Ref Expression
Hypothesis ttrclselem.1 
|- F = rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) )
Assertion ttrclselem1 
|- ( N e. _om -> ( F ` N ) C_ A )

Proof

Step Hyp Ref Expression
1 ttrclselem.1 
 |-  F = rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) )
2 nn0suc 
 |-  ( N e. _om -> ( N = (/) \/ E. n e. _om N = suc n ) )
3 1 fveq1i 
 |-  ( F ` N ) = ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) ) ` N )
4 fveq2 
 |-  ( N = (/) -> ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) ) ` N ) = ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) ) ` (/) ) )
5 3 4 eqtrid 
 |-  ( N = (/) -> ( F ` N ) = ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) ) ` (/) ) )
6 rdg0g 
 |-  ( Pred ( R , A , X ) e. _V -> ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) ) ` (/) ) = Pred ( R , A , X ) )
7 predss 
 |-  Pred ( R , A , X ) C_ A
8 6 7 eqsstrdi 
 |-  ( Pred ( R , A , X ) e. _V -> ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) ) ` (/) ) C_ A )
9 rdg0n 
 |-  ( -. Pred ( R , A , X ) e. _V -> ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) ) ` (/) ) = (/) )
10 0ss 
 |-  (/) C_ A
11 9 10 eqsstrdi 
 |-  ( -. Pred ( R , A , X ) e. _V -> ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) ) ` (/) ) C_ A )
12 8 11 pm2.61i 
 |-  ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) ) ` (/) ) C_ A
13 5 12 eqsstrdi 
 |-  ( N = (/) -> ( F ` N ) C_ A )
14 nnon 
 |-  ( n e. _om -> n e. On )
15 nfcv 
 |-  F/_ b Pred ( R , A , X )
16 nfcv 
 |-  F/_ b n
17 nfmpt1 
 |-  F/_ b ( b e. _V |-> U_ w e. b Pred ( R , A , w ) )
18 17 15 nfrdg 
 |-  F/_ b rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) )
19 1 18 nfcxfr 
 |-  F/_ b F
20 19 16 nffv 
 |-  F/_ b ( F ` n )
21 nfcv 
 |-  F/_ b Pred ( R , A , t )
22 20 21 nfiun 
 |-  F/_ b U_ t e. ( F ` n ) Pred ( R , A , t )
23 predeq3 
 |-  ( w = t -> Pred ( R , A , w ) = Pred ( R , A , t ) )
24 23 cbviunv 
 |-  U_ w e. b Pred ( R , A , w ) = U_ t e. b Pred ( R , A , t )
25 iuneq1 
 |-  ( b = ( F ` n ) -> U_ t e. b Pred ( R , A , t ) = U_ t e. ( F ` n ) Pred ( R , A , t ) )
26 24 25 eqtrid 
 |-  ( b = ( F ` n ) -> U_ w e. b Pred ( R , A , w ) = U_ t e. ( F ` n ) Pred ( R , A , t ) )
27 15 16 22 1 26 rdgsucmptf 
 |-  ( ( n e. On /\ U_ t e. ( F ` n ) Pred ( R , A , t ) e. _V ) -> ( F ` suc n ) = U_ t e. ( F ` n ) Pred ( R , A , t ) )
28 iunss 
 |-  ( U_ t e. ( F ` n ) Pred ( R , A , t ) C_ A <-> A. t e. ( F ` n ) Pred ( R , A , t ) C_ A )
29 predss 
 |-  Pred ( R , A , t ) C_ A
30 29 a1i 
 |-  ( t e. ( F ` n ) -> Pred ( R , A , t ) C_ A )
31 28 30 mprgbir 
 |-  U_ t e. ( F ` n ) Pred ( R , A , t ) C_ A
32 27 31 eqsstrdi 
 |-  ( ( n e. On /\ U_ t e. ( F ` n ) Pred ( R , A , t ) e. _V ) -> ( F ` suc n ) C_ A )
33 14 32 sylan 
 |-  ( ( n e. _om /\ U_ t e. ( F ` n ) Pred ( R , A , t ) e. _V ) -> ( F ` suc n ) C_ A )
34 15 16 22 1 26 rdgsucmptnf 
 |-  ( -. U_ t e. ( F ` n ) Pred ( R , A , t ) e. _V -> ( F ` suc n ) = (/) )
35 34 10 eqsstrdi 
 |-  ( -. U_ t e. ( F ` n ) Pred ( R , A , t ) e. _V -> ( F ` suc n ) C_ A )
36 35 adantl 
 |-  ( ( n e. _om /\ -. U_ t e. ( F ` n ) Pred ( R , A , t ) e. _V ) -> ( F ` suc n ) C_ A )
37 33 36 pm2.61dan 
 |-  ( n e. _om -> ( F ` suc n ) C_ A )
38 fveq2 
 |-  ( N = suc n -> ( F ` N ) = ( F ` suc n ) )
39 38 sseq1d 
 |-  ( N = suc n -> ( ( F ` N ) C_ A <-> ( F ` suc n ) C_ A ) )
40 37 39 syl5ibrcom 
 |-  ( n e. _om -> ( N = suc n -> ( F ` N ) C_ A ) )
41 40 rexlimiv 
 |-  ( E. n e. _om N = suc n -> ( F ` N ) C_ A )
42 13 41 jaoi 
 |-  ( ( N = (/) \/ E. n e. _om N = suc n ) -> ( F ` N ) C_ A )
43 2 42 syl 
 |-  ( N e. _om -> ( F ` N ) C_ A )