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	⊢ 𝑌 = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) }
	setrec1lem3.2	⊢ ( 𝜑 → 𝐴 ∈ V )
	setrec1lem3.3	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ( 𝑎 ∈ 𝑥 ∧ 𝑥 ∈ 𝑌 ) )
Assertion	setrec1lem3	⊢ ( 𝜑 → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		setrec1lem3.1	⊢ 𝑌 = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) }
2		setrec1lem3.2	⊢ ( 𝜑 → 𝐴 ∈ V )
3		setrec1lem3.3	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ( 𝑎 ∈ 𝑥 ∧ 𝑥 ∈ 𝑌 ) )
4		exancom	⊢ ( ∃ 𝑥 ( 𝑎 ∈ 𝑥 ∧ 𝑥 ∈ 𝑌 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝑥 ) )
5	4	ralbii	⊢ ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ( 𝑎 ∈ 𝑥 ∧ 𝑥 ∈ 𝑌 ) ↔ ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝑥 ) )
6	3 5	sylib	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝑥 ) )
7		df-rex	⊢ ( ∃ 𝑥 ∈ 𝑌 𝑎 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝑥 ) )
8	7	ralbii	⊢ ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝑌 𝑎 ∈ 𝑥 ↔ ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ( 𝑥 ∈ 𝑌 ∧ 𝑎 ∈ 𝑥 ) )
9	6 8	sylibr	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝑌 𝑎 ∈ 𝑥 )
10	2 9	bnd2d	⊢ ( 𝜑 → ∃ 𝑣 ( 𝑣 ⊆ 𝑌 ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝑣 𝑎 ∈ 𝑥 ) )
11		exancom	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝑎 ∈ 𝑥 ) ↔ ∃ 𝑥 ( 𝑎 ∈ 𝑥 ∧ 𝑥 ∈ 𝑣 ) )
12		df-rex	⊢ ( ∃ 𝑥 ∈ 𝑣 𝑎 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝑎 ∈ 𝑥 ) )
13		eluni	⊢ ( 𝑎 ∈ ∪ 𝑣 ↔ ∃ 𝑥 ( 𝑎 ∈ 𝑥 ∧ 𝑥 ∈ 𝑣 ) )
14	11 12 13	3bitr4i	⊢ ( ∃ 𝑥 ∈ 𝑣 𝑎 ∈ 𝑥 ↔ 𝑎 ∈ ∪ 𝑣 )
15	14	ralbii	⊢ ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝑣 𝑎 ∈ 𝑥 ↔ ∀ 𝑎 ∈ 𝐴 𝑎 ∈ ∪ 𝑣 )
16		dfss3	⊢ ( 𝐴 ⊆ ∪ 𝑣 ↔ ∀ 𝑎 ∈ 𝐴 𝑎 ∈ ∪ 𝑣 )
17	15 16	bitr4i	⊢ ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝑣 𝑎 ∈ 𝑥 ↔ 𝐴 ⊆ ∪ 𝑣 )
18	17	anbi2i	⊢ ( ( 𝑣 ⊆ 𝑌 ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝑣 𝑎 ∈ 𝑥 ) ↔ ( 𝑣 ⊆ 𝑌 ∧ 𝐴 ⊆ ∪ 𝑣 ) )
19	18	exbii	⊢ ( ∃ 𝑣 ( 𝑣 ⊆ 𝑌 ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝑣 𝑎 ∈ 𝑥 ) ↔ ∃ 𝑣 ( 𝑣 ⊆ 𝑌 ∧ 𝐴 ⊆ ∪ 𝑣 ) )
20	10 19	sylib	⊢ ( 𝜑 → ∃ 𝑣 ( 𝑣 ⊆ 𝑌 ∧ 𝐴 ⊆ ∪ 𝑣 ) )
21		vex	⊢ 𝑣 ∈ V
22	21	a1i	⊢ ( 𝑣 ⊆ 𝑌 → 𝑣 ∈ V )
23		id	⊢ ( 𝑣 ⊆ 𝑌 → 𝑣 ⊆ 𝑌 )
24	1 22 23	setrec1lem2	⊢ ( 𝑣 ⊆ 𝑌 → ∪ 𝑣 ∈ 𝑌 )
25	24	anim1i	⊢ ( ( 𝑣 ⊆ 𝑌 ∧ 𝐴 ⊆ ∪ 𝑣 ) → ( ∪ 𝑣 ∈ 𝑌 ∧ 𝐴 ⊆ ∪ 𝑣 ) )
26	25	ancomd	⊢ ( ( 𝑣 ⊆ 𝑌 ∧ 𝐴 ⊆ ∪ 𝑣 ) → ( 𝐴 ⊆ ∪ 𝑣 ∧ ∪ 𝑣 ∈ 𝑌 ) )
27	21	uniex	⊢ ∪ 𝑣 ∈ V
28		sseq2	⊢ ( 𝑥 = ∪ 𝑣 → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ∪ 𝑣 ) )
29		eleq1	⊢ ( 𝑥 = ∪ 𝑣 → ( 𝑥 ∈ 𝑌 ↔ ∪ 𝑣 ∈ 𝑌 ) )
30	28 29	anbi12d	⊢ ( 𝑥 = ∪ 𝑣 → ( ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ 𝑌 ) ↔ ( 𝐴 ⊆ ∪ 𝑣 ∧ ∪ 𝑣 ∈ 𝑌 ) ) )
31	27 30	spcev	⊢ ( ( 𝐴 ⊆ ∪ 𝑣 ∧ ∪ 𝑣 ∈ 𝑌 ) → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ 𝑌 ) )
32	26 31	syl	⊢ ( ( 𝑣 ⊆ 𝑌 ∧ 𝐴 ⊆ ∪ 𝑣 ) → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ 𝑌 ) )
33	32	exlimiv	⊢ ( ∃ 𝑣 ( 𝑣 ⊆ 𝑌 ∧ 𝐴 ⊆ ∪ 𝑣 ) → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ 𝑌 ) )
34	20 33	syl	⊢ ( 𝜑 → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ 𝑌 ) )