Step | Hyp | Ref
| Expression |
1 | | eldm2g 4474 |
. . 3
⊢ (B ∈ dom recs(𝐹) → (B ∈ dom recs(𝐹) ↔ ∃z〈B,
z〉 ∈
recs(𝐹))) |
2 | 1 | ibi 165 |
. 2
⊢ (B ∈ dom recs(𝐹) → ∃z〈B,
z〉 ∈
recs(𝐹)) |
3 | | df-recs 5861 |
. . . . . 6
⊢
recs(𝐹) = ∪ {f ∣ ∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))} |
4 | 3 | eleq2i 2101 |
. . . . 5
⊢
(〈B, z〉 ∈
recs(𝐹) ↔
〈B, z〉 ∈ ∪ {f ∣ ∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))}) |
5 | | eluniab 3583 |
. . . . 5
⊢
(〈B, z〉 ∈ ∪ {f ∣ ∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))}
↔ ∃f(〈B,
z〉 ∈
f ∧ ∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))))) |
6 | 4, 5 | bitri 173 |
. . . 4
⊢
(〈B, z〉 ∈
recs(𝐹) ↔ ∃f(〈B,
z〉 ∈
f ∧ ∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))))) |
7 | | fnop 4945 |
. . . . . . . . . . . . . 14
⊢
((f Fn x ∧ 〈B, z〉 ∈ f) →
B ∈
x) |
8 | | rspe 2364 |
. . . . . . . . . . . . . . . 16
⊢
((x ∈ On ∧ (f Fn x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))))
→ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))) |
9 | | tfrlem.1 |
. . . . . . . . . . . . . . . . . 18
⊢ A = {f ∣
∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))} |
10 | 9 | abeq2i 2145 |
. . . . . . . . . . . . . . . . 17
⊢ (f ∈ A ↔ ∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))) |
11 | | elssuni 3599 |
. . . . . . . . . . . . . . . . . 18
⊢ (f ∈ A → f
⊆ ∪ A) |
12 | 9 | recsfval 5872 |
. . . . . . . . . . . . . . . . . 18
⊢
recs(𝐹) = ∪ A |
13 | 11, 12 | syl6sseqr 2986 |
. . . . . . . . . . . . . . . . 17
⊢ (f ∈ A → f
⊆ recs(𝐹)) |
14 | 10, 13 | sylbir 125 |
. . . . . . . . . . . . . . . 16
⊢ (∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))
→ f ⊆ recs(𝐹)) |
15 | 8, 14 | syl 14 |
. . . . . . . . . . . . . . 15
⊢
((x ∈ On ∧ (f Fn x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))))
→ f ⊆ recs(𝐹)) |
16 | | fveq2 5121 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (y = B →
(f‘y) = (f‘B)) |
17 | | reseq2 4550 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (y = B →
(f ↾ y) = (f ↾
B)) |
18 | 17 | fveq2d 5125 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (y = B →
(𝐹‘(f ↾ y)) =
(𝐹‘(f ↾ B))) |
19 | 16, 18 | eqeq12d 2051 |
. . . . . . . . . . . . . . . . . . 19
⊢ (y = B →
((f‘y) = (𝐹‘(f ↾ y))
↔ (f‘B) = (𝐹‘(f ↾ B)))) |
20 | 19 | rspcv 2646 |
. . . . . . . . . . . . . . . . . 18
⊢ (B ∈ x → (∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))
→ (f‘B) = (𝐹‘(f ↾ B)))) |
21 | | fndm 4941 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (f Fn x →
dom f = x) |
22 | 21 | eleq2d 2104 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (f Fn x →
(B ∈ dom
f ↔ B ∈ x)) |
23 | 9 | tfrlem7 5874 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ Fun
recs(𝐹) |
24 | | funssfv 5142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Fun
recs(𝐹) ∧ f ⊆
recs(𝐹) ∧ B ∈ dom f) →
(recs(𝐹)‘B) = (f‘B)) |
25 | 23, 24 | mp3an1 1218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((f ⊆ recs(𝐹) ∧
B ∈ dom
f) → (recs(𝐹)‘B) = (f‘B)) |
26 | 25 | adantrl 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((f ⊆ recs(𝐹) ∧
((f Fn x ∧ x ∈ On) ∧ B ∈ dom f))
→ (recs(𝐹)‘B) = (f‘B)) |
27 | 21 | eleq1d 2103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (f Fn x →
(dom f ∈
On ↔ x ∈ On)) |
28 | | onelss 4090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (dom
f ∈ On
→ (B ∈ dom f →
B ⊆ dom f)) |
29 | 27, 28 | syl6bir 153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (f Fn x →
(x ∈ On
→ (B ∈ dom f →
B ⊆ dom f))) |
30 | 29 | imp31 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((f Fn x ∧ x ∈ On) ∧ B ∈ dom f) →
B ⊆ dom f) |
31 | | fun2ssres 4886 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((Fun
recs(𝐹) ∧ f ⊆
recs(𝐹) ∧ B ⊆ dom
f) → (recs(𝐹) ↾ B) = (f ↾
B)) |
32 | 31 | fveq2d 5125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Fun
recs(𝐹) ∧ f ⊆
recs(𝐹) ∧ B ⊆ dom
f) → (𝐹‘(recs(𝐹) ↾ B)) = (𝐹‘(f ↾ B))) |
33 | 23, 32 | mp3an1 1218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((f ⊆ recs(𝐹) ∧
B ⊆ dom f) → (𝐹‘(recs(𝐹) ↾ B)) = (𝐹‘(f ↾ B))) |
34 | 30, 33 | sylan2 270 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((f ⊆ recs(𝐹) ∧
((f Fn x ∧ x ∈ On) ∧ B ∈ dom f))
→ (𝐹‘(recs(𝐹) ↾ B)) = (𝐹‘(f ↾ B))) |
35 | 26, 34 | eqeq12d 2051 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((f ⊆ recs(𝐹) ∧
((f Fn x ∧ x ∈ On) ∧ B ∈ dom f))
→ ((recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B)) ↔ (f‘B) =
(𝐹‘(f ↾ B)))) |
36 | 35 | exbiri 364 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (f ⊆ recs(𝐹) → (((f Fn x ∧ x ∈ On) ∧ B ∈ dom f) → ((f‘B) =
(𝐹‘(f ↾ B))
→ (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))))) |
37 | 36 | com3l 75 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((f Fn x ∧ x ∈ On) ∧ B ∈ dom f) →
((f‘B) = (𝐹‘(f ↾ B))
→ (f ⊆ recs(𝐹) → (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))))) |
38 | 37 | exp31 346 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (f Fn x →
(x ∈ On
→ (B ∈ dom f →
((f‘B) = (𝐹‘(f ↾ B))
→ (f ⊆ recs(𝐹) → (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))))))) |
39 | 38 | com34 77 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (f Fn x →
(x ∈ On
→ ((f‘B) = (𝐹‘(f ↾ B))
→ (B ∈ dom f →
(f ⊆ recs(𝐹) → (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))))))) |
40 | 39 | com24 81 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (f Fn x →
(B ∈ dom
f → ((f‘B) =
(𝐹‘(f ↾ B))
→ (x ∈ On → (f
⊆ recs(𝐹) →
(recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))))))) |
41 | 22, 40 | sylbird 159 |
. . . . . . . . . . . . . . . . . . 19
⊢ (f Fn x →
(B ∈
x → ((f‘B) =
(𝐹‘(f ↾ B))
→ (x ∈ On → (f
⊆ recs(𝐹) →
(recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))))))) |
42 | 41 | com3l 75 |
. . . . . . . . . . . . . . . . . 18
⊢ (B ∈ x → ((f‘B) =
(𝐹‘(f ↾ B))
→ (f Fn x → (x
∈ On → (f ⊆ recs(𝐹) → (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))))))) |
43 | 20, 42 | syld 40 |
. . . . . . . . . . . . . . . . 17
⊢ (B ∈ x → (∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))
→ (f Fn x → (x
∈ On → (f ⊆ recs(𝐹) → (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))))))) |
44 | 43 | com24 81 |
. . . . . . . . . . . . . . . 16
⊢ (B ∈ x → (x
∈ On → (f Fn x →
(∀y
∈ x
(f‘y) = (𝐹‘(f ↾ y))
→ (f ⊆ recs(𝐹) → (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))))))) |
45 | 44 | imp4d 334 |
. . . . . . . . . . . . . . 15
⊢ (B ∈ x → ((x
∈ On ∧
(f Fn x
∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))))
→ (f ⊆ recs(𝐹) → (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))))) |
46 | 15, 45 | mpdi 38 |
. . . . . . . . . . . . . 14
⊢ (B ∈ x → ((x
∈ On ∧
(f Fn x
∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))))
→ (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B)))) |
47 | 7, 46 | syl 14 |
. . . . . . . . . . . . 13
⊢
((f Fn x ∧ 〈B, z〉 ∈ f) →
((x ∈ On
∧ (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))))
→ (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B)))) |
48 | 47 | exp4d 351 |
. . . . . . . . . . . 12
⊢
((f Fn x ∧ 〈B, z〉 ∈ f) →
(x ∈ On
→ (f Fn x → (∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))
→ (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B)))))) |
49 | 48 | ex 108 |
. . . . . . . . . . 11
⊢ (f Fn x →
(〈B, z〉 ∈ f → (x
∈ On → (f Fn x →
(∀y
∈ x
(f‘y) = (𝐹‘(f ↾ y))
→ (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))))))) |
50 | 49 | com4r 80 |
. . . . . . . . . 10
⊢ (f Fn x →
(f Fn x
→ (〈B, z〉 ∈ f → (x
∈ On → (∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))
→ (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))))))) |
51 | 50 | pm2.43i 43 |
. . . . . . . . 9
⊢ (f Fn x →
(〈B, z〉 ∈ f → (x
∈ On → (∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))
→ (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B)))))) |
52 | 51 | com3l 75 |
. . . . . . . 8
⊢
(〈B, z〉 ∈ f → (x
∈ On → (f Fn x →
(∀y
∈ x
(f‘y) = (𝐹‘(f ↾ y))
→ (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B)))))) |
53 | 52 | imp4a 331 |
. . . . . . 7
⊢
(〈B, z〉 ∈ f → (x
∈ On → ((f Fn x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))
→ (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))))) |
54 | 53 | rexlimdv 2426 |
. . . . . 6
⊢
(〈B, z〉 ∈ f → (∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))
→ (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B)))) |
55 | 54 | imp 115 |
. . . . 5
⊢
((〈B, z〉 ∈ f ∧ ∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))))
→ (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))) |
56 | 55 | exlimiv 1486 |
. . . 4
⊢ (∃f(〈B,
z〉 ∈
f ∧ ∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y))))
→ (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))) |
57 | 6, 56 | sylbi 114 |
. . 3
⊢
(〈B, z〉 ∈
recs(𝐹) → (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))) |
58 | 57 | exlimiv 1486 |
. 2
⊢ (∃z〈B,
z〉 ∈
recs(𝐹) → (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))) |
59 | 2, 58 | syl 14 |
1
⊢ (B ∈ dom recs(𝐹) → (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B))) |