Step | Hyp | Ref
| Expression |
1 | | tfr1on.f |
. . . . . . . . 9
⊢ 𝐹 = recs(𝐺) |
2 | | tfr1on.g |
. . . . . . . . 9
⊢ (𝜑 → Fun 𝐺) |
3 | | tfr1on.x |
. . . . . . . . 9
⊢ (𝜑 → Ord 𝑋) |
4 | | tfr1on.ex |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) |
5 | | tfr1onlemsucfn.1 |
. . . . . . . . 9
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} |
6 | | tfr1onlembacc.3 |
. . . . . . . . 9
⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}))} |
7 | | tfr1onlembacc.u |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) |
8 | | tfr1onlembacc.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ 𝑋) |
9 | | tfr1onlembacc.5 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | tfr1onlembfn 6348 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝐵 Fn
𝐷) |
11 | | fndm 5317 |
. . . . . . . 8
⊢ (∪ 𝐵 Fn
𝐷 → dom ∪ 𝐵 =
𝐷) |
12 | 10, 11 | syl 14 |
. . . . . . 7
⊢ (𝜑 → dom ∪ 𝐵 =
𝐷) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | tfr1onlembacc 6346 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
14 | 13 | unissd 3835 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝐵
⊆ ∪ 𝐴) |
15 | 5, 3 | tfr1onlemssrecs 6343 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝐴
⊆ recs(𝐺)) |
16 | 14, 15 | sstrd 3167 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝐵
⊆ recs(𝐺)) |
17 | | dmss 4828 |
. . . . . . . 8
⊢ (∪ 𝐵
⊆ recs(𝐺) → dom
∪ 𝐵 ⊆ dom recs(𝐺)) |
18 | 16, 17 | syl 14 |
. . . . . . 7
⊢ (𝜑 → dom ∪ 𝐵
⊆ dom recs(𝐺)) |
19 | 12, 18 | eqsstrrd 3194 |
. . . . . 6
⊢ (𝜑 → 𝐷 ⊆ dom recs(𝐺)) |
20 | 19 | sselda 3157 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → 𝑤 ∈ dom recs(𝐺)) |
21 | | eqid 2177 |
. . . . . 6
⊢ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} |
22 | 21 | tfrlem9 6323 |
. . . . 5
⊢ (𝑤 ∈ dom recs(𝐺) → (recs(𝐺)‘𝑤) = (𝐺‘(recs(𝐺) ↾ 𝑤))) |
23 | 20, 22 | syl 14 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → (recs(𝐺)‘𝑤) = (𝐺‘(recs(𝐺) ↾ 𝑤))) |
24 | | tfrfun 6324 |
. . . . 5
⊢ Fun
recs(𝐺) |
25 | 12 | eleq2d 2247 |
. . . . . 6
⊢ (𝜑 → (𝑤 ∈ dom ∪
𝐵 ↔ 𝑤 ∈ 𝐷)) |
26 | 25 | biimpar 297 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → 𝑤 ∈ dom ∪
𝐵) |
27 | | funssfv 5543 |
. . . . 5
⊢ ((Fun
recs(𝐺) ∧ ∪ 𝐵
⊆ recs(𝐺) ∧ 𝑤 ∈ dom ∪ 𝐵)
→ (recs(𝐺)‘𝑤) = (∪ 𝐵‘𝑤)) |
28 | 24, 16, 26, 27 | mp3an2ani 1344 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → (recs(𝐺)‘𝑤) = (∪ 𝐵‘𝑤)) |
29 | | ordelon 4385 |
. . . . . . . . . 10
⊢ ((Ord
𝑋 ∧ 𝐷 ∈ 𝑋) → 𝐷 ∈ On) |
30 | 3, 8, 29 | syl2anc 411 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ On) |
31 | | eloni 4377 |
. . . . . . . . 9
⊢ (𝐷 ∈ On → Ord 𝐷) |
32 | 30, 31 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → Ord 𝐷) |
33 | | ordelss 4381 |
. . . . . . . 8
⊢ ((Ord
𝐷 ∧ 𝑤 ∈ 𝐷) → 𝑤 ⊆ 𝐷) |
34 | 32, 33 | sylan 283 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → 𝑤 ⊆ 𝐷) |
35 | 12 | adantr 276 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → dom ∪
𝐵 = 𝐷) |
36 | 34, 35 | sseqtrrd 3196 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → 𝑤 ⊆ dom ∪
𝐵) |
37 | | fun2ssres 5261 |
. . . . . 6
⊢ ((Fun
recs(𝐺) ∧ ∪ 𝐵
⊆ recs(𝐺) ∧ 𝑤 ⊆ dom ∪ 𝐵)
→ (recs(𝐺) ↾
𝑤) = (∪ 𝐵
↾ 𝑤)) |
38 | 24, 16, 36, 37 | mp3an2ani 1344 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → (recs(𝐺) ↾ 𝑤) = (∪ 𝐵 ↾ 𝑤)) |
39 | 38 | fveq2d 5521 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → (𝐺‘(recs(𝐺) ↾ 𝑤)) = (𝐺‘(∪ 𝐵 ↾ 𝑤))) |
40 | 23, 28, 39 | 3eqtr3d 2218 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → (∪ 𝐵‘𝑤) = (𝐺‘(∪ 𝐵 ↾ 𝑤))) |
41 | 40 | ralrimiva 2550 |
. 2
⊢ (𝜑 → ∀𝑤 ∈ 𝐷 (∪ 𝐵‘𝑤) = (𝐺‘(∪ 𝐵 ↾ 𝑤))) |
42 | | fveq2 5517 |
. . . 4
⊢ (𝑢 = 𝑤 → (∪ 𝐵‘𝑢) = (∪ 𝐵‘𝑤)) |
43 | | reseq2 4904 |
. . . . 5
⊢ (𝑢 = 𝑤 → (∪ 𝐵 ↾ 𝑢) = (∪ 𝐵 ↾ 𝑤)) |
44 | 43 | fveq2d 5521 |
. . . 4
⊢ (𝑢 = 𝑤 → (𝐺‘(∪ 𝐵 ↾ 𝑢)) = (𝐺‘(∪ 𝐵 ↾ 𝑤))) |
45 | 42, 44 | eqeq12d 2192 |
. . 3
⊢ (𝑢 = 𝑤 → ((∪ 𝐵‘𝑢) = (𝐺‘(∪ 𝐵 ↾ 𝑢)) ↔ (∪ 𝐵‘𝑤) = (𝐺‘(∪ 𝐵 ↾ 𝑤)))) |
46 | 45 | cbvralv 2705 |
. 2
⊢
(∀𝑢 ∈
𝐷 (∪ 𝐵‘𝑢) = (𝐺‘(∪ 𝐵 ↾ 𝑢)) ↔ ∀𝑤 ∈ 𝐷 (∪ 𝐵‘𝑤) = (𝐺‘(∪ 𝐵 ↾ 𝑤))) |
47 | 41, 46 | sylibr 134 |
1
⊢ (𝜑 → ∀𝑢 ∈ 𝐷 (∪ 𝐵‘𝑢) = (𝐺‘(∪ 𝐵 ↾ 𝑢))) |