Metamath Proof Explorer


Theorem rdgssun

Description: In a recursive definition where each step expands on the previous one using a union, every previous step is a subset of every later step. (Contributed by ML, 1-Apr-2022)

Ref Expression
Hypotheses rdgssun.1
|- F = ( w e. _V |-> ( w u. B ) )
rdgssun.2
|- B e. _V
Assertion rdgssun
|- ( ( X e. On /\ Y e. X ) -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) )

Proof

Step Hyp Ref Expression
1 rdgssun.1
 |-  F = ( w e. _V |-> ( w u. B ) )
2 rdgssun.2
 |-  B e. _V
3 nfsbc1v
 |-  F/ x [. (/) / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x )
4 0ex
 |-  (/) e. _V
5 rzal
 |-  ( x = (/) -> A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) )
6 sbceq1a
 |-  ( x = (/) -> ( A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> [. (/) / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) )
7 5 6 mpbid
 |-  ( x = (/) -> [. (/) / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) )
8 3 4 7 vtoclef
 |-  [. (/) / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x )
9 vex
 |-  y e. _V
10 9 elsuc
 |-  ( y e. suc x <-> ( y e. x \/ y = x ) )
11 ssun1
 |-  ( rec ( F , A ) ` x ) C_ ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B )
12 fvex
 |-  ( rec ( F , A ) ` x ) e. _V
13 2 csbex
 |-  [_ ( rec ( F , A ) ` x ) / w ]_ B e. _V
14 12 13 unex
 |-  ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B ) e. _V
15 nfcv
 |-  F/_ w A
16 nfcv
 |-  F/_ w x
17 nfmpt1
 |-  F/_ w ( w e. _V |-> ( w u. B ) )
18 1 17 nfcxfr
 |-  F/_ w F
19 18 15 nfrdg
 |-  F/_ w rec ( F , A )
20 19 16 nffv
 |-  F/_ w ( rec ( F , A ) ` x )
21 20 nfcsb1
 |-  F/_ w [_ ( rec ( F , A ) ` x ) / w ]_ B
22 20 21 nfun
 |-  F/_ w ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B )
23 rdgeq1
 |-  ( F = ( w e. _V |-> ( w u. B ) ) -> rec ( F , A ) = rec ( ( w e. _V |-> ( w u. B ) ) , A ) )
24 1 23 ax-mp
 |-  rec ( F , A ) = rec ( ( w e. _V |-> ( w u. B ) ) , A )
25 id
 |-  ( w = ( rec ( F , A ) ` x ) -> w = ( rec ( F , A ) ` x ) )
26 csbeq1a
 |-  ( w = ( rec ( F , A ) ` x ) -> B = [_ ( rec ( F , A ) ` x ) / w ]_ B )
27 25 26 uneq12d
 |-  ( w = ( rec ( F , A ) ` x ) -> ( w u. B ) = ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B ) )
28 15 16 22 24 27 rdgsucmptf
 |-  ( ( x e. On /\ ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B ) e. _V ) -> ( rec ( F , A ) ` suc x ) = ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B ) )
29 14 28 mpan2
 |-  ( x e. On -> ( rec ( F , A ) ` suc x ) = ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B ) )
30 11 29 sseqtrrid
 |-  ( x e. On -> ( rec ( F , A ) ` x ) C_ ( rec ( F , A ) ` suc x ) )
31 sstr2
 |-  ( ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) -> ( ( rec ( F , A ) ` x ) C_ ( rec ( F , A ) ` suc x ) -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) )
32 30 31 syl5com
 |-  ( x e. On -> ( ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) )
33 32 imim2d
 |-  ( x e. On -> ( ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) -> ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) )
34 33 imp
 |-  ( ( x e. On /\ ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) -> ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) )
35 fveq2
 |-  ( y = x -> ( rec ( F , A ) ` y ) = ( rec ( F , A ) ` x ) )
36 35 sseq1d
 |-  ( y = x -> ( ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) <-> ( rec ( F , A ) ` x ) C_ ( rec ( F , A ) ` suc x ) ) )
37 30 36 syl5ibrcom
 |-  ( x e. On -> ( y = x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) )
38 37 adantr
 |-  ( ( x e. On /\ ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) -> ( y = x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) )
39 34 38 jaod
 |-  ( ( x e. On /\ ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) -> ( ( y e. x \/ y = x ) -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) )
40 10 39 syl5bi
 |-  ( ( x e. On /\ ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) -> ( y e. suc x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) )
41 40 ex
 |-  ( x e. On -> ( ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) -> ( y e. suc x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) )
42 41 ralimdv2
 |-  ( x e. On -> ( A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) -> A. y e. suc x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) )
43 df-sbc
 |-  ( [. suc x / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> suc x e. { x | A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) } )
44 vex
 |-  x e. _V
45 44 sucex
 |-  suc x e. _V
