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	⊢ 𝑌 = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) }
	setrec1lem2.2	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	setrec1lem2.3	⊢ ( 𝜑 → 𝑋 ⊆ 𝑌 )
Assertion	setrec1lem2	⊢ ( 𝜑 → ∪ 𝑋 ∈ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		setrec1lem2.1	⊢ 𝑌 = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) }
2		setrec1lem2.2	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
3		setrec1lem2.3	⊢ ( 𝜑 → 𝑋 ⊆ 𝑌 )
4		dfss3	⊢ ( 𝑋 ⊆ 𝑌 ↔ ∀ 𝑥 ∈ 𝑋 𝑥 ∈ 𝑌 )
5	3 4	sylib	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝑥 ∈ 𝑌 )
6		vex	⊢ 𝑥 ∈ V
7	6	a1i	⊢ ( 𝜑 → 𝑥 ∈ V )
8	1 7	setrec1lem1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑌 ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) ) )
9	8	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 𝑥 ∈ 𝑌 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) ) )
10	5 9	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) )
11		ralcom4	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) )
12	10 11	sylib	⊢ ( 𝜑 → ∀ 𝑧 ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) )
13		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 )
14		nfv	⊢ Ⅎ 𝑥 ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) )
15		rsp	⊢ ( ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) → ( 𝑥 ∈ 𝑋 → ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) ) )
16		elssuni	⊢ ( 𝑥 ∈ 𝑋 → 𝑥 ⊆ ∪ 𝑋 )
17		sstr2	⊢ ( 𝑤 ⊆ 𝑥 → ( 𝑥 ⊆ ∪ 𝑋 → 𝑤 ⊆ ∪ 𝑋 ) )
18	16 17	syl5com	⊢ ( 𝑥 ∈ 𝑋 → ( 𝑤 ⊆ 𝑥 → 𝑤 ⊆ ∪ 𝑋 ) )
19	18	imim1d	⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) ) )
20	19	alimdv	⊢ ( 𝑥 ∈ 𝑋 → ( ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) ) )
21	20	imim1d	⊢ ( 𝑥 ∈ 𝑋 → ( ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) → ( ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) ) )
22	15 21	sylcom	⊢ ( ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) → ( 𝑥 ∈ 𝑋 → ( ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) ) )
23	22	com23	⊢ ( ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) → ( ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ( 𝑥 ∈ 𝑋 → 𝑥 ⊆ 𝑧 ) ) )
24	13 14 23	ralrimd	⊢ ( ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) → ( ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ∀ 𝑥 ∈ 𝑋 𝑥 ⊆ 𝑧 ) )
25	24	alimi	⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑥 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑥 ⊆ 𝑧 ) → ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ∀ 𝑥 ∈ 𝑋 𝑥 ⊆ 𝑧 ) )
26	12 25	syl	⊢ ( 𝜑 → ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ∀ 𝑥 ∈ 𝑋 𝑥 ⊆ 𝑧 ) )
27		unissb	⊢ ( ∪ 𝑋 ⊆ 𝑧 ↔ ∀ 𝑥 ∈ 𝑋 𝑥 ⊆ 𝑧 )
28	27	imbi2i	⊢ ( ( ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ∪ 𝑋 ⊆ 𝑧 ) ↔ ( ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ∀ 𝑥 ∈ 𝑋 𝑥 ⊆ 𝑧 ) )
29	28	albii	⊢ ( ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ∪ 𝑋 ⊆ 𝑧 ) ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ∀ 𝑥 ∈ 𝑋 𝑥 ⊆ 𝑧 ) )
30	26 29	sylibr	⊢ ( 𝜑 → ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ∪ 𝑋 ⊆ 𝑧 ) )
31	2	uniexd	⊢ ( 𝜑 → ∪ 𝑋 ∈ V )
32	1 31	setrec1lem1	⊢ ( 𝜑 → ( ∪ 𝑋 ∈ 𝑌 ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ ∪ 𝑋 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → ∪ 𝑋 ⊆ 𝑧 ) ) )
33	30 32	mpbird	⊢ ( 𝜑 → ∪ 𝑋 ∈ 𝑌 )