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 ( F ) is closed under F . This effectively sets the actual value of setrecs ( F ) as a lower bound for setrecs ( F ) , as it implies that any set generated by successive applications of F is a member of B . This theorem "gets off the ground" because we can start by letting A = (/) , and the hypotheses of the theorem will hold trivially.
Variable B represents an abbreviation of setrecs ( F ) or another name of setrecs ( F ) (for an example of the latter, see theorem setrecon).
Proof summary: Assume that A C_ B , meaning that all elements of A are in some set recursively generated by F . Then by setrec1lem3 , A is a subset of some set recursively generated by F . (It turns out that A itself is recursively generated by F , but we don't need this fact. See the comment to setrec1lem3 .) Therefore, by setrec1lem4 , ( FA ) is a subset of some set recursively generated by F . Thus, by ssuni , it is a subset of the union of all sets recursively generated by F .
See df-setrecs for a detailed description of how the setrecs definition works.
(Contributed by Emmett Weisz, 9-Oct-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | setrec1.b | ⊢ 𝐵 = setrecs ( 𝐹 ) | |
| setrec1.v | ⊢ ( 𝜑 → 𝐴 ∈ V ) | ||
| setrec1.a | ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 ) | ||
| Assertion | setrec1 | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ⊆ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | setrec1.b | ⊢ 𝐵 = setrecs ( 𝐹 ) | |
| 2 | setrec1.v | ⊢ ( 𝜑 → 𝐴 ∈ V ) | |
| 3 | setrec1.a | ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 ) | |
| 4 | eqid | ⊢ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } | |
| 5 | 3 | sseld | ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐴 → 𝑎 ∈ 𝐵 ) ) |
| 6 | 5 | imp | ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐵 ) |
| 7 | df-setrecs | ⊢ setrecs ( 𝐹 ) = ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } | |
| 8 | 1 7 | eqtri | ⊢ 𝐵 = ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } |
| 9 | 6 8 | eleqtrdi | ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) |
| 10 | eluni | ⊢ ( 𝑎 ∈ ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ↔ ∃ 𝑥 ( 𝑎 ∈ 𝑥 ∧ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) ) | |
| 11 | 9 10 | sylib | ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑎 ∈ 𝑥 ∧ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) ) |
| 12 | 11 | ralrimiva | ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ( 𝑎 ∈ 𝑥 ∧ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) ) |
| 13 | 4 2 12 | setrec1lem3 | ⊢ ( 𝜑 → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) ) |
| 14 | nfv | ⊢ Ⅎ 𝑧 𝜑 | |
| 15 | nfv | ⊢ Ⅎ 𝑧 𝐴 ⊆ 𝑥 | |
| 16 | nfaba1 | ⊢ Ⅎ 𝑧 { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } | |
| 17 | 16 | nfel2 | ⊢ Ⅎ 𝑧 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } |
| 18 | 15 17 | nfan | ⊢ Ⅎ 𝑧 ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) |
| 19 | 14 18 | nfan | ⊢ Ⅎ 𝑧 ( 𝜑 ∧ ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) ) |
| 20 | 2 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) ) → 𝐴 ∈ V ) |
| 21 | simprl | ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) ) → 𝐴 ⊆ 𝑥 ) | |
| 22 | simprr | ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) ) → 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) | |
| 23 | 19 4 20 21 22 | setrec1lem4 | ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) ) → ( 𝑥 ∪ ( 𝐹 ‘ 𝐴 ) ) ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) |
| 24 | ssun2 | ⊢ ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝑥 ∪ ( 𝐹 ‘ 𝐴 ) ) | |
| 25 | 23 24 | jctil | ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) ) → ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝑥 ∪ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑥 ∪ ( 𝐹 ‘ 𝐴 ) ) ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) ) |
| 26 | ssuni | ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝑥 ∪ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑥 ∪ ( 𝐹 ‘ 𝐴 ) ) ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) → ( 𝐹 ‘ 𝐴 ) ⊆ ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) | |
| 27 | 25 26 | syl | ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) |
| 28 | 13 27 | exlimddv | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ⊆ ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ) |
| 29 | 28 8 | sseqtrrdi | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ⊆ 𝐵 ) |