Proof of Theorem setrec1lem4
| Step | Hyp | Ref
| Expression |
| 1 | | setrec1lem4.1 |
. . 3
⊢
Ⅎ𝑧𝜑 |
| 2 | | id 22 |
. . . . . . . 8
⊢ (𝑤 ⊆ 𝑋 → 𝑤 ⊆ 𝑋) |
| 3 | | ssun1 4178 |
. . . . . . . 8
⊢ 𝑋 ⊆ (𝑋 ∪ (𝐹‘𝐴)) |
| 4 | 2, 3 | sstrdi 3996 |
. . . . . . 7
⊢ (𝑤 ⊆ 𝑋 → 𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴))) |
| 5 | 4 | imim1i 63 |
. . . . . 6
⊢ ((𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧))) |
| 6 | 5 | alimi 1811 |
. . . . 5
⊢
(∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → ∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧))) |
| 7 | | setrec1lem4.5 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝑌) |
| 8 | | setrec1lem4.2 |
. . . . . . . . 9
⊢ 𝑌 = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)} |
| 9 | 8, 7 | setrec1lem1 49206 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ 𝑌 ↔ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧))) |
| 10 | 7, 9 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → ∀𝑧(∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧)) |
| 11 | | sp 2183 |
. . . . . . 7
⊢
(∀𝑧(∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧) → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧)) |
| 12 | 10, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑋 ⊆ 𝑧)) |
| 13 | | setrec1lem4.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ 𝑋) |
| 14 | | sstr2 3990 |
. . . . . . . . 9
⊢ (𝐴 ⊆ 𝑋 → (𝑋 ⊆ 𝑧 → 𝐴 ⊆ 𝑧)) |
| 15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ⊆ 𝑧 → 𝐴 ⊆ 𝑧)) |
| 16 | 12, 15 | syld 47 |
. . . . . . 7
⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝐴 ⊆ 𝑧)) |
| 17 | | setrec1lem4.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ V) |
| 18 | | sseq1 4009 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐴 → (𝑤 ⊆ 𝑋 ↔ 𝐴 ⊆ 𝑋)) |
| 19 | | sseq1 4009 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝐴 → (𝑤 ⊆ 𝑧 ↔ 𝐴 ⊆ 𝑧)) |
| 20 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝐴 → (𝐹‘𝑤) = (𝐹‘𝐴)) |
| 21 | 20 | sseq1d 4015 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝐴 → ((𝐹‘𝑤) ⊆ 𝑧 ↔ (𝐹‘𝐴) ⊆ 𝑧)) |
| 22 | 19, 21 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐴 → ((𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧) ↔ (𝐴 ⊆ 𝑧 → (𝐹‘𝐴) ⊆ 𝑧))) |
| 23 | 18, 22 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑤 = 𝐴 → ((𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) ↔ (𝐴 ⊆ 𝑋 → (𝐴 ⊆ 𝑧 → (𝐹‘𝐴) ⊆ 𝑧)))) |
| 24 | 17, 23 | spcdvw 49198 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝐴 ⊆ 𝑋 → (𝐴 ⊆ 𝑧 → (𝐹‘𝐴) ⊆ 𝑧)))) |
| 25 | 13, 24 | mpid 44 |
. . . . . . 7
⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝐴 ⊆ 𝑧 → (𝐹‘𝐴) ⊆ 𝑧))) |
| 26 | 16, 25 | mpdd 43 |
. . . . . 6
⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝐹‘𝐴) ⊆ 𝑧)) |
| 27 | 12, 26 | jcad 512 |
. . . . 5
⊢ (𝜑 → (∀𝑤(𝑤 ⊆ 𝑋 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ⊆ 𝑧 ∧ (𝐹‘𝐴) ⊆ 𝑧))) |
| 28 | 6, 27 | syl5 34 |
. . . 4
⊢ (𝜑 → (∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ⊆ 𝑧 ∧ (𝐹‘𝐴) ⊆ 𝑧))) |
| 29 | | unss 4190 |
. . . 4
⊢ ((𝑋 ⊆ 𝑧 ∧ (𝐹‘𝐴) ⊆ 𝑧) ↔ (𝑋 ∪ (𝐹‘𝐴)) ⊆ 𝑧) |
| 30 | 28, 29 | imbitrdi 251 |
. . 3
⊢ (𝜑 → (∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ∪ (𝐹‘𝐴)) ⊆ 𝑧)) |
| 31 | 1, 30 | alrimi 2213 |
. 2
⊢ (𝜑 → ∀𝑧(∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ∪ (𝐹‘𝐴)) ⊆ 𝑧)) |
| 32 | | fvex 6919 |
. . . 4
⊢ (𝐹‘𝐴) ∈ V |
| 33 | | unexg 7763 |
. . . 4
⊢ ((𝑋 ∈ 𝑌 ∧ (𝐹‘𝐴) ∈ V) → (𝑋 ∪ (𝐹‘𝐴)) ∈ V) |
| 34 | 7, 32, 33 | sylancl 586 |
. . 3
⊢ (𝜑 → (𝑋 ∪ (𝐹‘𝐴)) ∈ V) |
| 35 | 8, 34 | setrec1lem1 49206 |
. 2
⊢ (𝜑 → ((𝑋 ∪ (𝐹‘𝐴)) ∈ 𝑌 ↔ ∀𝑧(∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹‘𝐴)) → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → (𝑋 ∪ (𝐹‘𝐴)) ⊆ 𝑧))) |
| 36 | 31, 35 | mpbird 257 |
1
⊢ (𝜑 → (𝑋 ∪ (𝐹‘𝐴)) ∈ 𝑌) |