Description: This is the second of two fundamental theorems about set recursion from which all other facts will be derived. It states that the class setrecs ( F ) is a subclass of all classes C that are closed under F . Taken together, Theorems setrec1 and setrec2v say that setrecs ( F ) is the minimal class closed under F .
We express this by saying that if F respects the C_ relation and C is closed under F , then B C_ C . By substituting strategically constructed classes for C , we can easily prove many useful properties. Although this theorem cannot show equality between B and C , if we intend to prove equality between B and some particular class (such as On ), we first apply this theorem, then the relevant induction theorem (such as tfi ) to the other class. (Contributed by Emmett Weisz, 15-Feb-2021) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | setrec2fun.1 | ⊢ Ⅎ 𝑎 𝐹 | |
| setrec2fun.2 | ⊢ 𝐵 = setrecs ( 𝐹 ) | ||
| setrec2fun.3 | ⊢ Fun 𝐹 | ||
| setrec2fun.4 | ⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ) ) | ||
| Assertion | setrec2fun | ⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | setrec2fun.1 | ⊢ Ⅎ 𝑎 𝐹 | |
| 2 | setrec2fun.2 | ⊢ 𝐵 = setrecs ( 𝐹 ) | |
| 3 | setrec2fun.3 | ⊢ Fun 𝐹 | |
| 4 | setrec2fun.4 | ⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ) ) | |
| 5 | df-setrecs | ⊢ setrecs ( 𝐹 ) = ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } | |
| 6 | 2 5 | eqtri | ⊢ 𝐵 = ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } |
| 7 | eqid | ⊢ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } | |
| 8 | vex | ⊢ 𝑥 ∈ V | |
| 9 | 8 | a1i | ⊢ ( 𝜑 → 𝑥 ∈ V ) |
| 10 | 7 9 | setrec1lem1 | ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) ) ) |
| 11 | id | ⊢ ( 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) | |
| 12 | inss1 | ⊢ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ⊆ 𝐶 | |
| 13 | 11 12 | sstrdi | ⊢ ( 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → 𝑤 ⊆ 𝐶 ) |
| 14 | nfv | ⊢ Ⅎ 𝑎 𝑤 ⊆ 𝐶 | |
| 15 | nfcv | ⊢ Ⅎ 𝑎 𝑤 | |
| 16 | 1 15 | nffv | ⊢ Ⅎ 𝑎 ( 𝐹 ‘ 𝑤 ) |
| 17 | nfcv | ⊢ Ⅎ 𝑎 𝐶 | |
| 18 | 16 17 | nfss | ⊢ Ⅎ 𝑎 ( 𝐹 ‘ 𝑤 ) ⊆ 𝐶 |
| 19 | 14 18 | nfim | ⊢ Ⅎ 𝑎 ( 𝑤 ⊆ 𝐶 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝐶 ) |
| 20 | sseq1 | ⊢ ( 𝑎 = 𝑤 → ( 𝑎 ⊆ 𝐶 ↔ 𝑤 ⊆ 𝐶 ) ) | |
| 21 | fveq2 | ⊢ ( 𝑎 = 𝑤 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑤 ) ) | |
| 22 | 21 | sseq1d | ⊢ ( 𝑎 = 𝑤 → ( ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ↔ ( 𝐹 ‘ 𝑤 ) ⊆ 𝐶 ) ) |
| 23 | 20 22 | imbi12d | ⊢ ( 𝑎 = 𝑤 → ( ( 𝑎 ⊆ 𝐶 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ) ↔ ( 𝑤 ⊆ 𝐶 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝐶 ) ) ) |
| 24 | 23 | biimpd | ⊢ ( 𝑎 = 𝑤 → ( ( 𝑎 ⊆ 𝐶 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ) → ( 𝑤 ⊆ 𝐶 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝐶 ) ) ) |
| 25 | 19 24 | spimfv | ⊢ ( ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ) → ( 𝑤 ⊆ 𝐶 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝐶 ) ) |
| 26 | 4 25 | syl | ⊢ ( 𝜑 → ( 𝑤 ⊆ 𝐶 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝐶 ) ) |
| 27 | 13 26 | syl5 | ⊢ ( 𝜑 → ( 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( 𝐹 ‘ 𝑤 ) ⊆ 𝐶 ) ) |
| 28 | 27 | imp | ⊢ ( ( 𝜑 ∧ 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) → ( 𝐹 ‘ 𝑤 ) ⊆ 𝐶 ) |
| 29 | 28 | 3adant2 | ⊢ ( ( 𝜑 ∧ 𝑤 ⊆ 𝑥 ∧ 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) → ( 𝐹 ‘ 𝑤 ) ⊆ 𝐶 ) |
| 30 | velpw | ⊢ ( 𝑤 ∈ 𝒫 𝑥 ↔ 𝑤 ⊆ 𝑥 ) | |
| 31 | eliman0 | ⊢ ( ( 𝑤 ∈ 𝒫 𝑥 ∧ ¬ ( 𝐹 ‘ 𝑤 ) = ∅ ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝒫 𝑥 ) ) | |
| 32 | 31 | ex | ⊢ ( 𝑤 ∈ 𝒫 𝑥 → ( ¬ ( 𝐹 ‘ 𝑤 ) = ∅ → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝒫 𝑥 ) ) ) |
| 33 | 30 32 | sylbir | ⊢ ( 𝑤 ⊆ 𝑥 → ( ¬ ( 𝐹 ‘ 𝑤 ) = ∅ → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝒫 𝑥 ) ) ) |
| 34 | elssuni | ⊢ ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝒫 𝑥 ) → ( 𝐹 ‘ 𝑤 ) ⊆ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) | |
| 35 | 33 34 | syl6 | ⊢ ( 𝑤 ⊆ 𝑥 → ( ¬ ( 𝐹 ‘ 𝑤 ) = ∅ → ( 𝐹 ‘ 𝑤 ) ⊆ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) |
| 36 | id | ⊢ ( ( 𝐹 ‘ 𝑤 ) = ∅ → ( 𝐹 ‘ 𝑤 ) = ∅ ) | |
| 37 | 0ss | ⊢ ∅ ⊆ ∪ ( 𝐹 “ 𝒫 𝑥 ) | |
| 38 | 36 37 | eqsstrdi | ⊢ ( ( 𝐹 ‘ 𝑤 ) = ∅ → ( 𝐹 ‘ 𝑤 ) ⊆ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) |
| 39 | 35 38 | pm2.61d2 | ⊢ ( 𝑤 ⊆ 𝑥 → ( 𝐹 ‘ 𝑤 ) ⊆ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) |
| 40 | 39 | 3ad2ant2 | ⊢ ( ( 𝜑 ∧ 𝑤 ⊆ 𝑥 ∧ 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) → ( 𝐹 ‘ 𝑤 ) ⊆ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) |
| 41 | 29 40 | ssind | ⊢ ( ( 𝜑 ∧ 𝑤 ⊆ 𝑥 ∧ 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) → ( 𝐹 ‘ 𝑤 ) ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) |
| 42 | 41 | 3exp | ⊢ ( 𝜑 → ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( 𝐹 ‘ 𝑤 ) ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) ) ) |
| 43 | 42 | alrimiv | ⊢ ( 𝜑 → ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( 𝐹 ‘ 𝑤 ) ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) ) ) |
| 44 | 8 | pwex | ⊢ 𝒫 𝑥 ∈ V |
| 45 | 44 | funimaex | ⊢ ( Fun 𝐹 → ( 𝐹 “ 𝒫 𝑥 ) ∈ V ) |
| 46 | 3 45 | ax-mp | ⊢ ( 𝐹 “ 𝒫 𝑥 ) ∈ V |
| 47 | 46 | uniex | ⊢ ∪ ( 𝐹 “ 𝒫 𝑥 ) ∈ V |
| 48 | 47 | inex2 | ⊢ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ∈ V |
| 49 | sseq2 | ⊢ ( 𝑧 = ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( 𝑤 ⊆ 𝑧 ↔ 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) ) | |
| 50 | sseq2 | ⊢ ( 𝑧 = ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ↔ ( 𝐹 ‘ 𝑤 ) ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) ) | |
| 51 | 49 50 | imbi12d | ⊢ ( 𝑧 = ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ↔ ( 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( 𝐹 ‘ 𝑤 ) ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) ) ) |
| 52 | 51 | imbi2d | ⊢ ( 𝑧 = ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) ↔ ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( 𝐹 ‘ 𝑤 ) ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) ) ) ) |
| 53 | 52 | albidv | ⊢ ( 𝑧 = ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) ↔ ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( 𝐹 ‘ 𝑤 ) ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) ) ) ) |
| 54 | sseq2 | ⊢ ( 𝑧 = ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( 𝑥 ⊆ 𝑧 ↔ 𝑥 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) ) | |
| 55 | 53 54 | imbi12d | ⊢ ( 𝑧 = ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) ↔ ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( 𝐹 ‘ 𝑤 ) ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) ) → 𝑥 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) ) ) |
| 56 | 48 55 | spcv | ⊢ ( ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) → ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) → ( 𝐹 ‘ 𝑤 ) ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) ) → 𝑥 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) ) |
| 57 | 43 56 | mpan9 | ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) ) → 𝑥 ⊆ ( 𝐶 ∩ ∪ ( 𝐹 “ 𝒫 𝑥 ) ) ) |
| 58 | 57 12 | sstrdi | ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝐶 ) |
| 59 | 58 | ex | ⊢ ( 𝜑 → ( ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) → 𝑥 ⊆ 𝐶 ) ) |
| 60 | 10 59 | sylbid | ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } → 𝑥 ⊆ 𝐶 ) ) |
| 61 | 60 | ralrimiv | ⊢ ( 𝜑 → ∀ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } 𝑥 ⊆ 𝐶 ) |
| 62 | unissb | ⊢ ( ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ⊆ 𝐶 ↔ ∀ 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } 𝑥 ⊆ 𝐶 ) | |
| 63 | 61 62 | sylibr | ⊢ ( 𝜑 → ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } ⊆ 𝐶 ) |
| 64 | 6 63 | eqsstrid | ⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 ) |