Mathbox for Emmett Weisz |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > setrec1 | Structured version Visualization version GIF version |
Description: This is the first of two
fundamental theorems about set recursion from
which all other facts will be derived. It states that the class
setrecs(𝐹) is closed under 𝐹. This
effectively sets the
actual value of setrecs(𝐹) as a lower bound for
setrecs(𝐹), as it implies that any set
generated by successive
applications of 𝐹 is a member of 𝐵. This
theorem "gets off the
ground" because we can start by letting 𝐴 = ∅, and the
hypotheses
of the theorem will hold trivially.
Variable 𝐵 represents an abbreviation of setrecs(𝐹) or another name of setrecs(𝐹) (for an example of the latter, see theorem setrecon). Proof summary: Assume that 𝐴 ⊆ 𝐵, meaning that all elements of 𝐴 are in some set recursively generated by 𝐹. Then by setrec1lem3 45840, 𝐴 is a subset of some set recursively generated by 𝐹. (It turns out that 𝐴 itself is recursively generated by 𝐹, but we don't need this fact. See the comment to setrec1lem3 45840.) Therefore, by setrec1lem4 45841, (𝐹‘𝐴) is a subset of some set recursively generated by 𝐹. Thus, by ssuni 4824, it is a subset of the union of all sets recursively generated by 𝐹. See df-setrecs 45835 for a detailed description of how the setrecs definition works. (Contributed by Emmett Weisz, 9-Oct-2020.) |
Ref | Expression |
---|---|
setrec1.b | ⊢ 𝐵 = setrecs(𝐹) |
setrec1.v | ⊢ (𝜑 → 𝐴 ∈ V) |
setrec1.a | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Ref | Expression |
---|---|
setrec1 | ⊢ (𝜑 → (𝐹‘𝐴) ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2738 | . . . 4 ⊢ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)} = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)} | |
2 | setrec1.v | . . . 4 ⊢ (𝜑 → 𝐴 ∈ V) | |
3 | setrec1.a | . . . . . . . . 9 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
4 | 3 | sseld 3877 | . . . . . . . 8 ⊢ (𝜑 → (𝑎 ∈ 𝐴 → 𝑎 ∈ 𝐵)) |
5 | 4 | imp 410 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐵) |
6 | setrec1.b | . . . . . . . 8 ⊢ 𝐵 = setrecs(𝐹) | |
7 | df-setrecs 45835 | . . . . . . . 8 ⊢ setrecs(𝐹) = ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)} | |
8 | 6, 7 | eqtri 2761 | . . . . . . 7 ⊢ 𝐵 = ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)} |
9 | 5, 8 | eleqtrdi 2843 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}) |
10 | eluni 4800 | . . . . . 6 ⊢ (𝑎 ∈ ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)} ↔ ∃𝑥(𝑎 ∈ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) | |
11 | 9, 10 | sylib 221 | . . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∃𝑥(𝑎 ∈ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) |
12 | 11 | ralrimiva 3096 | . . . 4 ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∃𝑥(𝑎 ∈ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) |
13 | 1, 2, 12 | setrec1lem3 45840 | . . 3 ⊢ (𝜑 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) |
14 | nfv 1920 | . . . . . . 7 ⊢ Ⅎ𝑧𝜑 | |
15 | nfv 1920 | . . . . . . . 8 ⊢ Ⅎ𝑧 𝐴 ⊆ 𝑥 | |
16 | nfaba1 2907 | . . . . . . . . 9 ⊢ Ⅎ𝑧{𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)} | |
17 | 16 | nfel2 2917 | . . . . . . . 8 ⊢ Ⅎ𝑧 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)} |
18 | 15, 17 | nfan 1905 | . . . . . . 7 ⊢ Ⅎ𝑧(𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}) |
19 | 14, 18 | nfan 1905 | . . . . . 6 ⊢ Ⅎ𝑧(𝜑 ∧ (𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) |
20 | 2 | adantr 484 | . . . . . 6 ⊢ ((𝜑 ∧ (𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) → 𝐴 ∈ V) |
21 | simprl 771 | . . . . . 6 ⊢ ((𝜑 ∧ (𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) → 𝐴 ⊆ 𝑥) | |
22 | simprr 773 | . . . . . 6 ⊢ ((𝜑 ∧ (𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) → 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}) | |
23 | 19, 1, 20, 21, 22 | setrec1lem4 45841 | . . . . 5 ⊢ ((𝜑 ∧ (𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) → (𝑥 ∪ (𝐹‘𝐴)) ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}) |
24 | ssun2 4064 | . . . . 5 ⊢ (𝐹‘𝐴) ⊆ (𝑥 ∪ (𝐹‘𝐴)) | |
25 | 23, 24 | jctil 523 | . . . 4 ⊢ ((𝜑 ∧ (𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) → ((𝐹‘𝐴) ⊆ (𝑥 ∪ (𝐹‘𝐴)) ∧ (𝑥 ∪ (𝐹‘𝐴)) ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) |
26 | ssuni 4824 | . . . 4 ⊢ (((𝐹‘𝐴) ⊆ (𝑥 ∪ (𝐹‘𝐴)) ∧ (𝑥 ∪ (𝐹‘𝐴)) ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}) → (𝐹‘𝐴) ⊆ ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}) | |
27 | 25, 26 | syl 17 | . . 3 ⊢ ((𝜑 ∧ (𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) → (𝐹‘𝐴) ⊆ ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}) |
28 | 13, 27 | exlimddv 1941 | . 2 ⊢ (𝜑 → (𝐹‘𝐴) ⊆ ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}) |
29 | 28, 8 | sseqtrrdi 3929 | 1 ⊢ (𝜑 → (𝐹‘𝐴) ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∀wal 1540 = wceq 1542 ∃wex 1786 ∈ wcel 2113 {cab 2716 Vcvv 3398 ∪ cun 3842 ⊆ wss 3844 ∪ cuni 4797 ‘cfv 6340 setrecscsetrecs 45834 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5155 ax-sep 5168 ax-nul 5175 ax-pow 5233 ax-pr 5297 ax-un 7480 ax-reg 9130 ax-inf2 9178 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-reu 3060 df-rab 3062 df-v 3400 df-sbc 3683 df-csb 3792 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-pss 3863 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-tp 4522 df-op 4524 df-uni 4798 df-int 4838 df-iun 4884 df-iin 4885 df-br 5032 df-opab 5094 df-mpt 5112 df-tr 5138 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5484 df-we 5486 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-om 7601 df-wrecs 7977 df-recs 8038 df-rdg 8076 df-r1 9267 df-rank 9268 df-setrecs 45835 |
This theorem is referenced by: elsetrecslem 45849 elsetrecs 45850 setrecsss 45851 setrecsres 45852 vsetrec 45853 onsetrec 45858 |
Copyright terms: Public domain | W3C validator |