Proof of Theorem frecabex
Step | Hyp | Ref
| Expression |
1 | | omex 4259 |
. . . 4
⊢ 𝜔
∈ V |
2 | | simpr 103 |
. . . . . . 7
⊢ ((dom
𝑆 = suc 𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚))) → x ∈ (𝐹‘(𝑆‘𝑚))) |
3 | 2 | abssi 3009 |
. . . . . 6
⊢ {x ∣ (dom 𝑆 = suc 𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚)))} ⊆ (𝐹‘(𝑆‘𝑚)) |
4 | | frecabex.sex |
. . . . . . . 8
⊢ (φ → 𝑆 ∈ 𝑉) |
5 | | vex 2554 |
. . . . . . . 8
⊢ 𝑚 ∈ V |
6 | | fvexg 5137 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑚 ∈ V) → (𝑆‘𝑚) ∈
V) |
7 | 4, 5, 6 | sylancl 392 |
. . . . . . 7
⊢ (φ → (𝑆‘𝑚) ∈
V) |
8 | | frecabex.fvex |
. . . . . . 7
⊢ (φ → ∀y(𝐹‘y) ∈
V) |
9 | | fveq2 5121 |
. . . . . . . . 9
⊢ (y = (𝑆‘𝑚) → (𝐹‘y) = (𝐹‘(𝑆‘𝑚))) |
10 | 9 | eleq1d 2103 |
. . . . . . . 8
⊢ (y = (𝑆‘𝑚) → ((𝐹‘y) ∈ V ↔
(𝐹‘(𝑆‘𝑚)) ∈
V)) |
11 | 10 | spcgv 2634 |
. . . . . . 7
⊢ ((𝑆‘𝑚) ∈ V
→ (∀y(𝐹‘y) ∈ V →
(𝐹‘(𝑆‘𝑚)) ∈
V)) |
12 | 7, 8, 11 | sylc 56 |
. . . . . 6
⊢ (φ → (𝐹‘(𝑆‘𝑚)) ∈
V) |
13 | | ssexg 3887 |
. . . . . 6
⊢
(({x ∣ (dom 𝑆 = suc 𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚)))} ⊆ (𝐹‘(𝑆‘𝑚)) ∧ (𝐹‘(𝑆‘𝑚)) ∈ V)
→ {x ∣ (dom 𝑆 = suc 𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚)))} ∈
V) |
14 | 3, 12, 13 | sylancr 393 |
. . . . 5
⊢ (φ → {x ∣ (dom 𝑆 = suc 𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚)))} ∈
V) |
15 | 14 | ralrimivw 2387 |
. . . 4
⊢ (φ → ∀𝑚 ∈
𝜔 {x ∣ (dom 𝑆 = suc 𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚)))} ∈
V) |
16 | | abrexex2g 5689 |
. . . 4
⊢
((𝜔 ∈ V ∧ ∀𝑚 ∈ 𝜔 {x
∣ (dom 𝑆 = suc 𝑚 ∧
x ∈
(𝐹‘(𝑆‘𝑚)))} ∈ V)
→ {x ∣ ∃𝑚 ∈
𝜔 (dom 𝑆 = suc
𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚)))} ∈
V) |
17 | 1, 15, 16 | sylancr 393 |
. . 3
⊢ (φ → {x ∣ ∃𝑚 ∈ 𝜔 (dom 𝑆 = suc 𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚)))} ∈
V) |
18 | | simpr 103 |
. . . . 5
⊢ ((dom
𝑆 = ∅ ∧ x ∈ A) →
x ∈
A) |
19 | 18 | abssi 3009 |
. . . 4
⊢ {x ∣ (dom 𝑆 = ∅ ∧ x ∈ A)} ⊆
A |
20 | | frecabex.aex |
. . . 4
⊢ (φ → A ∈ 𝑊) |
21 | | ssexg 3887 |
. . . 4
⊢
(({x ∣ (dom 𝑆 = ∅ ∧ x ∈ A)} ⊆
A ∧
A ∈ 𝑊) → {x ∣ (dom 𝑆 = ∅ ∧ x ∈ A)} ∈ V) |
22 | 19, 20, 21 | sylancr 393 |
. . 3
⊢ (φ → {x ∣ (dom 𝑆 = ∅ ∧ x ∈ A)} ∈ V) |
23 | 17, 22 | jca 290 |
. 2
⊢ (φ → ({x ∣ ∃𝑚 ∈ 𝜔 (dom 𝑆 = suc 𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚)))} ∈ V
∧ {x
∣ (dom 𝑆 = ∅
∧ x ∈ A)} ∈ V)) |
24 | | unexb 4143 |
. . 3
⊢
(({x ∣ ∃𝑚 ∈
𝜔 (dom 𝑆 = suc
𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚)))} ∈ V
∧ {x
∣ (dom 𝑆 = ∅
∧ x ∈ A)} ∈ V) ↔ ({x
∣ ∃𝑚 ∈
𝜔 (dom 𝑆 = suc
𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚)))} ∪ {x ∣ (dom 𝑆 = ∅ ∧ x ∈ A)}) ∈ V) |
25 | | unab 3198 |
. . . 4
⊢
({x ∣ ∃𝑚 ∈
𝜔 (dom 𝑆 = suc
𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚)))} ∪ {x ∣ (dom 𝑆 = ∅ ∧ x ∈ A)}) =
{x ∣ (∃𝑚 ∈
𝜔 (dom 𝑆 = suc
𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚))) ∨ (dom
𝑆 = ∅ ∧ x ∈ A))} |
26 | 25 | eleq1i 2100 |
. . 3
⊢
(({x ∣ ∃𝑚 ∈
𝜔 (dom 𝑆 = suc
𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚)))} ∪ {x ∣ (dom 𝑆 = ∅ ∧ x ∈ A)}) ∈ V ↔ {x
∣ (∃𝑚 ∈
𝜔 (dom 𝑆 = suc
𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚))) ∨ (dom
𝑆 = ∅ ∧ x ∈ A))} ∈ V) |
27 | 24, 26 | bitri 173 |
. 2
⊢
(({x ∣ ∃𝑚 ∈
𝜔 (dom 𝑆 = suc
𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚)))} ∈ V
∧ {x
∣ (dom 𝑆 = ∅
∧ x ∈ A)} ∈ V) ↔ {x
∣ (∃𝑚 ∈
𝜔 (dom 𝑆 = suc
𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚))) ∨ (dom
𝑆 = ∅ ∧ x ∈ A))} ∈ V) |
28 | 23, 27 | sylib 127 |
1
⊢ (φ → {x ∣ (∃𝑚 ∈ 𝜔 (dom 𝑆 = suc 𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚))) ∨ (dom
𝑆 = ∅ ∧ x ∈ A))} ∈ V) |