Description: Lemma for setrec1 . If X is recursively generated by F , then so is X u. ( FA ) .
In the proof of setrec1 , the following is substituted for this theorem's ph : ( ph /\ ( A C_ x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( Fw ) C_ z ) ) -> y C_ z ) } ) ) Therefore, we cannot declare z to be a distinct variable from ph , since we need it to appear as a bound variable in ph . This theorem can be proven without the hypothesis F/ z ph , but the proof would be harder to read because theorems in deduction form would be interrupted by theorems like eximi , making the antecedent of each line something more complicated than ph . The proof of setrec1lem2 could similarly be made easier to read by adding the hypothesis F/ z ph , but I had already finished the proof and decided to leave it as is. (Contributed by Emmett Weisz, 26-Nov-2020) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | setrec1lem4.1 | ⊢ Ⅎ 𝑧 𝜑 | |
| setrec1lem4.2 | ⊢ 𝑌 = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } | ||
| setrec1lem4.3 | ⊢ ( 𝜑 → 𝐴 ∈ V ) | ||
| setrec1lem4.4 | ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 ) | ||
| setrec1lem4.5 | ⊢ ( 𝜑 → 𝑋 ∈ 𝑌 ) | ||
| Assertion | setrec1lem4 | ⊢ ( 𝜑 → ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) ∈ 𝑌 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | setrec1lem4.1 | ⊢ Ⅎ 𝑧 𝜑 | |
| 2 | setrec1lem4.2 | ⊢ 𝑌 = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } | |
| 3 | setrec1lem4.3 | ⊢ ( 𝜑 → 𝐴 ∈ V ) | |
| 4 | setrec1lem4.4 | ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 ) | |
| 5 | setrec1lem4.5 | ⊢ ( 𝜑 → 𝑋 ∈ 𝑌 ) | |
| 6 | id | ⊢ ( 𝑤 ⊆ 𝑋 → 𝑤 ⊆ 𝑋 ) | |
| 7 | ssun1 | ⊢ 𝑋 ⊆ ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) | |
| 8 | 6 7 | sstrdi | ⊢ ( 𝑤 ⊆ 𝑋 → 𝑤 ⊆ ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) ) |
| 9 | 8 | imim1i | ⊢ ( ( 𝑤 ⊆ ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) ) |
| 10 | 9 | alimi | ⊢ ( ∀ 𝑤 ( 𝑤 ⊆ ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) ) |
| 11 | 2 5 | setrec1lem1 | ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑌 ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑋 ⊆ 𝑧 ) ) ) |
| 12 | 5 11 | mpbid | ⊢ ( 𝜑 → ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑋 ⊆ 𝑧 ) ) |
| 13 | sp | ⊢ ( ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑋 ⊆ 𝑧 ) → ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑋 ⊆ 𝑧 ) ) | |
| 14 | 12 13 | syl | ⊢ ( 𝜑 → ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑋 ⊆ 𝑧 ) ) |
| 15 | sstr2 | ⊢ ( 𝐴 ⊆ 𝑋 → ( 𝑋 ⊆ 𝑧 → 𝐴 ⊆ 𝑧 ) ) | |
| 16 | 4 15 | syl | ⊢ ( 𝜑 → ( 𝑋 ⊆ 𝑧 → 𝐴 ⊆ 𝑧 ) ) |
| 17 | 14 16 | syld | ⊢ ( 𝜑 → ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝐴 ⊆ 𝑧 ) ) |
| 18 | sseq1 | ⊢ ( 𝑤 = 𝐴 → ( 𝑤 ⊆ 𝑋 ↔ 𝐴 ⊆ 𝑋 ) ) | |
| 19 | sseq1 | ⊢ ( 𝑤 = 𝐴 → ( 𝑤 ⊆ 𝑧 ↔ 𝐴 ⊆ 𝑧 ) ) | |
| 20 | fveq2 | ⊢ ( 𝑤 = 𝐴 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝐴 ) ) | |
| 21 | 20 | sseq1d | ⊢ ( 𝑤 = 𝐴 → ( ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ↔ ( 𝐹 ‘ 𝐴 ) ⊆ 𝑧 ) ) |
| 22 | 19 21 | imbi12d | ⊢ ( 𝑤 = 𝐴 → ( ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ↔ ( 𝐴 ⊆ 𝑧 → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑧 ) ) ) |
| 23 | 18 22 | imbi12d | ⊢ ( 𝑤 = 𝐴 → ( ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) ↔ ( 𝐴 ⊆ 𝑋 → ( 𝐴 ⊆ 𝑧 → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑧 ) ) ) ) |
| 24 | 3 23 | spcdvw | ⊢ ( 𝜑 → ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ( 𝐴 ⊆ 𝑋 → ( 𝐴 ⊆ 𝑧 → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑧 ) ) ) ) |
| 25 | 4 24 | mpid | ⊢ ( 𝜑 → ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ( 𝐴 ⊆ 𝑧 → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑧 ) ) ) |
| 26 | 17 25 | mpdd | ⊢ ( 𝜑 → ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑧 ) ) |
| 27 | 14 26 | jcad | ⊢ ( 𝜑 → ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ( 𝑋 ⊆ 𝑧 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝑧 ) ) ) |
| 28 | 10 27 | syl5 | ⊢ ( 𝜑 → ( ∀ 𝑤 ( 𝑤 ⊆ ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ( 𝑋 ⊆ 𝑧 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝑧 ) ) ) |
| 29 | unss | ⊢ ( ( 𝑋 ⊆ 𝑧 ∧ ( 𝐹 ‘ 𝐴 ) ⊆ 𝑧 ) ↔ ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) ⊆ 𝑧 ) | |
| 30 | 28 29 | imbitrdi | ⊢ ( 𝜑 → ( ∀ 𝑤 ( 𝑤 ⊆ ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) ⊆ 𝑧 ) ) |
| 31 | 1 30 | alrimi | ⊢ ( 𝜑 → ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) ⊆ 𝑧 ) ) |
| 32 | fvex | ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V | |
| 33 | unexg | ⊢ ( ( 𝑋 ∈ 𝑌 ∧ ( 𝐹 ‘ 𝐴 ) ∈ V ) → ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) ∈ V ) | |
| 34 | 5 32 33 | sylancl | ⊢ ( 𝜑 → ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) ∈ V ) |
| 35 | 2 34 | setrec1lem1 | ⊢ ( 𝜑 → ( ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) ∈ 𝑌 ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) ⊆ 𝑧 ) ) ) |
| 36 | 31 35 | mpbird | ⊢ ( 𝜑 → ( 𝑋 ∪ ( 𝐹 ‘ 𝐴 ) ) ∈ 𝑌 ) |