Step | Hyp | Ref
| Expression |
1 | | df-irdg 6329 |
. . . 4
⊢ rec(𝐹, 𝐴) = recs((𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))) |
2 | | rdgruledefgg 6334 |
. . . . 5
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉) → (Fun (𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘𝑦) ∈ V)) |
3 | 2 | alrimiv 1861 |
. . . 4
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉) → ∀𝑦(Fun (𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘𝑦) ∈ V)) |
4 | 1, 3 | tfri2d 6295 |
. . 3
⊢ (((𝐹 Fn V ∧ 𝐴 ∈ 𝑉) ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = ((𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘(rec(𝐹, 𝐴) ↾ 𝐵))) |
5 | 4 | 3impa 1183 |
. 2
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = ((𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘(rec(𝐹, 𝐴) ↾ 𝐵))) |
6 | | eqidd 2165 |
. . 3
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → (𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) = (𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))) |
7 | | dmeq 4798 |
. . . . . 6
⊢ (𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵) → dom 𝑔 = dom (rec(𝐹, 𝐴) ↾ 𝐵)) |
8 | | onss 4464 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → 𝐵 ⊆ On) |
9 | 8 | 3ad2ant3 1009 |
. . . . . . . 8
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → 𝐵 ⊆ On) |
10 | | rdgifnon 6338 |
. . . . . . . . . 10
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉) → rec(𝐹, 𝐴) Fn On) |
11 | | fndm 5281 |
. . . . . . . . . 10
⊢
(rec(𝐹, 𝐴) Fn On → dom rec(𝐹, 𝐴) = On) |
12 | 10, 11 | syl 14 |
. . . . . . . . 9
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉) → dom rec(𝐹, 𝐴) = On) |
13 | 12 | 3adant3 1006 |
. . . . . . . 8
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → dom rec(𝐹, 𝐴) = On) |
14 | 9, 13 | sseqtrrd 3176 |
. . . . . . 7
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → 𝐵 ⊆ dom rec(𝐹, 𝐴)) |
15 | | ssdmres 4900 |
. . . . . . 7
⊢ (𝐵 ⊆ dom rec(𝐹, 𝐴) ↔ dom (rec(𝐹, 𝐴) ↾ 𝐵) = 𝐵) |
16 | 14, 15 | sylib 121 |
. . . . . 6
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → dom (rec(𝐹, 𝐴) ↾ 𝐵) = 𝐵) |
17 | 7, 16 | sylan9eqr 2219 |
. . . . 5
⊢ (((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ 𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵)) → dom 𝑔 = 𝐵) |
18 | | fveq1 5479 |
. . . . . . 7
⊢ (𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵) → (𝑔‘𝑥) = ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) |
19 | 18 | fveq2d 5484 |
. . . . . 6
⊢ (𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵) → (𝐹‘(𝑔‘𝑥)) = (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) |
20 | 19 | adantl 275 |
. . . . 5
⊢ (((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ 𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵)) → (𝐹‘(𝑔‘𝑥)) = (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) |
21 | 17, 20 | iuneq12d 3884 |
. . . 4
⊢ (((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ 𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵)) → ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)) = ∪
𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) |
22 | 21 | uneq2d 3271 |
. . 3
⊢ (((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ 𝑔 = (rec(𝐹, 𝐴) ↾ 𝐵)) → (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))) = (𝐴 ∪ ∪
𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)))) |
23 | | rdgfun 6332 |
. . . . 5
⊢ Fun
rec(𝐹, 𝐴) |
24 | | resfunexg 5700 |
. . . . 5
⊢ ((Fun
rec(𝐹, 𝐴) ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V) |
25 | 23, 24 | mpan 421 |
. . . 4
⊢ (𝐵 ∈ On → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V) |
26 | 25 | 3ad2ant3 1009 |
. . 3
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V) |
27 | | simpr 109 |
. . . . . 6
⊢ ((𝐹 Fn V ∧ 𝐵 ∈ On) → 𝐵 ∈ On) |
28 | | vex 2724 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
29 | | fvexg 5499 |
. . . . . . . . . 10
⊢
(((rec(𝐹, 𝐴) ↾ 𝐵) ∈ V ∧ 𝑥 ∈ V) → ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V) |
30 | 25, 28, 29 | sylancl 410 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V) |
31 | 30 | ralrimivw 2538 |
. . . . . . . 8
⊢ (𝐵 ∈ On → ∀𝑥 ∈ 𝐵 ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V) |
32 | 31 | adantl 275 |
. . . . . . 7
⊢ ((𝐹 Fn V ∧ 𝐵 ∈ On) → ∀𝑥 ∈ 𝐵 ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V) |
33 | | funfvex 5497 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ dom 𝐹) → (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V) |
34 | 33 | funfni 5282 |
. . . . . . . . . 10
⊢ ((𝐹 Fn V ∧ ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V) → (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V) |
35 | 34 | ex 114 |
. . . . . . . . 9
⊢ (𝐹 Fn V → (((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V → (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)) |
36 | 35 | ralimdv 2532 |
. . . . . . . 8
⊢ (𝐹 Fn V → (∀𝑥 ∈ 𝐵 ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V → ∀𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)) |
37 | 36 | adantr 274 |
. . . . . . 7
⊢ ((𝐹 Fn V ∧ 𝐵 ∈ On) → (∀𝑥 ∈ 𝐵 ((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥) ∈ V → ∀𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V)) |
38 | 32, 37 | mpd 13 |
. . . . . 6
⊢ ((𝐹 Fn V ∧ 𝐵 ∈ On) → ∀𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V) |
39 | | iunexg 6079 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ ∀𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V) → ∪ 𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V) |
40 | 27, 38, 39 | syl2anc 409 |
. . . . 5
⊢ ((𝐹 Fn V ∧ 𝐵 ∈ On) → ∪ 𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V) |
41 | 40 | 3adant2 1005 |
. . . 4
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → ∪ 𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V) |
42 | | unexg 4415 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V) → (𝐴 ∪ ∪
𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) ∈ V) |
43 | 42 | ex 114 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (∪
𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V → (𝐴 ∪ ∪
𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) ∈ V)) |
44 | 43 | 3ad2ant2 1008 |
. . . 4
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → (∪ 𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)) ∈ V → (𝐴 ∪ ∪
𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) ∈ V)) |
45 | 41, 44 | mpd 13 |
. . 3
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → (𝐴 ∪ ∪
𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))) ∈ V) |
46 | 6, 22, 26, 45 | fvmptd 5561 |
. 2
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → ((𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘(rec(𝐹, 𝐴) ↾ 𝐵)) = (𝐴 ∪ ∪
𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)))) |
47 | 5, 46 | eqtrd 2197 |
1
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = (𝐴 ∪ ∪
𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)))) |