Proof of Theorem tfr1onlemubacc
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 6292 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝐵 Fn
𝐷) |
11 | | fndm 5270 |
. . . . . . . 8
⊢ (∪ 𝐵 Fn
𝐷 → dom ∪ 𝐵 =
𝐷) |
12 | 10, 11 | syl 14 |
. . . . . . 7
⊢ (𝜑 → dom ∪ 𝐵 =
𝐷) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | tfr1onlembacc 6290 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
14 | 13 | unissd 3797 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝐵
⊆ ∪ 𝐴) |
15 | 5, 3 | tfr1onlemssrecs 6287 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝐴
⊆ recs(𝐺)) |
16 | 14, 15 | sstrd 3138 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝐵
⊆ recs(𝐺)) |
17 | | dmss 4786 |
. . . . . . . 8
⊢ (∪ 𝐵
⊆ recs(𝐺) → dom
∪ 𝐵 ⊆ dom recs(𝐺)) |
18 | 16, 17 | syl 14 |
. . . . . . 7
⊢ (𝜑 → dom ∪ 𝐵
⊆ dom recs(𝐺)) |
19 | 12, 18 | eqsstrrd 3165 |
. . . . . 6
⊢ (𝜑 → 𝐷 ⊆ dom recs(𝐺)) |
20 | 19 | sselda 3128 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → 𝑤 ∈ dom recs(𝐺)) |
21 | | eqid 2157 |
. . . . . 6
⊢ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} |
22 | 21 | tfrlem9 6267 |
. . . . 5
⊢ (𝑤 ∈ dom recs(𝐺) → (recs(𝐺)‘𝑤) = (𝐺‘(recs(𝐺) ↾ 𝑤))) |
23 | 20, 22 | syl 14 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → (recs(𝐺)‘𝑤) = (𝐺‘(recs(𝐺) ↾ 𝑤))) |
24 | | tfrfun 6268 |
. . . . 5
⊢ Fun
recs(𝐺) |
25 | 12 | eleq2d 2227 |
. . . . . 6
⊢ (𝜑 → (𝑤 ∈ dom ∪
𝐵 ↔ 𝑤 ∈ 𝐷)) |
26 | 25 | biimpar 295 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → 𝑤 ∈ dom ∪
𝐵) |
27 | | funssfv 5495 |
. . . . 5
⊢ ((Fun
recs(𝐺) ∧ ∪ 𝐵
⊆ recs(𝐺) ∧ 𝑤 ∈ dom ∪ 𝐵)
→ (recs(𝐺)‘𝑤) = (∪ 𝐵‘𝑤)) |
28 | 24, 16, 26, 27 | mp3an2ani 1326 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → (recs(𝐺)‘𝑤) = (∪ 𝐵‘𝑤)) |
29 | | ordelon 4344 |
. . . . . . . . . 10
⊢ ((Ord
𝑋 ∧ 𝐷 ∈ 𝑋) → 𝐷 ∈ On) |
30 | 3, 8, 29 | syl2anc 409 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ On) |
31 | | eloni 4336 |
. . . . . . . . 9
⊢ (𝐷 ∈ On → Ord 𝐷) |
32 | 30, 31 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → Ord 𝐷) |
33 | | ordelss 4340 |
. . . . . . . 8
⊢ ((Ord
𝐷 ∧ 𝑤 ∈ 𝐷) → 𝑤 ⊆ 𝐷) |
34 | 32, 33 | sylan 281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → 𝑤 ⊆ 𝐷) |
35 | 12 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → dom ∪
𝐵 = 𝐷) |
36 | 34, 35 | sseqtrrd 3167 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → 𝑤 ⊆ dom ∪
𝐵) |
37 | | fun2ssres 5214 |
. . . . . 6
⊢ ((Fun
recs(𝐺) ∧ ∪ 𝐵
⊆ recs(𝐺) ∧ 𝑤 ⊆ dom ∪ 𝐵)
→ (recs(𝐺) ↾
𝑤) = (∪ 𝐵
↾ 𝑤)) |
38 | 24, 16, 36, 37 | mp3an2ani 1326 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → (recs(𝐺) ↾ 𝑤) = (∪ 𝐵 ↾ 𝑤)) |
39 | 38 | fveq2d 5473 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → (𝐺‘(recs(𝐺) ↾ 𝑤)) = (𝐺‘(∪ 𝐵 ↾ 𝑤))) |
40 | 23, 28, 39 | 3eqtr3d 2198 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → (∪ 𝐵‘𝑤) = (𝐺‘(∪ 𝐵 ↾ 𝑤))) |
41 | 40 | ralrimiva 2530 |
. 2
⊢ (𝜑 → ∀𝑤 ∈ 𝐷 (∪ 𝐵‘𝑤) = (𝐺‘(∪ 𝐵 ↾ 𝑤))) |
42 | | fveq2 5469 |
. . . 4
⊢ (𝑢 = 𝑤 → (∪ 𝐵‘𝑢) = (∪ 𝐵‘𝑤)) |
43 | | reseq2 4862 |
. . . . 5
⊢ (𝑢 = 𝑤 → (∪ 𝐵 ↾ 𝑢) = (∪ 𝐵 ↾ 𝑤)) |
44 | 43 | fveq2d 5473 |
. . . 4
⊢ (𝑢 = 𝑤 → (𝐺‘(∪ 𝐵 ↾ 𝑢)) = (𝐺‘(∪ 𝐵 ↾ 𝑤))) |
45 | 42, 44 | eqeq12d 2172 |
. . 3
⊢ (𝑢 = 𝑤 → ((∪ 𝐵‘𝑢) = (𝐺‘(∪ 𝐵 ↾ 𝑢)) ↔ (∪ 𝐵‘𝑤) = (𝐺‘(∪ 𝐵 ↾ 𝑤)))) |
46 | 45 | cbvralv 2680 |
. 2
⊢
(∀𝑢 ∈
𝐷 (∪ 𝐵‘𝑢) = (𝐺‘(∪ 𝐵 ↾ 𝑢)) ↔ ∀𝑤 ∈ 𝐷 (∪ 𝐵‘𝑤) = (𝐺‘(∪ 𝐵 ↾ 𝑤))) |
47 | 41, 46 | sylibr 133 |
1
⊢ (𝜑 → ∀𝑢 ∈ 𝐷 (∪ 𝐵‘𝑢) = (𝐺‘(∪ 𝐵 ↾ 𝑢))) |