Proof of Theorem tz7.44-2
| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . 4
⊢ (𝑦 = suc 𝐵 → (𝐹‘𝑦) = (𝐹‘suc 𝐵)) |
| 2 | | reseq2 5992 |
. . . . 5
⊢ (𝑦 = suc 𝐵 → (𝐹 ↾ 𝑦) = (𝐹 ↾ suc 𝐵)) |
| 3 | 2 | fveq2d 6910 |
. . . 4
⊢ (𝑦 = suc 𝐵 → (𝐺‘(𝐹 ↾ 𝑦)) = (𝐺‘(𝐹 ↾ suc 𝐵))) |
| 4 | 1, 3 | eqeq12d 2753 |
. . 3
⊢ (𝑦 = suc 𝐵 → ((𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)) ↔ (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵)))) |
| 5 | | tz7.44.2 |
. . 3
⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦))) |
| 6 | 4, 5 | vtoclga 3577 |
. 2
⊢ (suc
𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵))) |
| 7 | | tz7.44.1 |
. . 3
⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))))) |
| 8 | | eqeq1 2741 |
. . . 4
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥 = ∅ ↔ (𝐹 ↾ suc 𝐵) = ∅)) |
| 9 | | dmeq 5914 |
. . . . . 6
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → dom 𝑥 = dom (𝐹 ↾ suc 𝐵)) |
| 10 | | limeq 6396 |
. . . . . 6
⊢ (dom
𝑥 = dom (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵))) |
| 11 | 9, 10 | syl 17 |
. . . . 5
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵))) |
| 12 | | rneq 5947 |
. . . . . 6
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ran 𝑥 = ran (𝐹 ↾ suc 𝐵)) |
| 13 | 12 | unieqd 4920 |
. . . . 5
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ ran
𝑥 = ∪ ran (𝐹 ↾ suc 𝐵)) |
| 14 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom
𝑥)) |
| 15 | 9 | unieqd 4920 |
. . . . . . . 8
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ dom
𝑥 = ∪ dom (𝐹 ↾ suc 𝐵)) |
| 16 | 15 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ((𝐹 ↾ suc 𝐵)‘∪ dom
𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))) |
| 17 | 14, 16 | eqtrd 2777 |
. . . . . 6
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))) |
| 18 | 17 | fveq2d 6910 |
. . . . 5
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝐻‘(𝑥‘∪ dom 𝑥)) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))) |
| 19 | 11, 13, 18 | ifbieq12d 4554 |
. . . 4
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) |
| 20 | 8, 19 | ifbieq2d 4552 |
. . 3
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))))) |
| 21 | 2 | eleq1d 2826 |
. . . 4
⊢ (𝑦 = suc 𝐵 → ((𝐹 ↾ 𝑦) ∈ V ↔ (𝐹 ↾ suc 𝐵) ∈ V)) |
| 22 | | tz7.44.3 |
. . . 4
⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V) |
| 23 | 21, 22 | vtoclga 3577 |
. . 3
⊢ (suc
𝐵 ∈ 𝑋 → (𝐹 ↾ suc 𝐵) ∈ V) |
| 24 | | noel 4338 |
. . . . . . 7
⊢ ¬
𝐵 ∈
∅ |
| 25 | | dmeq 5914 |
. . . . . . . . 9
⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = dom ∅) |
| 26 | | dm0 5931 |
. . . . . . . . 9
⊢ dom
∅ = ∅ |
| 27 | 25, 26 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = ∅) |
| 28 | | tz7.44.5 |
. . . . . . . . . . . . 13
⊢ Ord 𝑋 |
| 29 | | ordsson 7803 |
. . . . . . . . . . . . 13
⊢ (Ord
𝑋 → 𝑋 ⊆ On) |
| 30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝑋 ⊆ On |
| 31 | | ordtr 6398 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝑋 → Tr 𝑋) |
| 32 | 28, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ Tr 𝑋 |
| 33 | | trsuc 6471 |
. . . . . . . . . . . . 13
⊢ ((Tr
𝑋 ∧ suc 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋) |
| 34 | 32, 33 | mpan 690 |
. . . . . . . . . . . 12
⊢ (suc
𝐵 ∈ 𝑋 → 𝐵 ∈ 𝑋) |
| 35 | 30, 34 | sselid 3981 |
. . . . . . . . . . 11
⊢ (suc
𝐵 ∈ 𝑋 → 𝐵 ∈ On) |
| 36 | | sucidg 6465 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → 𝐵 ∈ suc 𝐵) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . 10
⊢ (suc
𝐵 ∈ 𝑋 → 𝐵 ∈ suc 𝐵) |
| 38 | | dmres 6030 |
. . . . . . . . . . 11
⊢ dom
(𝐹 ↾ suc 𝐵) = (suc 𝐵 ∩ dom 𝐹) |
| 39 | | ordelss 6400 |
. . . . . . . . . . . . . 14
⊢ ((Ord
𝑋 ∧ suc 𝐵 ∈ 𝑋) → suc 𝐵 ⊆ 𝑋) |
| 40 | 28, 39 | mpan 690 |
. . . . . . . . . . . . 13
⊢ (suc
𝐵 ∈ 𝑋 → suc 𝐵 ⊆ 𝑋) |
| 41 | | tz7.44.4 |
. . . . . . . . . . . . . 14
⊢ 𝐹 Fn 𝑋 |
| 42 | 41 | fndmi 6672 |
. . . . . . . . . . . . 13
⊢ dom 𝐹 = 𝑋 |
| 43 | 40, 42 | sseqtrrdi 4025 |
. . . . . . . . . . . 12
⊢ (suc
𝐵 ∈ 𝑋 → suc 𝐵 ⊆ dom 𝐹) |
| 44 | | dfss2 3969 |
. . . . . . . . . . . 12
⊢ (suc
𝐵 ⊆ dom 𝐹 ↔ (suc 𝐵 ∩ dom 𝐹) = suc 𝐵) |
| 45 | 43, 44 | sylib 218 |
. . . . . . . . . . 11
⊢ (suc
𝐵 ∈ 𝑋 → (suc 𝐵 ∩ dom 𝐹) = suc 𝐵) |
| 46 | 38, 45 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (suc
𝐵 ∈ 𝑋 → dom (𝐹 ↾ suc 𝐵) = suc 𝐵) |
| 47 | 37, 46 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ (suc
𝐵 ∈ 𝑋 → 𝐵 ∈ dom (𝐹 ↾ suc 𝐵)) |
| 48 | | eleq2 2830 |
. . . . . . . . 9
⊢ (dom
(𝐹 ↾ suc 𝐵) = ∅ → (𝐵 ∈ dom (𝐹 ↾ suc 𝐵) ↔ 𝐵 ∈ ∅)) |
| 49 | 47, 48 | syl5ibcom 245 |
. . . . . . . 8
⊢ (suc
𝐵 ∈ 𝑋 → (dom (𝐹 ↾ suc 𝐵) = ∅ → 𝐵 ∈ ∅)) |
| 50 | 27, 49 | syl5 34 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵) = ∅ → 𝐵 ∈ ∅)) |
| 51 | 24, 50 | mtoi 199 |
. . . . . 6
⊢ (suc
𝐵 ∈ 𝑋 → ¬ (𝐹 ↾ suc 𝐵) = ∅) |
| 52 | 51 | iffalsed 4536 |
. . . . 5
⊢ (suc
𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) |
| 53 | | nlimsucg 7863 |
. . . . . . . 8
⊢ (𝐵 ∈ On → ¬ Lim suc
𝐵) |
| 54 | 35, 53 | syl 17 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → ¬ Lim suc 𝐵) |
| 55 | | limeq 6396 |
. . . . . . . 8
⊢ (dom
(𝐹 ↾ suc 𝐵) = suc 𝐵 → (Lim dom (𝐹 ↾ suc 𝐵) ↔ Lim suc 𝐵)) |
| 56 | 46, 55 | syl 17 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → (Lim dom (𝐹 ↾ suc 𝐵) ↔ Lim suc 𝐵)) |
| 57 | 54, 56 | mtbird 325 |
. . . . . 6
⊢ (suc
𝐵 ∈ 𝑋 → ¬ Lim dom (𝐹 ↾ suc 𝐵)) |
| 58 | 57 | iffalsed 4536 |
. . . . 5
⊢ (suc
𝐵 ∈ 𝑋 → if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))) |
| 59 | 46 | unieqd 4920 |
. . . . . . . . 9
⊢ (suc
𝐵 ∈ 𝑋 → ∪ dom
(𝐹 ↾ suc 𝐵) = ∪
suc 𝐵) |
| 60 | | eloni 6394 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → Ord 𝐵) |
| 61 | | ordunisuc 7852 |
. . . . . . . . . 10
⊢ (Ord
𝐵 → ∪ suc 𝐵 = 𝐵) |
| 62 | 35, 60, 61 | 3syl 18 |
. . . . . . . . 9
⊢ (suc
𝐵 ∈ 𝑋 → ∪ suc
𝐵 = 𝐵) |
| 63 | 59, 62 | eqtrd 2777 |
. . . . . . . 8
⊢ (suc
𝐵 ∈ 𝑋 → ∪ dom
(𝐹 ↾ suc 𝐵) = 𝐵) |
| 64 | 63 | fveq2d 6910 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)) = ((𝐹 ↾ suc 𝐵)‘𝐵)) |
| 65 | 37 | fvresd 6926 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘𝐵) = (𝐹‘𝐵)) |
| 66 | 64, 65 | eqtrd 2777 |
. . . . . 6
⊢ (suc
𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)) = (𝐹‘𝐵)) |
| 67 | 66 | fveq2d 6910 |
. . . . 5
⊢ (suc
𝐵 ∈ 𝑋 → (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))) = (𝐻‘(𝐹‘𝐵))) |
| 68 | 52, 58, 67 | 3eqtrd 2781 |
. . . 4
⊢ (suc
𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) = (𝐻‘(𝐹‘𝐵))) |
| 69 | | fvex 6919 |
. . . 4
⊢ (𝐻‘(𝐹‘𝐵)) ∈ V |
| 70 | 68, 69 | eqeltrdi 2849 |
. . 3
⊢ (suc
𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) ∈ V) |
| 71 | 7, 20, 23, 70 | fvmptd3 7039 |
. 2
⊢ (suc
𝐵 ∈ 𝑋 → (𝐺‘(𝐹 ↾ suc 𝐵)) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))))) |
| 72 | 6, 71, 68 | 3eqtrd 2781 |
1
⊢ (suc
𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹‘𝐵))) |