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 | ⊢ 𝑌 = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } | |
| setrec1lem1.2 | ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) | ||
| Assertion | setrec1lem1 | ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑌 ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑋 ⊆ 𝑧 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | setrec1lem1.1 | ⊢ 𝑌 = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } | |
| 2 | setrec1lem1.2 | ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) | |
| 3 | sseq2 | ⊢ ( 𝑦 = 𝑋 → ( 𝑤 ⊆ 𝑦 ↔ 𝑤 ⊆ 𝑋 ) ) | |
| 4 | 3 | imbi1d | ⊢ ( 𝑦 = 𝑋 → ( ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) ↔ ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) ) ) |
| 5 | 4 | albidv | ⊢ ( 𝑦 = 𝑋 → ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) ↔ ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) ) ) |
| 6 | sseq1 | ⊢ ( 𝑦 = 𝑋 → ( 𝑦 ⊆ 𝑧 ↔ 𝑋 ⊆ 𝑧 ) ) | |
| 7 | 5 6 | imbi12d | ⊢ ( 𝑦 = 𝑋 → ( ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) ↔ ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑋 ⊆ 𝑧 ) ) ) |
| 8 | 7 | albidv | ⊢ ( 𝑦 = 𝑋 → ( ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑋 ⊆ 𝑧 ) ) ) |
| 9 | 8 1 | elab2g | ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ 𝑌 ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑋 ⊆ 𝑧 ) ) ) |
| 10 | 2 9 | syl | ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑌 ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑋 ⊆ 𝑧 ) ) ) |