Proof of Theorem rdgruledefgg
Step | Hyp | Ref
| Expression |
1 | | elex 2560 |
. 2
⊢ (A ∈ 𝑉 → A ∈
V) |
2 | | funmpt 4881 |
. . . 4
⊢ Fun
(g ∈ V
↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))) |
3 | | vex 2554 |
. . . . 5
⊢ f ∈
V |
4 | | vex 2554 |
. . . . . . . . . . . . 13
⊢ g ∈
V |
5 | | vex 2554 |
. . . . . . . . . . . . 13
⊢ x ∈
V |
6 | 4, 5 | fvex 5138 |
. . . . . . . . . . . 12
⊢ (g‘x) ∈ V |
7 | | funfvex 5135 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ (g‘x) ∈ dom 𝐹) → (𝐹‘(g‘x))
∈ V) |
8 | 7 | funfni 4942 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn V ∧ (g‘x) ∈ V) → (𝐹‘(g‘x))
∈ V) |
9 | 6, 8 | mpan2 401 |
. . . . . . . . . . 11
⊢ (𝐹 Fn V → (𝐹‘(g‘x))
∈ V) |
10 | 9 | ralrimivw 2387 |
. . . . . . . . . 10
⊢ (𝐹 Fn V → ∀x ∈ dom g(𝐹‘(g‘x))
∈ V) |
11 | 4 | dmex 4541 |
. . . . . . . . . . 11
⊢ dom
g ∈
V |
12 | | iunexg 5688 |
. . . . . . . . . . 11
⊢ ((dom
g ∈ V
∧ ∀x ∈ dom g(𝐹‘(g‘x))
∈ V) → ∪ x ∈ dom g(𝐹‘(g‘x))
∈ V) |
13 | 11, 12 | mpan 400 |
. . . . . . . . . 10
⊢ (∀x ∈ dom g(𝐹‘(g‘x))
∈ V → ∪ x ∈ dom g(𝐹‘(g‘x))
∈ V) |
14 | 10, 13 | syl 14 |
. . . . . . . . 9
⊢ (𝐹 Fn V → ∪ x ∈ dom g(𝐹‘(g‘x))
∈ V) |
15 | | unexg 4144 |
. . . . . . . . 9
⊢
((A ∈ V ∧ ∪ x ∈ dom g(𝐹‘(g‘x))
∈ V) → (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))
∈ V) |
16 | 14, 15 | sylan2 270 |
. . . . . . . 8
⊢
((A ∈ V ∧ 𝐹 Fn V) → (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))
∈ V) |
17 | 16 | ancoms 255 |
. . . . . . 7
⊢ ((𝐹 Fn V ∧ A ∈ V) → (A
∪ ∪ x
∈ dom g(𝐹‘(g‘x)))
∈ V) |
18 | 17 | ralrimivw 2387 |
. . . . . 6
⊢ ((𝐹 Fn V ∧ A ∈ V) → ∀g ∈ V (A ∪
∪ x ∈ dom g(𝐹‘(g‘x)))
∈ V) |
19 | | dmmptg 4761 |
. . . . . 6
⊢ (∀g ∈ V (A ∪
∪ x ∈ dom g(𝐹‘(g‘x)))
∈ V → dom (g ∈ V ↦
(A ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))) =
V) |
20 | 18, 19 | syl 14 |
. . . . 5
⊢ ((𝐹 Fn V ∧ A ∈ V) → dom (g ∈ V ↦
(A ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))) =
V) |
21 | 3, 20 | syl5eleqr 2124 |
. . . 4
⊢ ((𝐹 Fn V ∧ A ∈ V) → f
∈ dom (g
∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))) |
22 | | funfvex 5135 |
. . . 4
⊢ ((Fun
(g ∈ V
↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))
∧ f ∈ dom (g ∈ V ↦ (A
∪ ∪ x
∈ dom g(𝐹‘(g‘x)))))
→ ((g ∈ V ↦ (A
∪ ∪ x
∈ dom g(𝐹‘(g‘x))))‘f)
∈ V) |
23 | 2, 21, 22 | sylancr 393 |
. . 3
⊢ ((𝐹 Fn V ∧ A ∈ V) → ((g
∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))‘f)
∈ V) |
24 | 23, 2 | jctil 295 |
. 2
⊢ ((𝐹 Fn V ∧ A ∈ V) → (Fun (g ∈ V ↦
(A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))
∧ ((g
∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))‘f)
∈ V)) |
25 | 1, 24 | sylan2 270 |
1
⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → (Fun (g ∈ V ↦
(A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))
∧ ((g
∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))‘f)
∈ V)) |