46 fveq2
 |-  ( z = suc x -> ( rec ( F , A ) ` z ) = ( rec ( F , A ) ` suc x ) )
47 46 sseq2d
 |-  ( z = suc x -> ( ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) <-> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) )
48 47 raleqbi1dv
 |-  ( z = suc x -> ( A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) <-> A. y e. suc x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) )
49 fveq2
 |-  ( x = z -> ( rec ( F , A ) ` x ) = ( rec ( F , A ) ` z ) )
50 49 sseq2d
 |-  ( x = z -> ( ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) ) )
51 50 raleqbi1dv
 |-  ( x = z -> ( A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) ) )
52 51 cbvabv
 |-  { x | A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) } = { z | A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) }
53 45 48 52 elab2
 |-  ( suc x e. { x | A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) } <-> A. y e. suc x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) )
54 43 53 bitri
 |-  ( [. suc x / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> A. y e. suc x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) )
55 42 54 syl6ibr
 |-  ( x e. On -> ( A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) -> [. suc x / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) )
56 ssiun2
 |-  ( y e. z -> ( rec ( F , A ) ` y ) C_ U_ y e. z ( rec ( F , A ) ` y ) )
57 56 adantl
 |-  ( ( Lim z /\ y e. z ) -> ( rec ( F , A ) ` y ) C_ U_ y e. z ( rec ( F , A ) ` y ) )
58 vex
 |-  z e. _V
59 rdglim2a
 |-  ( ( z e. _V /\ Lim z ) -> ( rec ( F , A ) ` z ) = U_ y e. z ( rec ( F , A ) ` y ) )
60 58 59 mpan
 |-  ( Lim z -> ( rec ( F , A ) ` z ) = U_ y e. z ( rec ( F , A ) ` y ) )
61 60 adantr
 |-  ( ( Lim z /\ y e. z ) -> ( rec ( F , A ) ` z ) = U_ y e. z ( rec ( F , A ) ` y ) )
62 57 61 sseqtrrd
 |-  ( ( Lim z /\ y e. z ) -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) )
63 62 ralrimiva
 |-  ( Lim z -> A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) )
64 df-sbc
 |-  ( [. z / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> z e. { x | A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) } )
65 52 eleq2i
 |-  ( z e. { x | A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) } <-> z e. { z | A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) } )
66 64 65 bitri
 |-  ( [. z / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> z e. { z | A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) } )
67 abid
 |-  ( z e. { z | A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) } <-> A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) )
68 66 67 bitri
 |-  ( [. z / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) )
69 63 68 sylibr
 |-  ( Lim z -> [. z / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) )
70 69 a1d
 |-  ( Lim z -> ( A. x e. z A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) -> [. z / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) )
71 8 55 70 tfindes
 |-  ( x e. On -> A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) )
72 rsp
 |-  ( A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) -> ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) )
73 71 72 syl
 |-  ( x e. On -> ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) )
74 eleq1
 |-  ( x = X -> ( x e. On <-> X e. On ) )
75 74 adantl
 |-  ( ( y = Y /\ x = X ) -> ( x e. On <-> X e. On ) )
76 eleq12
 |-  ( ( y = Y /\ x = X ) -> ( y e. x <-> Y e. X ) )
77 fveq2
 |-  ( y = Y -> ( rec ( F , A ) ` y ) = ( rec ( F , A ) ` Y ) )
78 77 adantr
 |-  ( ( y = Y /\ x = X ) -> ( rec ( F , A ) ` y ) = ( rec ( F , A ) ` Y ) )
79 fveq2
 |-  ( x = X -> ( rec ( F , A ) ` x ) = ( rec ( F , A ) ` X ) )
80 79 adantl
 |-  ( ( y = Y /\ x = X ) -> ( rec ( F , A ) ` x ) = ( rec ( F , A ) ` X ) )
81 78 80 sseq12d
 |-  ( ( y = Y /\ x = X ) -> ( ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) )
82 76 81 imbi12d
 |-  ( ( y = Y /\ x = X ) -> ( ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) <-> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) )
83 75 82 imbi12d
 |-  ( ( y = Y /\ x = X ) -> ( ( x e. On -> ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) <-> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) ) )
84 73 83 mpbii
 |-  ( ( y = Y /\ x = X ) -> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) )
85 84 ex
 |-  ( y = Y -> ( x = X -> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) ) )
86 85 vtocleg
 |-  ( Y e. X -> ( x = X -> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) ) )
87 86 com12
 |-  ( x = X -> ( Y e. X -> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) ) )
88 87 vtocleg
 |-  ( X e. On -> ( Y e. X -> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) ) )
89 88 pm2.43b
 |-  ( Y e. X -> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) )
90 89 pm2.43b
 |-  ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) )
91 90 imp
 |-  ( ( X e. On /\ Y e. X ) -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) )