Proof of Theorem rdgruledefgg
Step | Hyp | Ref
| Expression |
1 | | elex 2741 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | | funmpt 5236 |
. . . 4
⊢ Fun
(𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) |
3 | | vex 2733 |
. . . . 5
⊢ 𝑓 ∈ V |
4 | | vex 2733 |
. . . . . . . . . . . . 13
⊢ 𝑔 ∈ V |
5 | | vex 2733 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
6 | 4, 5 | fvex 5516 |
. . . . . . . . . . . 12
⊢ (𝑔‘𝑥) ∈ V |
7 | | funfvex 5513 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ (𝑔‘𝑥) ∈ dom 𝐹) → (𝐹‘(𝑔‘𝑥)) ∈ V) |
8 | 7 | funfni 5298 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn V ∧ (𝑔‘𝑥) ∈ V) → (𝐹‘(𝑔‘𝑥)) ∈ V) |
9 | 6, 8 | mpan2 423 |
. . . . . . . . . . 11
⊢ (𝐹 Fn V → (𝐹‘(𝑔‘𝑥)) ∈ V) |
10 | 9 | ralrimivw 2544 |
. . . . . . . . . 10
⊢ (𝐹 Fn V → ∀𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)) ∈ V) |
11 | 4 | dmex 4877 |
. . . . . . . . . . 11
⊢ dom 𝑔 ∈ V |
12 | | iunexg 6098 |
. . . . . . . . . . 11
⊢ ((dom
𝑔 ∈ V ∧
∀𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)) ∈ V) → ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)) ∈ V) |
13 | 11, 12 | mpan 422 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
dom 𝑔(𝐹‘(𝑔‘𝑥)) ∈ V → ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)) ∈ V) |
14 | 10, 13 | syl 14 |
. . . . . . . . 9
⊢ (𝐹 Fn V → ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)) ∈ V) |
15 | | unexg 4428 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)) ∈ V) → (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))) ∈ V) |
16 | 14, 15 | sylan2 284 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn V) → (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))) ∈ V) |
17 | 16 | ancoms 266 |
. . . . . . 7
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ V) → (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))) ∈ V) |
18 | 17 | ralrimivw 2544 |
. . . . . 6
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ V) → ∀𝑔 ∈ V (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))) ∈ V) |
19 | | dmmptg 5108 |
. . . . . 6
⊢
(∀𝑔 ∈ V
(𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))) ∈ V → dom (𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) = V) |
20 | 18, 19 | syl 14 |
. . . . 5
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ V) → dom (𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) = V) |
21 | 3, 20 | eleqtrrid 2260 |
. . . 4
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ V) → 𝑓 ∈ dom (𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))) |
22 | | funfvex 5513 |
. . . 4
⊢ ((Fun
(𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) ∧ 𝑓 ∈ dom (𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))) → ((𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘𝑓) ∈ V) |
23 | 2, 21, 22 | sylancr 412 |
. . 3
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ V) → ((𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘𝑓) ∈ V) |
24 | 23, 2 | jctil 310 |
. 2
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ V) → (Fun (𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘𝑓) ∈ V)) |
25 | 1, 24 | sylan2 284 |
1
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉) → (Fun (𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪
𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘𝑓) ∈ V)) |