Step | Hyp | Ref
| Expression |
1 | | dmuni 5256 |
. . . 4
⊢ dom ∪ 𝐶 =
∪ 𝑧 ∈ 𝐶 dom 𝑧 |
2 | 1 | eleq2i 2680 |
. . 3
⊢ (𝑋 ∈ dom ∪ 𝐶
↔ 𝑋 ∈ ∪ 𝑧 ∈ 𝐶 dom 𝑧) |
3 | | eliun 4460 |
. . 3
⊢ (𝑋 ∈ ∪ 𝑧 ∈ 𝐶 dom 𝑧 ↔ ∃𝑧 ∈ 𝐶 𝑋 ∈ dom 𝑧) |
4 | 2, 3 | bitri 263 |
. 2
⊢ (𝑋 ∈ dom ∪ 𝐶
↔ ∃𝑧 ∈
𝐶 𝑋 ∈ dom 𝑧) |
5 | | ssel2 3563 |
. . . . 5
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ 𝐵) |
6 | | frrlem5.3 |
. . . . . . . 8
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} |
7 | 6 | frrlem1 31024 |
. . . . . . 7
⊢ 𝐵 = {𝑧 ∣ ∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤 ⊆ 𝐴 ∧ ∀𝑡 ∈ 𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡 ∈ 𝑤 (𝑧‘𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))))} |
8 | 7 | abeq2i 2722 |
. . . . . 6
⊢ (𝑧 ∈ 𝐵 ↔ ∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤 ⊆ 𝐴 ∧ ∀𝑡 ∈ 𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡 ∈ 𝑤 (𝑧‘𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))))) |
9 | | fndm 5904 |
. . . . . . . . 9
⊢ (𝑧 Fn 𝑤 → dom 𝑧 = 𝑤) |
10 | | predeq3 5601 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑋 → Pred(𝑅, 𝐴, 𝑡) = Pred(𝑅, 𝐴, 𝑋)) |
11 | 10 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑋 → (Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤)) |
12 | 11 | rspccv 3279 |
. . . . . . . . . . 11
⊢
(∀𝑡 ∈
𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 → (𝑋 ∈ 𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤)) |
13 | 12 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝑤 ⊆ 𝐴 ∧ ∀𝑡 ∈ 𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡 ∈ 𝑤 (𝑧‘𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ 𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤)) |
14 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (dom
𝑧 = 𝑤 → (𝑋 ∈ dom 𝑧 ↔ 𝑋 ∈ 𝑤)) |
15 | | sseq2 3590 |
. . . . . . . . . . 11
⊢ (dom
𝑧 = 𝑤 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤)) |
16 | 14, 15 | imbi12d 333 |
. . . . . . . . . 10
⊢ (dom
𝑧 = 𝑤 → ((𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) ↔ (𝑋 ∈ 𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))) |
17 | 13, 16 | syl5ibr 235 |
. . . . . . . . 9
⊢ (dom
𝑧 = 𝑤 → ((𝑤 ⊆ 𝐴 ∧ ∀𝑡 ∈ 𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡 ∈ 𝑤 (𝑧‘𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))) |
18 | 9, 17 | syl 17 |
. . . . . . . 8
⊢ (𝑧 Fn 𝑤 → ((𝑤 ⊆ 𝐴 ∧ ∀𝑡 ∈ 𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡 ∈ 𝑤 (𝑧‘𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))) |
19 | 18 | imp 444 |
. . . . . . 7
⊢ ((𝑧 Fn 𝑤 ∧ (𝑤 ⊆ 𝐴 ∧ ∀𝑡 ∈ 𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡 ∈ 𝑤 (𝑧‘𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡))))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)) |
20 | 19 | exlimiv 1845 |
. . . . . 6
⊢
(∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤 ⊆ 𝐴 ∧ ∀𝑡 ∈ 𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡 ∈ 𝑤 (𝑧‘𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡))))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)) |
21 | 8, 20 | sylbi 206 |
. . . . 5
⊢ (𝑧 ∈ 𝐵 → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)) |
22 | 5, 21 | syl 17 |
. . . 4
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)) |
23 | | dmeq 5246 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → dom 𝑤 = dom 𝑧) |
24 | 23 | sseq2d 3596 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)) |
25 | 24 | rspcev 3282 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → ∃𝑤 ∈ 𝐶 Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤) |
26 | | ssiun 4498 |
. . . . . . . 8
⊢
(∃𝑤 ∈
𝐶 Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ ∪ 𝑤 ∈ 𝐶 dom 𝑤) |
27 | 25, 26 | syl 17 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → Pred(𝑅, 𝐴, 𝑋) ⊆ ∪ 𝑤 ∈ 𝐶 dom 𝑤) |
28 | | dmuni 5256 |
. . . . . . 7
⊢ dom ∪ 𝐶 =
∪ 𝑤 ∈ 𝐶 dom 𝑤 |
29 | 27, 28 | syl6sseqr 3615 |
. . . . . 6
⊢ ((𝑧 ∈ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → Pred(𝑅, 𝐴, 𝑋) ⊆ dom ∪
𝐶) |
30 | 29 | ex 449 |
. . . . 5
⊢ (𝑧 ∈ 𝐶 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom ∪
𝐶)) |
31 | 30 | adantl 481 |
. . . 4
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑧 ∈ 𝐶) → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom ∪
𝐶)) |
32 | 22, 31 | syld 46 |
. . 3
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom ∪
𝐶)) |
33 | 32 | rexlimdva 3013 |
. 2
⊢ (𝐶 ⊆ 𝐵 → (∃𝑧 ∈ 𝐶 𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom ∪
𝐶)) |
34 | 4, 33 | syl5bi 231 |
1
⊢ (𝐶 ⊆ 𝐵 → (𝑋 ∈ dom ∪
𝐶 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom ∪
𝐶)) |