Step | Hyp | Ref
| Expression |
1 | | simp2l 1192 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦)) ∧ (𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) → 𝐺 Fn 𝐴) |
2 | | simp1 1129 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦)) ∧ (𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) → 𝐴 ∈ 𝑉) |
3 | | fnex 6853 |
. . . 4
⊢ ((𝐺 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐺 ∈ V) |
4 | 1, 2, 3 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦)) ∧ (𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) → 𝐺 ∈ V) |
5 | | simp2r 1193 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦)) ∧ (𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) → ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦)) |
6 | | difeq2 4020 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝐴 ∖ 𝑤) = (𝐴 ∖ 𝑊)) |
7 | 6 | raleqdv 3377 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (∀𝑦 ∈ (𝐴 ∖ 𝑤)(𝐺‘𝑦) = ∪ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) |
8 | 7 | rspcev 3561 |
. . . . 5
⊢ ((𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦)) → ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(𝐺‘𝑦) = ∪ (𝐹‘𝑦)) |
9 | 8 | 3ad2ant3 1128 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦)) ∧ (𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) → ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(𝐺‘𝑦) = ∪ (𝐹‘𝑦)) |
10 | 1, 5, 9 | 3jca 1121 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦)) ∧ (𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) → (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) |
11 | | fveq1 6544 |
. . . . . . 7
⊢ (ℎ = 𝐺 → (ℎ‘𝑦) = (𝐺‘𝑦)) |
12 | 11 | eqcomd 2803 |
. . . . . 6
⊢ (ℎ = 𝐺 → (𝐺‘𝑦) = (ℎ‘𝑦)) |
13 | 12 | ixpeq2dv 8333 |
. . . . 5
⊢ (ℎ = 𝐺 → X𝑦 ∈ 𝐴 (𝐺‘𝑦) = X𝑦 ∈ 𝐴 (ℎ‘𝑦)) |
14 | 13 | biantrud 532 |
. . . 4
⊢ (ℎ = 𝐺 → ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ↔ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ X𝑦 ∈ 𝐴 (𝐺‘𝑦) = X𝑦 ∈ 𝐴 (ℎ‘𝑦)))) |
15 | | fneq1 6321 |
. . . . 5
⊢ (ℎ = 𝐺 → (ℎ Fn 𝐴 ↔ 𝐺 Fn 𝐴)) |
16 | 11 | eleq1d 2869 |
. . . . . 6
⊢ (ℎ = 𝐺 → ((ℎ‘𝑦) ∈ (𝐹‘𝑦) ↔ (𝐺‘𝑦) ∈ (𝐹‘𝑦))) |
17 | 16 | ralbidv 3166 |
. . . . 5
⊢ (ℎ = 𝐺 → (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦))) |
18 | 11 | eqeq1d 2799 |
. . . . . 6
⊢ (ℎ = 𝐺 → ((ℎ‘𝑦) = ∪ (𝐹‘𝑦) ↔ (𝐺‘𝑦) = ∪ (𝐹‘𝑦))) |
19 | 18 | rexralbidv 3266 |
. . . . 5
⊢ (ℎ = 𝐺 → (∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ↔ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) |
20 | 15, 17, 19 | 3anbi123d 1428 |
. . . 4
⊢ (ℎ = 𝐺 → ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ↔ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(𝐺‘𝑦) = ∪ (𝐹‘𝑦)))) |
21 | 14, 20 | bitr3d 282 |
. . 3
⊢ (ℎ = 𝐺 → (((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ X𝑦 ∈ 𝐴 (𝐺‘𝑦) = X𝑦 ∈ 𝐴 (ℎ‘𝑦)) ↔ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(𝐺‘𝑦) = ∪ (𝐹‘𝑦)))) |
22 | 4, 10, 21 | elabd 3609 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦)) ∧ (𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) → ∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ X𝑦 ∈ 𝐴 (𝐺‘𝑦) = X𝑦 ∈ 𝐴 (ℎ‘𝑦))) |
23 | | ptbas.1 |
. . 3
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} |
24 | 23 | elpt 21868 |
. 2
⊢ (X𝑦 ∈
𝐴 (𝐺‘𝑦) ∈ 𝐵 ↔ ∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ X𝑦 ∈ 𝐴 (𝐺‘𝑦) = X𝑦 ∈ 𝐴 (ℎ‘𝑦))) |
25 | 22, 24 | sylibr 235 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦)) ∧ (𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ 𝐵) |