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 ∀ w w ⊆ 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 ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
2 setrec1lem2.2 ⊢ φ → X ∈ V
3 setrec1lem2.3 ⊢ φ → X ⊆ Y
4 dfss3 ⊢ X ⊆ Y ↔ ∀ x ∈ X x ∈ Y
5 3 4 sylib ⊢ φ → ∀ x ∈ X x ∈ Y
6 vex ⊢ x ∈ V
7 6 a1i ⊢ φ → x ∈ V
8 1 7 setrec1lem1 ⊢ φ → x ∈ Y ↔ ∀ z ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z
9 8 ralbidv ⊢ φ → ∀ x ∈ X x ∈ Y ↔ ∀ x ∈ X ∀ z ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z
10 5 9 mpbid ⊢ φ → ∀ x ∈ X ∀ z ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z
11 ralcom4 ⊢ ∀ x ∈ X ∀ z ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z ↔ ∀ z ∀ x ∈ X ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z
12 10 11 sylib ⊢ φ → ∀ z ∀ x ∈ X ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z
13 nfra1 ⊢ Ⅎ x ∀ x ∈ X ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z
14 nfv ⊢ Ⅎ x ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z
15 rsp ⊢ ∀ x ∈ X ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z → x ∈ X → ∀ w w ⊆ 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 → ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z → ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z
21 20 imim1d ⊢ x ∈ X → ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z → ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z
22 15 21 sylcom ⊢ ∀ x ∈ X ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z → x ∈ X → ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z
23 22 com23 ⊢ ∀ x ∈ X ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z → ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z → x ∈ X → x ⊆ z
24 13 14 23 ralrimd ⊢ ∀ x ∈ X ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z → ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z → ∀ x ∈ X x ⊆ z
25 24 alimi ⊢ ∀ z ∀ x ∈ X ∀ w w ⊆ x → w ⊆ z → F ⁡ w ⊆ z → x ⊆ z → ∀ z ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z → ∀ x ∈ X x ⊆ z
26 12 25 syl ⊢ φ → ∀ z ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z → ∀ x ∈ X x ⊆ z
27 unissb ⊢ ⋃ X ⊆ z ↔ ∀ x ∈ X x ⊆ z
28 27 imbi2i ⊢ ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z → ⋃ X ⊆ z ↔ ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z → ∀ x ∈ X x ⊆ z
29 28 albii ⊢ ∀ z ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z → ⋃ X ⊆ z ↔ ∀ z ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z → ∀ x ∈ X x ⊆ z
30 26 29 sylibr ⊢ φ → ∀ z ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z → ⋃ X ⊆ z
31 2 uniexd ⊢ φ → ⋃ X ∈ V
32 1 31 setrec1lem1 ⊢ φ → ⋃ X ∈ Y ↔ ∀ z ∀ w w ⊆ ⋃ X → w ⊆ z → F ⁡ w ⊆ z → ⋃ X ⊆ z
33 30 32 mpbird ⊢ φ → ⋃ X ∈ Y