Metamath Proof Explorer

Theorem setrec1lem4

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 ⊢ Ⅎ z φ
setrec1lem4.2 ⊢ Y = y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
setrec1lem4.3 ⊢ φ → A ∈ V
setrec1lem4.4 ⊢ φ → A ⊆ X
setrec1lem4.5 ⊢ φ → X ∈ Y
Assertion setrec1lem4 ⊢ φ → X ∪ F ⁡ A ∈ Y

Proof

Step Hyp Ref Expression
1 setrec1lem4.1 ⊢ Ⅎ z φ
2 setrec1lem4.2 ⊢ Y = y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
3 setrec1lem4.3 ⊢ φ → A ∈ V
4 setrec1lem4.4 ⊢ φ → A ⊆ X
5 setrec1lem4.5 ⊢ φ → X ∈ Y
6 id ⊢ w ⊆ X → w ⊆ X
7 ssun1 ⊢ X ⊆ X ∪ F ⁡ A
8 6 7 sstrdi ⊢ w ⊆ X → w ⊆ X ∪ F ⁡ A
9 8 imim1i ⊢ w ⊆ X ∪ F ⁡ A → w ⊆ z → F ⁡ w ⊆ z → w ⊆ X → w ⊆ z → F ⁡ w ⊆ z
10 9 alimi ⊢ ∀ w w ⊆ X ∪ F ⁡ A → w ⊆ z → F ⁡ w ⊆ z → ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z
11 2 5 setrec1lem1 ⊢ φ → X ∈ Y ↔ ∀ z ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → X ⊆ z
12 5 11 mpbid ⊢ φ → ∀ z ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → X ⊆ z
13 sp ⊢ ∀ z ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → X ⊆ z → ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → X ⊆ z
14 12 13 syl ⊢ φ → ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → X ⊆ z
15 sstr2 ⊢ A ⊆ X → X ⊆ z → A ⊆ z
16 4 15 syl ⊢ φ → X ⊆ z → A ⊆ z
17 14 16 syld ⊢ φ → ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → A ⊆ z
18 sseq1 ⊢ w = A → w ⊆ X ↔ A ⊆ X
19 sseq1 ⊢ w = A → w ⊆ z ↔ A ⊆ z
20 fveq2 ⊢ w = A → F ⁡ w = F ⁡ A
21 20 sseq1d ⊢ w = A → F ⁡ w ⊆ z ↔ F ⁡ A ⊆ z
22 19 21 imbi12d ⊢ w = A → w ⊆ z → F ⁡ w ⊆ z ↔ A ⊆ z → F ⁡ A ⊆ z
23 18 22 imbi12d ⊢ w = A → w ⊆ X → w ⊆ z → F ⁡ w ⊆ z ↔ A ⊆ X → A ⊆ z → F ⁡ A ⊆ z
24 3 23 spcdvw ⊢ φ → ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → A ⊆ X → A ⊆ z → F ⁡ A ⊆ z
25 4 24 mpid ⊢ φ → ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → A ⊆ z → F ⁡ A ⊆ z
26 17 25 mpdd ⊢ φ → ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → F ⁡ A ⊆ z
27 14 26 jcad ⊢ φ → ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → X ⊆ z ∧ F ⁡ A ⊆ z
28 10 27 syl5 ⊢ φ → ∀ w w ⊆ X ∪ F ⁡ A → w ⊆ z → F ⁡ w ⊆ z → X ⊆ z ∧ F ⁡ A ⊆ z
29 unss ⊢ X ⊆ z ∧ F ⁡ A ⊆ z ↔ X ∪ F ⁡ A ⊆ z
30 28 29 syl6ib ⊢ φ → ∀ w w ⊆ X ∪ F ⁡ A → w ⊆ z → F ⁡ w ⊆ z → X ∪ F ⁡ A ⊆ z
31 1 30 alrimi ⊢ φ → ∀ z ∀ w w ⊆ X ∪ F ⁡ A → w ⊆ z → F ⁡ w ⊆ z → X ∪ F ⁡ A ⊆ z
32 fvex ⊢ F ⁡ A ∈ V
33 unexg ⊢ X ∈ Y ∧ F ⁡ A ∈ V → X ∪ F ⁡ A ∈ V
34 5 32 33 sylancl ⊢ φ → X ∪ F ⁡ A ∈ V
35 2 34 setrec1lem1 ⊢ φ → X ∪ F ⁡ A ∈ Y ↔ ∀ z ∀ w w ⊆ X ∪ F ⁡ A → w ⊆ z → F ⁡ w ⊆ z → X ∪ F ⁡ A ⊆ z
36 31 35 mpbird ⊢ φ → X ∪ F ⁡ A ∈ Y