Proof of Theorem tz7.44-2
Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . 4
⊢ (𝑦 = suc 𝐵 → (𝐹‘𝑦) = (𝐹‘suc 𝐵)) |
2 | | reseq2 5391 |
. . . . 5
⊢ (𝑦 = suc 𝐵 → (𝐹 ↾ 𝑦) = (𝐹 ↾ suc 𝐵)) |
3 | 2 | fveq2d 6195 |
. . . 4
⊢ (𝑦 = suc 𝐵 → (𝐺‘(𝐹 ↾ 𝑦)) = (𝐺‘(𝐹 ↾ suc 𝐵))) |
4 | 1, 3 | eqeq12d 2637 |
. . 3
⊢ (𝑦 = suc 𝐵 → ((𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)) ↔ (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵)))) |
5 | | tz7.44.2 |
. . 3
⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦))) |
6 | 4, 5 | vtoclga 3272 |
. 2
⊢ (suc
𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐺‘(𝐹 ↾ suc 𝐵))) |
7 | 2 | eleq1d 2686 |
. . . 4
⊢ (𝑦 = suc 𝐵 → ((𝐹 ↾ 𝑦) ∈ V ↔ (𝐹 ↾ suc 𝐵) ∈ V)) |
8 | | tz7.44.3 |
. . . 4
⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V) |
9 | 7, 8 | vtoclga 3272 |
. . 3
⊢ (suc
𝐵 ∈ 𝑋 → (𝐹 ↾ suc 𝐵) ∈ V) |
10 | | noel 3919 |
. . . . . . 7
⊢ ¬
𝐵 ∈
∅ |
11 | | dmeq 5324 |
. . . . . . . . 9
⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = dom ∅) |
12 | | dm0 5339 |
. . . . . . . . 9
⊢ dom
∅ = ∅ |
13 | 11, 12 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝐹 ↾ suc 𝐵) = ∅ → dom (𝐹 ↾ suc 𝐵) = ∅) |
14 | | tz7.44.5 |
. . . . . . . . . . . . 13
⊢ Ord 𝑋 |
15 | | ordsson 6989 |
. . . . . . . . . . . . 13
⊢ (Ord
𝑋 → 𝑋 ⊆ On) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝑋 ⊆ On |
17 | | ordtr 5737 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝑋 → Tr 𝑋) |
18 | 14, 17 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ Tr 𝑋 |
19 | | trsuc 5810 |
. . . . . . . . . . . . 13
⊢ ((Tr
𝑋 ∧ suc 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋) |
20 | 18, 19 | mpan 706 |
. . . . . . . . . . . 12
⊢ (suc
𝐵 ∈ 𝑋 → 𝐵 ∈ 𝑋) |
21 | 16, 20 | sseldi 3601 |
. . . . . . . . . . 11
⊢ (suc
𝐵 ∈ 𝑋 → 𝐵 ∈ On) |
22 | | sucidg 5803 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → 𝐵 ∈ suc 𝐵) |
23 | 21, 22 | syl 17 |
. . . . . . . . . 10
⊢ (suc
𝐵 ∈ 𝑋 → 𝐵 ∈ suc 𝐵) |
24 | | dmres 5419 |
. . . . . . . . . . 11
⊢ dom
(𝐹 ↾ suc 𝐵) = (suc 𝐵 ∩ dom 𝐹) |
25 | | ordelss 5739 |
. . . . . . . . . . . . . 14
⊢ ((Ord
𝑋 ∧ suc 𝐵 ∈ 𝑋) → suc 𝐵 ⊆ 𝑋) |
26 | 14, 25 | mpan 706 |
. . . . . . . . . . . . 13
⊢ (suc
𝐵 ∈ 𝑋 → suc 𝐵 ⊆ 𝑋) |
27 | | tz7.44.4 |
. . . . . . . . . . . . . 14
⊢ 𝐹 Fn 𝑋 |
28 | | fndm 5990 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ dom 𝐹 = 𝑋 |
30 | 26, 29 | syl6sseqr 3652 |
. . . . . . . . . . . 12
⊢ (suc
𝐵 ∈ 𝑋 → suc 𝐵 ⊆ dom 𝐹) |
31 | | df-ss 3588 |
. . . . . . . . . . . 12
⊢ (suc
𝐵 ⊆ dom 𝐹 ↔ (suc 𝐵 ∩ dom 𝐹) = suc 𝐵) |
32 | 30, 31 | sylib 208 |
. . . . . . . . . . 11
⊢ (suc
𝐵 ∈ 𝑋 → (suc 𝐵 ∩ dom 𝐹) = suc 𝐵) |
33 | 24, 32 | syl5eq 2668 |
. . . . . . . . . 10
⊢ (suc
𝐵 ∈ 𝑋 → dom (𝐹 ↾ suc 𝐵) = suc 𝐵) |
34 | 23, 33 | eleqtrrd 2704 |
. . . . . . . . 9
⊢ (suc
𝐵 ∈ 𝑋 → 𝐵 ∈ dom (𝐹 ↾ suc 𝐵)) |
35 | | eleq2 2690 |
. . . . . . . . 9
⊢ (dom
(𝐹 ↾ suc 𝐵) = ∅ → (𝐵 ∈ dom (𝐹 ↾ suc 𝐵) ↔ 𝐵 ∈ ∅)) |
36 | 34, 35 | syl5ibcom 235 |
. . . . . . . 8
⊢ (suc
𝐵 ∈ 𝑋 → (dom (𝐹 ↾ suc 𝐵) = ∅ → 𝐵 ∈ ∅)) |
37 | 13, 36 | syl5 34 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵) = ∅ → 𝐵 ∈ ∅)) |
38 | 10, 37 | mtoi 190 |
. . . . . 6
⊢ (suc
𝐵 ∈ 𝑋 → ¬ (𝐹 ↾ suc 𝐵) = ∅) |
39 | 38 | iffalsed 4097 |
. . . . 5
⊢ (suc
𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) |
40 | | nlimsucg 7042 |
. . . . . . . 8
⊢ (𝐵 ∈ On → ¬ Lim suc
𝐵) |
41 | 21, 40 | syl 17 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → ¬ Lim suc 𝐵) |
42 | | limeq 5735 |
. . . . . . . 8
⊢ (dom
(𝐹 ↾ suc 𝐵) = suc 𝐵 → (Lim dom (𝐹 ↾ suc 𝐵) ↔ Lim suc 𝐵)) |
43 | 33, 42 | syl 17 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → (Lim dom (𝐹 ↾ suc 𝐵) ↔ Lim suc 𝐵)) |
44 | 41, 43 | mtbird 315 |
. . . . . 6
⊢ (suc
𝐵 ∈ 𝑋 → ¬ Lim dom (𝐹 ↾ suc 𝐵)) |
45 | 44 | iffalsed 4097 |
. . . . 5
⊢ (suc
𝐵 ∈ 𝑋 → if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))) |
46 | 33 | unieqd 4446 |
. . . . . . . . 9
⊢ (suc
𝐵 ∈ 𝑋 → ∪ dom
(𝐹 ↾ suc 𝐵) = ∪
suc 𝐵) |
47 | | eloni 5733 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → Ord 𝐵) |
48 | | ordunisuc 7032 |
. . . . . . . . . . 11
⊢ (Ord
𝐵 → ∪ suc 𝐵 = 𝐵) |
49 | 47, 48 | syl 17 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → ∪ suc 𝐵 = 𝐵) |
50 | 21, 49 | syl 17 |
. . . . . . . . 9
⊢ (suc
𝐵 ∈ 𝑋 → ∪ suc
𝐵 = 𝐵) |
51 | 46, 50 | eqtrd 2656 |
. . . . . . . 8
⊢ (suc
𝐵 ∈ 𝑋 → ∪ dom
(𝐹 ↾ suc 𝐵) = 𝐵) |
52 | 51 | fveq2d 6195 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)) = ((𝐹 ↾ suc 𝐵)‘𝐵)) |
53 | | fvres 6207 |
. . . . . . . 8
⊢ (𝐵 ∈ suc 𝐵 → ((𝐹 ↾ suc 𝐵)‘𝐵) = (𝐹‘𝐵)) |
54 | 23, 53 | syl 17 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘𝐵) = (𝐹‘𝐵)) |
55 | 52, 54 | eqtrd 2656 |
. . . . . 6
⊢ (suc
𝐵 ∈ 𝑋 → ((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)) = (𝐹‘𝐵)) |
56 | 55 | fveq2d 6195 |
. . . . 5
⊢ (suc
𝐵 ∈ 𝑋 → (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))) = (𝐻‘(𝐹‘𝐵))) |
57 | 39, 45, 56 | 3eqtrd 2660 |
. . . 4
⊢ (suc
𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) = (𝐻‘(𝐹‘𝐵))) |
58 | | fvex 6201 |
. . . 4
⊢ (𝐻‘(𝐹‘𝐵)) ∈ V |
59 | 57, 58 | syl6eqel 2709 |
. . 3
⊢ (suc
𝐵 ∈ 𝑋 → if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) ∈ V) |
60 | | eqeq1 2626 |
. . . . 5
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥 = ∅ ↔ (𝐹 ↾ suc 𝐵) = ∅)) |
61 | | dmeq 5324 |
. . . . . . 7
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → dom 𝑥 = dom (𝐹 ↾ suc 𝐵)) |
62 | | limeq 5735 |
. . . . . . 7
⊢ (dom
𝑥 = dom (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵))) |
63 | 61, 62 | syl 17 |
. . . . . 6
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (Lim dom 𝑥 ↔ Lim dom (𝐹 ↾ suc 𝐵))) |
64 | | rneq 5351 |
. . . . . . 7
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ran 𝑥 = ran (𝐹 ↾ suc 𝐵)) |
65 | 64 | unieqd 4446 |
. . . . . 6
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ ran
𝑥 = ∪ ran (𝐹 ↾ suc 𝐵)) |
66 | | fveq1 6190 |
. . . . . . . 8
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom
𝑥)) |
67 | 61 | unieqd 4446 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ∪ dom
𝑥 = ∪ dom (𝐹 ↾ suc 𝐵)) |
68 | 67 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → ((𝐹 ↾ suc 𝐵)‘∪ dom
𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))) |
69 | 66, 68 | eqtrd 2656 |
. . . . . . 7
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝑥‘∪ dom 𝑥) = ((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))) |
70 | 69 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → (𝐻‘(𝑥‘∪ dom 𝑥)) = (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))) |
71 | 63, 65, 70 | ifbieq12d 4113 |
. . . . 5
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))) = if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) |
72 | 60, 71 | ifbieq2d 4111 |
. . . 4
⊢ (𝑥 = (𝐹 ↾ suc 𝐵) → if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))))) |
73 | | tz7.44.1 |
. . . 4
⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))))) |
74 | 72, 73 | fvmptg 6280 |
. . 3
⊢ (((𝐹 ↾ suc 𝐵) ∈ V ∧ if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵))))) ∈ V) → (𝐺‘(𝐹 ↾ suc 𝐵)) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))))) |
75 | 9, 59, 74 | syl2anc 693 |
. 2
⊢ (suc
𝐵 ∈ 𝑋 → (𝐺‘(𝐹 ↾ suc 𝐵)) = if((𝐹 ↾ suc 𝐵) = ∅, 𝐴, if(Lim dom (𝐹 ↾ suc 𝐵), ∪ ran (𝐹 ↾ suc 𝐵), (𝐻‘((𝐹 ↾ suc 𝐵)‘∪ dom
(𝐹 ↾ suc 𝐵)))))) |
76 | 6, 75, 57 | 3eqtrd 2660 |
1
⊢ (suc
𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹‘𝐵))) |