Theorem setrec1lem4 50272

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

In the proof of setrec1 50273, 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 1854, making the antecedent of each line something more complicated than 𝜑. The proof of setrec1lem2 50270 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 22	. . . . . . . 8 ⊢ (𝑤 ⊆ 𝑋 → 𝑤 ⊆ 𝑋)
3		ssun1 4128	. . . . . . . 8 ⊢ 𝑋 ⊆ (𝑋 ∪ (𝐹‘𝐴))
4	2, 3	sstrdi 3946	. . . . . . 7 ⊢ (𝑤 ⊆ 𝑋 → 𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)))
5	4	imim1i 63	. . . . . 6 ⊢ ((𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)))
6	5	alimi 1830	. . . . 5 ⊢ (∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → ∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)))
7		setrec1lem4.5	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑌)
8		setrec1lem4.2	. . . . . . . . 9 ⊢ 𝑌 = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}
9	8, 7	setrec1lem1 50269	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∈ 𝑌 ↔ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧)))
10	7, 9	mpbid 234	. . . . . . 7 ⊢ (𝜑 → ∀𝑧(∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧))
11		sp 2217	. . . . . . 7 ⊢ (∀𝑧(∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧) → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧))
12	10, 11	syl 17	. . . . . 6 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧))
13		setrec1lem4.4	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ⊆ 𝑋)
14		sstr2 3941	. . . . . . . . 9 ⊢ (𝐴 ⊆ 𝑋 → (𝑋 ⊆ 𝑧 → 𝐴 ⊆ 𝑧))
15	13, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ⊆ 𝑧 → 𝐴 ⊆ 𝑧))
16	12, 15	syld 47	. . . . . . 7 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝐴 ⊆ 𝑧))
17		setrec1lem4.3	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ V)
18		sseq1 3959	. . . . . . . . . 10 ⊢ (𝑤 = 𝐴 → (𝑤 ⊆ 𝑋 ↔ 𝐴 ⊆ 𝑋))
19		sseq1 3959	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐴 → (𝑤 ⊆ 𝑧 ↔ 𝐴 ⊆ 𝑧))
20		fveq2 6862	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐴 → (𝐹‘𝑤) = (𝐹‘𝐴))
21	20	sseq1d 3965	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐴 → ((𝐹‘𝑤) ⊆ 𝑧 ↔ (𝐹‘𝐴) ⊆ 𝑧))
22	19, 21	imbi12d 346	. . . . . . . . . 10 ⊢ (𝑤 = 𝐴 → ((𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧) ↔ (𝐴 ⊆ 𝑧 → (𝐹‘𝐴) ⊆ 𝑧)))
23	18, 22	imbi12d 346	. . . . . . . . 9 ⊢ (𝑤 = 𝐴 → ((𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) ↔ (𝐴 ⊆ 𝑋 → (𝐴 ⊆ 𝑧 → (𝐹‘𝐴) ⊆ 𝑧))))
24	17, 23	spcdvw 50261	. . . . . . . 8 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝐴 ⊆ 𝑋 → (𝐴 ⊆ 𝑧 → (𝐹‘𝐴) ⊆ 𝑧))))
25	13, 24	mpid 44	. . . . . . 7 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝐴 ⊆ 𝑧 → (𝐹‘𝐴) ⊆ 𝑧)))
26	16, 25	mpdd 43	. . . . . 6 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝐹‘𝐴) ⊆ 𝑧))
27	12, 26	jcad 520	. . . . 5 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ⊆ 𝑧 ∧ (𝐹‘𝐴) ⊆ 𝑧)))
28	6, 27	syl5 34	. . . 4 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ⊆ 𝑧 ∧ (𝐹‘𝐴) ⊆ 𝑧)))
29		unss 4140	. . . 4 ⊢ ((𝑋 ⊆ 𝑧 ∧ (𝐹‘𝐴) ⊆ 𝑧) ↔ (𝑋 ∪ (𝐹‘𝐴)) ⊆ 𝑧)
30	28, 29	imbitrdi 253	. . 3 ⊢ (𝜑 → (∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ∪ (𝐹‘𝐴)) ⊆ 𝑧))
31	1, 30	alrimi 2247	. 2 ⊢ (𝜑 → ∀𝑧(∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ∪ (𝐹‘𝐴)) ⊆ 𝑧))
32		fvex 6875	. . . 4 ⊢ (𝐹‘𝐴) ∈ V
33		unexg 7721	. . . 4 ⊢ ((𝑋 ∈ 𝑌 ∧ (𝐹‘𝐴) ∈ V) → (𝑋 ∪ (𝐹‘𝐴)) ∈ V)
34	7, 32, 33	sylancl 595	. . 3 ⊢ (𝜑 → (𝑋 ∪ (𝐹‘𝐴)) ∈ V)
35	8, 34	setrec1lem1 50269	. 2 ⊢ (𝜑 → ((𝑋 ∪ (𝐹‘𝐴)) ∈ 𝑌 ↔ ∀𝑧(∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ∪ (𝐹‘𝐴)) ⊆ 𝑧)))
36	31, 35	mpbird 259	1 ⊢ (𝜑 → (𝑋 ∪ (𝐹‘𝐴)) ∈ 𝑌)

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1557   = wceq 1559  Ⅎwnf 1802   ∈ wcel 2141  {cab 2739  Vcvv 3453   ∪ cun 3900   ⊆ wss 3902  ‘cfv 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524

This theorem is referenced by:  setrec1  50273