Theorem setrec1lem4 50616

Description: Lemma for setrec1 50617. If 𝑋 is recursively generated by 𝐹, then so is 𝑋 ∪ (𝐹‘𝐴).

In the proof of setrec1 50617, the following is substituted for this theorem's 𝜑: (𝜑 ∧ (𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤 (𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) Therefore, we cannot declare 𝑧 to be a distinct variable from 𝜑, since we need it to appear as a bound variable in 𝜑. This theorem can be proven without the hypothesis Ⅎ𝑧𝜑, but the proof would be harder to read because theorems in deduction form would be interrupted by theorems like eximi 1868, making the antecedent of each line something more complicated than 𝜑. The proof of setrec1lem2 50614 could similarly be made easier to read by adding the hypothesis Ⅎ𝑧𝜑, but I had already finished the proof and decided to leave it as is. (Contributed by Emmett Weisz, 26-Nov-2020.) (New usage is discouraged.)

Hypotheses

Ref	Expression
setrec1lem4.1	⊢ Ⅎ𝑧𝜑
setrec1lem4.2	⊢ 𝑌 = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}
setrec1lem4.3	⊢ (𝜑 → 𝐴 ∈ V)
setrec1lem4.4	⊢ (𝜑 → 𝐴 ⊆ 𝑋)
setrec1lem4.5	⊢ (𝜑 → 𝑋 ∈ 𝑌)

Assertion

Ref	Expression
setrec1lem4	⊢ (𝜑 → (𝑋 ∪ (𝐹‘𝐴)) ∈ 𝑌)

Distinct variable groups:   𝑦,𝑤,𝑧,𝐴   𝑤,𝐹,𝑦,𝑧   𝑤,𝑋,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑦, 𝑧, 𝑤)   𝑌(𝑦, 𝑧, 𝑤)

Proof of Theorem setrec1lem4

Step	Hyp	Ref	Expression
1		setrec1lem4.1	. . 3 ⊢ Ⅎ𝑧𝜑
2		id 23	. . . . . . . 8 ⊢ (𝑤 ⊆ 𝑋 → 𝑤 ⊆ 𝑋)
3		ssun1 4124	. . . . . . . 8 ⊢ 𝑋 ⊆ (𝑋 ∪ (𝐹‘𝐴))
4	2, 3	sstrdi 3943	. . . . . . 7 ⊢ (𝑤 ⊆ 𝑋 → 𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)))
5	4	imim1i 64	. . . . . 6 ⊢ ((𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)))
6	5	alimi 1844	. . . . 5 ⊢ (∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → ∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)))
7		setrec1lem4.5	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑌)
8		setrec1lem4.2	. . . . . . . . 9 ⊢ 𝑌 = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}
9	8, 7	setrec1lem1 50613	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∈ 𝑌 ↔ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧)))
10	7, 9	mpbid 235	. . . . . . 7 ⊢ (𝜑 → ∀𝑧(∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧))
11		sp 2219	. . . . . . 7 ⊢ (∀𝑧(∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧) → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧))
12	10, 11	syl 18	. . . . . 6 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧))
13		setrec1lem4.4	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ⊆ 𝑋)
14		sstr2 3938	. . . . . . . . 9 ⊢ (𝐴 ⊆ 𝑋 → (𝑋 ⊆ 𝑧 → 𝐴 ⊆ 𝑧))
15	13, 14	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ⊆ 𝑧 → 𝐴 ⊆ 𝑧))
16	12, 15	syld 48	. . . . . . 7 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝐴 ⊆ 𝑧))
17		setrec1lem4.3	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ V)
18		sseq1 3956	. . . . . . . . . 10 ⊢ (𝑤 = 𝐴 → (𝑤 ⊆ 𝑋 ↔ 𝐴 ⊆ 𝑋))
19		sseq1 3956	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐴 → (𝑤 ⊆ 𝑧 ↔ 𝐴 ⊆ 𝑧))
20		fveq2 6878	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐴 → (𝐹‘𝑤) = (𝐹‘𝐴))
21	20	sseq1d 3962	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐴 → ((𝐹‘𝑤) ⊆ 𝑧 ↔ (𝐹‘𝐴) ⊆ 𝑧))
22	19, 21	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑤 = 𝐴 → ((𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧) ↔ (𝐴 ⊆ 𝑧 → (𝐹‘𝐴) ⊆ 𝑧)))
23	18, 22	imbi12d 347	. . . . . . . . 9 ⊢ (𝑤 = 𝐴 → ((𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) ↔ (𝐴 ⊆ 𝑋 → (𝐴 ⊆ 𝑧 → (𝐹‘𝐴) ⊆ 𝑧))))
24	17, 23	spcdvw 50605	. . . . . . . 8 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝐴 ⊆ 𝑋 → (𝐴 ⊆ 𝑧 → (𝐹‘𝐴) ⊆ 𝑧))))
25	13, 24	mpid 45	. . . . . . 7 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝐴 ⊆ 𝑧 → (𝐹‘𝐴) ⊆ 𝑧)))
26	16, 25	mpdd 44	. . . . . 6 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝐹‘𝐴) ⊆ 𝑧))
27	12, 26	jcad 522	. . . . 5 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ⊆ 𝑧 ∧ (𝐹‘𝐴) ⊆ 𝑧)))
28	6, 27	syl5 35	. . . 4 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ⊆ 𝑧 ∧ (𝐹‘𝐴) ⊆ 𝑧)))
29		unss 4136	. . . 4 ⊢ ((𝑋 ⊆ 𝑧 ∧ (𝐹‘𝐴) ⊆ 𝑧) ↔ (𝑋 ∪ (𝐹‘𝐴)) ⊆ 𝑧)
30	28, 29	imbitrdi 254	. . 3 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ∪ (𝐹‘𝐴)) ⊆ 𝑧))
31	1, 30	alrimi 2249	. 2 ⊢ (𝜑 → ∀𝑧(∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ∪ (𝐹‘𝐴)) ⊆ 𝑧))
32		fvex 6891	. . . 4 ⊢ (𝐹‘𝐴) ∈ V
33		unexg 7745	. . . 4 ⊢ ((𝑋 ∈ 𝑌 ∧ (𝐹‘𝐴) ∈ V) → (𝑋 ∪ (𝐹‘𝐴)) ∈ V)
34	7, 32, 33	sylancl 598	. . 3 ⊢ (𝜑 → (𝑋 ∪ (𝐹‘𝐴)) ∈ V)
35	8, 34	setrec1lem1 50613	. 2 ⊢ (𝜑 → ((𝑋 ∪ (𝐹‘𝐴)) ∈ 𝑌 ↔ ∀𝑧(∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ∪ (𝐹‘𝐴)) ⊆ 𝑧)))
36	31, 35	mpbird 260	1 ⊢ (𝜑 → (𝑋 ∪ (𝐹‘𝐴)) ∈ 𝑌)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2145  {cab 2738  Vcvv 3450   ∪ cun 3897   ⊆ wss 3899  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541

This theorem is used by:  setrec1  50617