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 ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
setrec1lem3.2 ⊢ φ → A ∈ V
setrec1lem3.3 ⊢ φ → ∀ a ∈ A ∃ x a ∈ x ∧ x ∈ Y
Assertion setrec1lem3 ⊢ φ → ∃ x A ⊆ x ∧ x ∈ Y

Proof

Step Hyp Ref Expression
1 setrec1lem3.1 ⊢ Y = y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
2 setrec1lem3.2 ⊢ φ → A ∈ V
3 setrec1lem3.3 ⊢ φ → ∀ a ∈ A ∃ x a ∈ x ∧ x ∈ Y
4 exancom ⊢ ∃ x a ∈ x ∧ x ∈ Y ↔ ∃ x x ∈ Y ∧ a ∈ x
5 4 ralbii ⊢ ∀ a ∈ A ∃ x a ∈ x ∧ x ∈ Y ↔ ∀ a ∈ A ∃ x x ∈ Y ∧ a ∈ x
6 3 5 sylib ⊢ φ → ∀ a ∈ A ∃ x x ∈ Y ∧ a ∈ x
7 df-rex ⊢ ∃ x ∈ Y a ∈ x ↔ ∃ x x ∈ Y ∧ a ∈ x
8 7 ralbii ⊢ ∀ a ∈ A ∃ x ∈ Y a ∈ x ↔ ∀ a ∈ A ∃ x x ∈ Y ∧ a ∈ x
9 6 8 sylibr ⊢ φ → ∀ a ∈ A ∃ x ∈ Y a ∈ x
10 2 9 bnd2d ⊢ φ → ∃ v v ⊆ Y ∧ ∀ a ∈ A ∃ x ∈ v a ∈ x
11 exancom ⊢ ∃ x x ∈ v ∧ a ∈ x ↔ ∃ x a ∈ x ∧ x ∈ v
12 df-rex ⊢ ∃ x ∈ v a ∈ x ↔ ∃ x x ∈ v ∧ a ∈ x
13 eluni ⊢ a ∈ ⋃ v ↔ ∃ x a ∈ x ∧ x ∈ v
14 11 12 13 3bitr4i ⊢ ∃ x ∈ v a ∈ x ↔ a ∈ ⋃ v
15 14 ralbii ⊢ ∀ a ∈ A ∃ x ∈ v a ∈ x ↔ ∀ a ∈ A a ∈ ⋃ v
16 dfss3 ⊢ A ⊆ ⋃ v ↔ ∀ a ∈ A a ∈ ⋃ v
17 15 16 bitr4i ⊢ ∀ a ∈ A ∃ x ∈ v a ∈ x ↔ A ⊆ ⋃ v
18 17 anbi2i ⊢ v ⊆ Y ∧ ∀ a ∈ A ∃ x ∈ v a ∈ x ↔ v ⊆ Y ∧ A ⊆ ⋃ v
19 18 exbii ⊢ ∃ v v ⊆ Y ∧ ∀ a ∈ A ∃ x ∈ v a ∈ x ↔ ∃ v v ⊆ Y ∧ A ⊆ ⋃ v
20 10 19 sylib ⊢ φ → ∃ v v ⊆ 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 → ∃ x A ⊆ x ∧ x ∈ Y
32 26 31 syl ⊢ v ⊆ Y ∧ A ⊆ ⋃ v → ∃ x A ⊆ x ∧ x ∈ Y
33 32 exlimiv ⊢ ∃ v v ⊆ Y ∧ A ⊆ ⋃ v → ∃ x A ⊆ x ∧ x ∈ Y
34 20 33 syl ⊢ φ → ∃ x A ⊆ x ∧ x ∈ Y