Proof of Theorem tz7.44-2
Step | Hyp | Ref
| Expression |
1 | | fveq2 6665 |
. . . 4
⊢ (𝑦 = suc 𝐵 → (𝐹‘𝑦) = (𝐹‘suc 𝐵)) |
2 | | reseq2 5843 |
. . . . 5
⊢ (𝑦 = suc 𝐵 → (𝐹 ↾ 𝑦) = (𝐹 ↾ suc 𝐵)) |
3 | 2 | fveq2d 6669 |
. . . 4
⊢ (𝑦 = suc 𝐵 → (𝐺‘(𝐹 ↾ 𝑦)) = (𝐺‘(𝐹 ↾ suc 𝐵))) |
4 | 1, 3 | eqeq12d 2837 |
. . 3
⊢ (𝑦 = suc 𝐵 → ((𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)) ↔ (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵)))) |
5 | | tz7.44.2 |
. . 3
⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦))) |
6 | 4, 5 | vtoclga 3574 |
. 2
⊢ (suc
𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵))) |
7 | | tz7.44.1 |
. . 3
⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))))) |
8 | | eqeq1 2825 |
. . . 4
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥 = ∅ ↔ (𝐹 ↾ suc 𝐵) = ∅)) |
9 | | dmeq 5767 |
. . . . . 6
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → dom 𝑥 = dom (𝐹 ↾ suc 𝐵)) |
10 | | limeq 6198 |
. . . . . 6
⊢ (dom
𝑥 = dom (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵))) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵))) |
12 | | rneq 5801 |
. . . . . 6
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ran 𝑥 = ran (𝐹 ↾ suc 𝐵)) |
13 | 12 | unieqd 4842 |
. . . . 5
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ ran
𝑥 = ∪ ran (𝐹 ↾ suc 𝐵)) |
14 | | fveq1 6664 |
. . . . . . 7
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom
𝑥)) |
15 | 9 | unieqd 4842 |
. . . . . . . 8
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ dom
𝑥 = ∪ dom (𝐹 ↾ suc 𝐵)) |
16 | 15 | fveq2d 6669 |
. . . . . . 7
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ((𝐹 ↾ suc 𝐵)‘∪ dom
𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))) |
17 | 14, 16 | eqtrd 2856 |
. . . . . 6
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))) |
18 | 17 | fveq2d 6669 |
. . . . 5
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝐻‘(𝑥‘∪ dom 𝑥)) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))) |
19 | 11, 13, 18 | ifbieq12d 4494 |
. . . 4
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) |
20 | 8, 19 | ifbieq2d 4492 |
. . 3
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))))) |
21 | 2 | eleq1d 2897 |
. . . 4
⊢ (𝑦 = suc 𝐵 → ((𝐹 ↾ 𝑦) ∈ V ↔ (𝐹 ↾ suc 𝐵) ∈ V)) |
22 | | tz7.44.3 |
. . . 4
⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V) |
23 | 21, 22 | vtoclga 3574 |
. . 3
⊢ (suc
𝐵 ∈ 𝑋 → (𝐹 ↾ suc 𝐵) ∈ V) |
24 | | noel 4296 |
. . . . . . 7
⊢ ¬
𝐵 ∈
∅ |
25 | | dmeq 5767 |
. . . . . . . . 9
⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = dom ∅) |
26 | | dm0 5785 |
. . . . . . . . 9
⊢ dom
∅ = ∅ |
27 | 25, 26 | syl6eq 2872 |
. . . . . . . 8
⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = ∅) |
28 | | tz7.44.5 |
. . . . . . . . . . . . 13
⊢ Ord 𝑋 |
29 | | ordsson 7498 |
. . . . . . . . . . . . 13
⊢ (Ord
𝑋 → 𝑋 ⊆ On) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝑋 ⊆ On |
31 | | ordtr 6200 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝑋 → Tr 𝑋) |
32 | 28, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ Tr 𝑋 |
33 | | trsuc 6270 |
. . . . . . . . . . . . 13
⊢ ((Tr
𝑋 ∧ suc 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋) |
34 | 32, 33 | mpan 688 |
. . . . . . . . . . . 12
⊢ (suc
𝐵 ∈ 𝑋 → 𝐵 ∈ 𝑋) |
35 | 30, 34 | sseldi 3965 |
. . . . . . . . . . 11
⊢ (suc
𝐵 ∈ 𝑋 → 𝐵 ∈ On) |
36 | | sucidg 6264 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → 𝐵 ∈ suc 𝐵) |
37 | 35, 36 | syl 17 |
. . . . . . . . . 10
⊢ (suc
𝐵 ∈ 𝑋 → 𝐵 ∈ suc 𝐵) |
38 | | dmres 5870 |
. . . . . . . . . . 11
⊢ dom
(𝐹 ↾ suc 𝐵) = (suc 𝐵 ∩ dom 𝐹) |
39 | | ordelss 6202 |
. . . . . . . . . . . . . 14
⊢ ((Ord
𝑋 ∧ suc 𝐵 ∈ 𝑋) → suc 𝐵 ⊆ 𝑋) |
40 | 28, 39 | mpan 688 |
. . . . . . . . . . . . 13
⊢ (suc
𝐵 ∈ 𝑋 → suc 𝐵 ⊆ 𝑋) |
41 | | tz7.44.4 |
. . . . . . . . . . . . . 14
⊢ 𝐹 Fn 𝑋 |
42 | | fndm 6450 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ dom 𝐹 = 𝑋 |
44 | 40, 43 | sseqtrrdi 4018 |
. . . . . . . . . . . 12
⊢ (suc
𝐵 ∈ 𝑋 → suc 𝐵 ⊆ dom 𝐹) |
45 | | df-ss 3952 |
. . . . . . . . . . . 12
⊢ (suc
𝐵 ⊆ dom 𝐹 ↔ (suc 𝐵 ∩ dom 𝐹) = suc 𝐵) |
46 | 44, 45 | sylib 220 |
. . . . . . . . . . 11
⊢ (suc
𝐵 ∈ 𝑋 → (suc 𝐵 ∩ dom 𝐹) = suc 𝐵) |
47 | 38, 46 | syl5eq 2868 |
. . . . . . . . . 10
⊢ (suc
𝐵 ∈ 𝑋 → dom (𝐹 ↾ suc 𝐵) = suc 𝐵) |
48 | 37, 47 | eleqtrrd 2916 |
. . . . . . . . 9
⊢ (suc
𝐵 ∈ 𝑋 → 𝐵 ∈ dom (𝐹 ↾ suc 𝐵)) |
49 | | eleq2 2901 |
. . . . . . . . 9
⊢ (dom
(𝐹 ↾ suc 𝐵) = ∅ → (𝐵 ∈ dom (𝐹 ↾ suc 𝐵) ↔ 𝐵 ∈ ∅)) |
50 | 48, 49 | syl5ibcom 247 |
. . . . . . . 8
⊢ (suc
𝐵 ∈ 𝑋 → (dom (𝐹 ↾ suc 𝐵) = ∅ → 𝐵 ∈ ∅)) |
51 | 27, 50 | syl5 34 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵) = ∅ → 𝐵 ∈ ∅)) |
52 | 24, 51 | mtoi 201 |
. . . . . 6
⊢ (suc
𝐵 ∈ 𝑋 → ¬ (𝐹 ↾ suc 𝐵) = ∅) |
53 | 52 | iffalsed 4478 |
. . . . 5
⊢ (suc
𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) |
54 | | nlimsucg 7551 |
. . . . . . . 8
⊢ (𝐵 ∈ On → ¬ Lim suc
𝐵) |
55 | 35, 54 | syl 17 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → ¬ Lim suc 𝐵) |
56 | | limeq 6198 |
. . . . . . . 8
⊢ (dom
(𝐹 ↾ suc 𝐵) = suc 𝐵 → (Lim dom (𝐹 ↾ suc 𝐵) ↔ Lim suc 𝐵)) |
57 | 47, 56 | syl 17 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → (Lim dom (𝐹 ↾ suc 𝐵) ↔ Lim suc 𝐵)) |
58 | 55, 57 | mtbird 327 |
. . . . . 6
⊢ (suc
𝐵 ∈ 𝑋 → ¬ Lim dom (𝐹 ↾ suc 𝐵)) |
59 | 58 | iffalsed 4478 |
. . . . 5
⊢ (suc
𝐵 ∈ 𝑋 → if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))) |
60 | 47 | unieqd 4842 |
. . . . . . . . 9
⊢ (suc
𝐵 ∈ 𝑋 → ∪ dom
(𝐹 ↾ suc 𝐵) = ∪
suc 𝐵) |
61 | | eloni 6196 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → Ord 𝐵) |
62 | | ordunisuc 7541 |
. . . . . . . . . 10
⊢ (Ord
𝐵 → ∪ suc 𝐵 = 𝐵) |
63 | 35, 61, 62 | 3syl 18 |
. . . . . . . . 9
⊢ (suc
𝐵 ∈ 𝑋 → ∪ suc
𝐵 = 𝐵) |
64 | 60, 63 | eqtrd 2856 |
. . . . . . . 8
⊢ (suc
𝐵 ∈ 𝑋 → ∪ dom
(𝐹 ↾ suc 𝐵) = 𝐵) |
65 | 64 | fveq2d 6669 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)) = ((𝐹 ↾ suc 𝐵)‘𝐵)) |
66 | 37 | fvresd 6685 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘𝐵) = (𝐹‘𝐵)) |
67 | 65, 66 | eqtrd 2856 |
. . . . . 6
⊢ (suc
𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)) = (𝐹‘𝐵)) |
68 | 67 | fveq2d 6669 |
. . . . 5
⊢ (suc
𝐵 ∈ 𝑋 → (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))) = (𝐻‘(𝐹‘𝐵))) |
69 | 53, 59, 68 | 3eqtrd 2860 |
. . . 4
⊢ (suc
𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) = (𝐻‘(𝐹‘𝐵))) |
70 | | fvex 6678 |
. . . 4
⊢ (𝐻‘(𝐹‘𝐵)) ∈ V |
71 | 69, 70 | eqeltrdi 2921 |
. . 3
⊢ (suc
𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) ∈ V) |
72 | 7, 20, 23, 71 | fvmptd3 6786 |
. 2
⊢ (suc
𝐵 ∈ 𝑋 → (𝐺‘(𝐹 ↾ suc 𝐵)) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))))) |
73 | 6, 72, 69 | 3eqtrd 2860 |
1
⊢ (suc
𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹‘𝐵))) |