Metamath Proof Explorer

Theorem setrec1

Description: This is the first of two fundamental theorems about set recursion from which all other facts will be derived. It states that the class setrecs ( F ) is closed under F . This effectively sets the actual value of setrecs ( F ) as a lower bound for setrecs ( F ) , as it implies that any set generated by successive applications of F is a member of B . This theorem "gets off the ground" because we can start by letting A = (/) , and the hypotheses of the theorem will hold trivially.

Variable B represents an abbreviation of setrecs ( F ) or another name of setrecs ( F ) (for an example of the latter, see theorem setrecon).

Proof summary: Assume that A C_ B , meaning that all elements of A are in some set recursively generated by F . Then by setrec1lem3 , A is a subset of some set recursively generated by F . (It turns out that A itself is recursively generated by F , but we don't need this fact. See the comment to setrec1lem3 .) Therefore, by setrec1lem4 , ( FA ) is a subset of some set recursively generated by F . Thus, by ssuni , it is a subset of the union of all sets recursively generated by F .

See df-setrecs for a detailed description of how the setrecs definition works.

(Contributed by Emmett Weisz, 9-Oct-2020)

Ref Expression
Hypotheses setrec1.b ⊢ B = setrecs ⁡ F
setrec1.v ⊢ φ → A ∈ V
setrec1.a ⊢ φ → A ⊆ B
Assertion setrec1 ⊢ φ → F ⁡ A ⊆ B

Proof

Step Hyp Ref Expression
1 setrec1.b ⊢ B = setrecs ⁡ F
2 setrec1.v ⊢ φ → A ∈ V
3 setrec1.a ⊢ φ → A ⊆ B
4 eqid ⊢ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z = y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
5 3 sseld ⊢ φ → a ∈ A → a ∈ B
6 5 imp ⊢ φ ∧ a ∈ A → a ∈ B
7 df-setrecs ⊢ setrecs ⁡ F = ⋃ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
8 1 7 eqtri ⊢ B = ⋃ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
9 6 8 eleqtrdi ⊢ φ ∧ a ∈ A → a ∈ ⋃ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
10 eluni ⊢ a ∈ ⋃ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z ↔ ∃ x a ∈ x ∧ x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
11 9 10 sylib ⊢ φ ∧ a ∈ A → ∃ x a ∈ x ∧ x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
12 11 ralrimiva ⊢ φ → ∀ a ∈ A ∃ x a ∈ x ∧ x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
13 4 2 12 setrec1lem3 ⊢ φ → ∃ x A ⊆ x ∧ x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
14 nfv ⊢ Ⅎ z φ
15 nfv ⊢ Ⅎ z A ⊆ x
16 nfaba1 ⊢ Ⅎ _ z y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
17 16 nfel2 ⊢ Ⅎ z x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
18 15 17 nfan ⊢ Ⅎ z A ⊆ x ∧ x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
19 14 18 nfan ⊢ Ⅎ z φ ∧ A ⊆ x ∧ x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
20 2 adantr ⊢ φ ∧ A ⊆ x ∧ x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z → A ∈ V
21 simprl ⊢ φ ∧ A ⊆ x ∧ x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z → A ⊆ x
22 simprr ⊢ φ ∧ A ⊆ x ∧ x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z → x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
23 19 4 20 21 22 setrec1lem4 ⊢ φ ∧ A ⊆ x ∧ x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z → x ∪ F ⁡ A ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
24 ssun2 ⊢ F ⁡ A ⊆ x ∪ F ⁡ A
25 23 24 jctil ⊢ φ ∧ A ⊆ x ∧ x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z → F ⁡ A ⊆ x ∪ F ⁡ A ∧ x ∪ F ⁡ A ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
26 ssuni ⊢ F ⁡ A ⊆ x ∪ F ⁡ A ∧ x ∪ F ⁡ A ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z → F ⁡ A ⊆ ⋃ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
27 25 26 syl ⊢ φ ∧ A ⊆ x ∧ x ∈ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z → F ⁡ A ⊆ ⋃ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
28 13 27 exlimddv ⊢ φ → F ⁡ A ⊆ ⋃ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
29 28 8 sseqtrrdi ⊢ φ → F ⁡ A ⊆ B