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∈V⟼w∪B
rdgssun.2 ⊢B∈V
Assertion rdgssun ⊢X∈On∧Y∈X→rec⁡FA⁡Y⊆rec⁡FA⁡X

Proof

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