Step | Hyp | Ref
| Expression |
1 | | dmuni 5472 |
. . . 4
⊢ dom ∪ 𝐶 =
∪ 𝑧 ∈ 𝐶 dom 𝑧 |
2 | 1 | eleq2i 2842 |
. . 3
⊢ (𝑋 ∈ dom ∪ 𝐶
↔ 𝑋 ∈ ∪ 𝑧 ∈ 𝐶 dom 𝑧) |
3 | | eliun 4658 |
. . 3
⊢ (𝑋 ∈ ∪ 𝑧 ∈ 𝐶 dom 𝑧 ↔ ∃𝑧 ∈ 𝐶 𝑋 ∈ dom 𝑧) |
4 | 2, 3 | bitri 264 |
. 2
⊢ (𝑋 ∈ dom ∪ 𝐶
↔ ∃𝑧 ∈
𝐶 𝑋 ∈ dom 𝑧) |
5 | | ssel2 3747 |
. . . . 5
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ 𝐵) |
6 | | frrlem5.3 |
. . . . . . . 8
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} |
7 | 6 | frrlem1 32117 |
. . . . . . 7
⊢ 𝐵 = {𝑧 ∣ ∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤 ⊆ 𝐴 ∧ ∀𝑡 ∈ 𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡 ∈ 𝑤 (𝑧‘𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡))))} |
8 | 7 | abeq2i 2884 |
. . . . . 6
⊢ (𝑧 ∈ 𝐵 ↔ ∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤 ⊆ 𝐴 ∧ ∀𝑡 ∈ 𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡 ∈ 𝑤 (𝑧‘𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡))))) |
9 | | predeq3 5827 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑋 → Pred(𝑅, 𝐴, 𝑡) = Pred(𝑅, 𝐴, 𝑋)) |
10 | 9 | sseq1d 3781 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑋 → (Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤)) |
11 | 10 | rspccv 3457 |
. . . . . . . . . 10
⊢
(∀𝑡 ∈
𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 → (𝑋 ∈ 𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤)) |
12 | 11 | ad2antlr 706 |
. . . . . . . . 9
⊢ (((𝑤 ⊆ 𝐴 ∧ ∀𝑡 ∈ 𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡 ∈ 𝑤 (𝑧‘𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ 𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤)) |
13 | | fndm 6130 |
. . . . . . . . . . 11
⊢ (𝑧 Fn 𝑤 → dom 𝑧 = 𝑤) |
14 | 13 | eleq2d 2836 |
. . . . . . . . . 10
⊢ (𝑧 Fn 𝑤 → (𝑋 ∈ dom 𝑧 ↔ 𝑋 ∈ 𝑤)) |
15 | 13 | sseq2d 3782 |
. . . . . . . . . 10
⊢ (𝑧 Fn 𝑤 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤)) |
16 | 14, 15 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑧 Fn 𝑤 → ((𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) ↔ (𝑋 ∈ 𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))) |
17 | 12, 16 | syl5ibr 236 |
. . . . . . . 8
⊢ (𝑧 Fn 𝑤 → (((𝑤 ⊆ 𝐴 ∧ ∀𝑡 ∈ 𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡 ∈ 𝑤 (𝑧‘𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))) |
18 | 17 | 3impib 1108 |
. . . . . . 7
⊢ ((𝑧 Fn 𝑤 ∧ (𝑤 ⊆ 𝐴 ∧ ∀𝑡 ∈ 𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡 ∈ 𝑤 (𝑧‘𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)) |
19 | 18 | exlimiv 2010 |
. . . . . 6
⊢
(∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤 ⊆ 𝐴 ∧ ∀𝑡 ∈ 𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡 ∈ 𝑤 (𝑧‘𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)) |
20 | 8, 19 | sylbi 207 |
. . . . 5
⊢ (𝑧 ∈ 𝐵 → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)) |
21 | 5, 20 | syl 17 |
. . . 4
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)) |
22 | | dmeq 5462 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → dom 𝑤 = dom 𝑧) |
23 | 22 | sseq2d 3782 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)) |
24 | 23 | rspcev 3460 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → ∃𝑤 ∈ 𝐶 Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤) |
25 | | ssiun 4696 |
. . . . . . . 8
⊢
(∃𝑤 ∈
𝐶 Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ ∪ 𝑤 ∈ 𝐶 dom 𝑤) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → Pred(𝑅, 𝐴, 𝑋) ⊆ ∪ 𝑤 ∈ 𝐶 dom 𝑤) |
27 | | dmuni 5472 |
. . . . . . 7
⊢ dom ∪ 𝐶 =
∪ 𝑤 ∈ 𝐶 dom 𝑤 |
28 | 26, 27 | syl6sseqr 3801 |
. . . . . 6
⊢ ((𝑧 ∈ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → Pred(𝑅, 𝐴, 𝑋) ⊆ dom ∪
𝐶) |
29 | 28 | ex 397 |
. . . . 5
⊢ (𝑧 ∈ 𝐶 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom ∪
𝐶)) |
30 | 29 | adantl 467 |
. . . 4
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑧 ∈ 𝐶) → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom ∪
𝐶)) |
31 | 21, 30 | syld 47 |
. . 3
⊢ ((𝐶 ⊆ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom ∪
𝐶)) |
32 | 31 | rexlimdva 3179 |
. 2
⊢ (𝐶 ⊆ 𝐵 → (∃𝑧 ∈ 𝐶 𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom ∪
𝐶)) |
33 | 4, 32 | syl5bi 232 |
1
⊢ (𝐶 ⊆ 𝐵 → (𝑋 ∈ dom ∪
𝐶 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom ∪
𝐶)) |