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 biimtrid 
 |-  ( ( 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 imbitrrdi 
 |-  ( 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 ) )