Metamath Proof Explorer

Theorem setrec1lem3

Description: Lemma for setrec1 . If each element a of A is covered by a set x recursively generated by F , then there is a single such set covering all of A . The set is constructed explicitly using setrec1lem2 . It turns out that x = A also works, i.e., given the hypotheses it is possible to prove that A e. Y . I don't know if proving this fact directly using setrec1lem1 would be any easier than the current proof using setrec1lem2 , and it would only slightly simplify the proof of setrec1 . Other than the use of bnd2d , this is a purely technical theorem for rearranging notation from that of setrec1lem2 to that of setrec1 . (Contributed by Emmett Weisz, 20-Jan-2021) (New usage is discouraged.)

Ref Expression
Hypotheses setrec1lem3.1 ⊢Y=y|∀z∀ww⊆y→w⊆z→F⁡w⊆z→y⊆z
setrec1lem3.2 ⊢φ→A∈V
setrec1lem3.3 ⊢φ→∀a∈A∃xa∈x∧x∈Y
Assertion setrec1lem3 ⊢φ→∃xA⊆x∧x∈Y

Proof

Step Hyp Ref Expression
1 setrec1lem3.1 ⊢Y=y|∀z∀ww⊆y→w⊆z→F⁡w⊆z→y⊆z
2 setrec1lem3.2 ⊢φ→A∈V
3 setrec1lem3.3 ⊢φ→∀a∈A∃xa∈x∧x∈Y
4 exancom ⊢∃xa∈x∧x∈Y↔∃xx∈Y∧a∈x
5 4 ralbii ⊢∀a∈A∃xa∈x∧x∈Y↔∀a∈A∃xx∈Y∧a∈x
6 3 5 sylib ⊢φ→∀a∈A∃xx∈Y∧a∈x
7 df-rex ⊢∃x∈Ya∈x↔∃xx∈Y∧a∈x
8 7 ralbii ⊢∀a∈A∃x∈Ya∈x↔∀a∈A∃xx∈Y∧a∈x
9 6 8 sylibr ⊢φ→∀a∈A∃x∈Ya∈x
10 2 9 bnd2d ⊢φ→∃vv⊆Y∧∀a∈A∃x∈va∈x
11 exancom ⊢∃xx∈v∧a∈x↔∃xa∈x∧x∈v
12 df-rex ⊢∃x∈va∈x↔∃xx∈v∧a∈x
13 eluni ⊢a∈⋃v↔∃xa∈x∧x∈v
14 11 12 13 3bitr4i ⊢∃x∈va∈x↔a∈⋃v
15 14 ralbii ⊢∀a∈A∃x∈va∈x↔∀a∈Aa∈⋃v
16 dfss3 ⊢A⊆⋃v↔∀a∈Aa∈⋃v
17 15 16 bitr4i ⊢∀a∈A∃x∈va∈x↔A⊆⋃v
18 17 anbi2i ⊢v⊆Y∧∀a∈A∃x∈va∈x↔v⊆Y∧A⊆⋃v
19 18 exbii ⊢∃vv⊆Y∧∀a∈A∃x∈va∈x↔∃vv⊆Y∧A⊆⋃v
20 10 19 sylib ⊢φ→∃vv⊆Y∧A⊆⋃v
21 vex ⊢v∈V
22 21 a1i ⊢v⊆Y→v∈V
23 id ⊢v⊆Y→v⊆Y
24 1 22 23 setrec1lem2 ⊢v⊆Y→⋃v∈Y
25 24 anim1i ⊢v⊆Y∧A⊆⋃v→⋃v∈Y∧A⊆⋃v
26 25 ancomd ⊢v⊆Y∧A⊆⋃v→A⊆⋃v∧⋃v∈Y
27 21 uniex ⊢⋃v∈V
28 sseq2 ⊢x=⋃v→A⊆x↔A⊆⋃v
29 eleq1 ⊢x=⋃v→x∈Y↔⋃v∈Y
30 28 29 anbi12d ⊢x=⋃v→A⊆x∧x∈Y↔A⊆⋃v∧⋃v∈Y
31 27 30 spcev ⊢A⊆⋃v∧⋃v∈Y→∃xA⊆x∧x∈Y
32 26 31 syl ⊢v⊆Y∧A⊆⋃v→∃xA⊆x∧x∈Y
33 32 exlimiv ⊢∃vv⊆Y∧A⊆⋃v→∃xA⊆x∧x∈Y
34 20 33 syl ⊢φ→∃xA⊆x∧x∈Y