Metamath Proof Explorer

Theorem setrec1lem2

Description: Lemma for setrec1 . If a family of sets are all recursively generated by F , so is their union. In this theorem, X is a family of sets which are all elements of Y , and V is any class. Use dfss3 , equivalence and equality theorems, and unissb at the end. Sandwich with applications of setrec1lem1. (Contributed by Emmett Weisz, 24-Jan-2021) (New usage is discouraged.)

Ref Expression
Hypotheses setrec1lem2.1 ⊢Y=y|∀z∀ww⊆y→w⊆z→F⁡w⊆z→y⊆z
setrec1lem2.2 ⊢φ→X∈V
setrec1lem2.3 ⊢φ→X⊆Y
Assertion setrec1lem2 ⊢φ→⋃X∈Y

Proof

Step Hyp Ref Expression
1 setrec1lem2.1 ⊢Y=y|∀z∀ww⊆y→w⊆z→F⁡w⊆z→y⊆z
2 setrec1lem2.2 ⊢φ→X∈V
3 setrec1lem2.3 ⊢φ→X⊆Y
4 dfss3 ⊢X⊆Y↔∀x∈Xx∈Y
5 3 4 sylib ⊢φ→∀x∈Xx∈Y
6 vex ⊢x∈V
7 6 a1i ⊢φ→x∈V
8 1 7 setrec1lem1 ⊢φ→x∈Y↔∀z∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z
9 8 ralbidv ⊢φ→∀x∈Xx∈Y↔∀x∈X∀z∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z
10 5 9 mpbid ⊢φ→∀x∈X∀z∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z
11 ralcom4 ⊢∀x∈X∀z∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z↔∀z∀x∈X∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z
12 10 11 sylib ⊢φ→∀z∀x∈X∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z
13 nfra1 ⊢Ⅎx∀x∈X∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z
14 nfv ⊢Ⅎx∀ww⊆⋃X→w⊆z→F⁡w⊆z
15 rsp ⊢∀x∈X∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z→x∈X→∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z
16 elssuni ⊢x∈X→x⊆⋃X
17 sstr2 ⊢w⊆x→x⊆⋃X→w⊆⋃X
18 16 17 syl5com ⊢x∈X→w⊆x→w⊆⋃X
19 18 imim1d ⊢x∈X→w⊆⋃X→w⊆z→F⁡w⊆z→w⊆x→w⊆z→F⁡w⊆z
20 19 alimdv ⊢x∈X→∀ww⊆⋃X→w⊆z→F⁡w⊆z→∀ww⊆x→w⊆z→F⁡w⊆z
21 20 imim1d ⊢x∈X→∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z→∀ww⊆⋃X→w⊆z→F⁡w⊆z→x⊆z
22 15 21 sylcom ⊢∀x∈X∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z→x∈X→∀ww⊆⋃X→w⊆z→F⁡w⊆z→x⊆z
23 22 com23 ⊢∀x∈X∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z→∀ww⊆⋃X→w⊆z→F⁡w⊆z→x∈X→x⊆z
24 13 14 23 ralrimd ⊢∀x∈X∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z→∀ww⊆⋃X→w⊆z→F⁡w⊆z→∀x∈Xx⊆z
25 24 alimi ⊢∀z∀x∈X∀ww⊆x→w⊆z→F⁡w⊆z→x⊆z→∀z∀ww⊆⋃X→w⊆z→F⁡w⊆z→∀x∈Xx⊆z
26 12 25 syl ⊢φ→∀z∀ww⊆⋃X→w⊆z→F⁡w⊆z→∀x∈Xx⊆z
27 unissb ⊢⋃X⊆z↔∀x∈Xx⊆z
28 27 imbi2i ⊢∀ww⊆⋃X→w⊆z→F⁡w⊆z→⋃X⊆z↔∀ww⊆⋃X→w⊆z→F⁡w⊆z→∀x∈Xx⊆z
29 28 albii ⊢∀z∀ww⊆⋃X→w⊆z→F⁡w⊆z→⋃X⊆z↔∀z∀ww⊆⋃X→w⊆z→F⁡w⊆z→∀x∈Xx⊆z
30 26 29 sylibr ⊢φ→∀z∀ww⊆⋃X→w⊆z→F⁡w⊆z→⋃X⊆z
31 2 uniexd ⊢φ→⋃X∈V
32 1 31 setrec1lem1 ⊢φ→⋃X∈Y↔∀z∀ww⊆⋃X→w⊆z→F⁡w⊆z→⋃X⊆z
33 30 32 mpbird ⊢φ→⋃X∈Y