Metamath Proof Explorer

Theorem setrec1lem1

Description: Lemma for setrec1 . This is a utility theorem showing the equivalence of the statement X e. Y and its expanded form. The proof uses elabg and equivalence theorems.

Variable Y is the class of sets y that are recursively generated by the function F . In other words, y e. Y iff by starting with the empty set and repeatedly applying F to subsets w of our set, we will eventually generate all the elements of Y . In this theorem, X is any element of Y , and V is any class. (Contributed by Emmett Weisz, 16-Oct-2020) (New usage is discouraged.)

Ref Expression
Hypotheses setrec1lem1.1 ⊢ Y = y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
setrec1lem1.2 ⊢ φ → X ∈ V
Assertion setrec1lem1 ⊢ φ → X ∈ Y ↔ ∀ z ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → X ⊆ z

Proof

Step Hyp Ref Expression
1 setrec1lem1.1 ⊢ Y = y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
2 setrec1lem1.2 ⊢ φ → X ∈ V
3 sseq2 ⊢ y = X → w ⊆ y ↔ w ⊆ X
4 3 imbi1d ⊢ y = X → w ⊆ y → w ⊆ z → F ⁡ w ⊆ z ↔ w ⊆ X → w ⊆ z → F ⁡ w ⊆ z
5 4 albidv ⊢ y = X → ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z ↔ ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z
6 sseq1 ⊢ y = X → y ⊆ z ↔ X ⊆ z
7 5 6 imbi12d ⊢ y = X → ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z ↔ ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → X ⊆ z
8 7 albidv ⊢ y = X → ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z ↔ ∀ z ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → X ⊆ z
9 8 1 elab2g ⊢ X ∈ V → X ∈ Y ↔ ∀ z ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → X ⊆ z
10 2 9 syl ⊢ φ → X ∈ Y ↔ ∀ z ∀ w w ⊆ X → w ⊆ z → F ⁡ w ⊆ z → X ⊆ z