Step | Hyp | Ref
| Expression |
1 | | uniiun 4509 |
. . 3
⊢ ∪ 𝐵 =
∪ 𝑦 ∈ 𝐵 𝑦 |
2 | 1 | a1i 11 |
. 2
⊢ (𝐹:𝐴–onto→𝐵 → ∪ 𝐵 = ∪ 𝑦 ∈ 𝐵 𝑦) |
3 | | simpl 472 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑦 ∈ 𝐵) → 𝐹:𝐴–onto→𝐵) |
4 | | simpr 476 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
5 | | foelrni 6154 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦) |
6 | 3, 4, 5 | syl2anc 691 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦) |
7 | | eqimss2 3621 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) = 𝑦 → 𝑦 ⊆ (𝐹‘𝑥)) |
8 | 7 | reximi 2994 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 (𝐹‘𝑥) = 𝑦 → ∃𝑥 ∈ 𝐴 𝑦 ⊆ (𝐹‘𝑥)) |
9 | 8 | a1i 11 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → ∃𝑥 ∈ 𝐴 𝑦 ⊆ (𝐹‘𝑥))) |
10 | 6, 9 | mpd 15 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ⊆ (𝐹‘𝑥)) |
11 | 10 | ralrimiva 2949 |
. . . 4
⊢ (𝐹:𝐴–onto→𝐵 → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 ⊆ (𝐹‘𝑥)) |
12 | | iunss2 4501 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 ∃𝑥 ∈ 𝐴 𝑦 ⊆ (𝐹‘𝑥) → ∪
𝑦 ∈ 𝐵 𝑦 ⊆ ∪
𝑥 ∈ 𝐴 (𝐹‘𝑥)) |
13 | 11, 12 | syl 17 |
. . 3
⊢ (𝐹:𝐴–onto→𝐵 → ∪
𝑦 ∈ 𝐵 𝑦 ⊆ ∪
𝑥 ∈ 𝐴 (𝐹‘𝑥)) |
14 | | fof 6028 |
. . . . . . 7
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
15 | 14 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
16 | | ssid 3587 |
. . . . . . 7
⊢ (𝐹‘𝑥) ⊆ (𝐹‘𝑥) |
17 | 16 | a1i 11 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ⊆ (𝐹‘𝑥)) |
18 | | sseq2 3590 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝑥) → ((𝐹‘𝑥) ⊆ 𝑦 ↔ (𝐹‘𝑥) ⊆ (𝐹‘𝑥))) |
19 | 18 | rspcev 3282 |
. . . . . 6
⊢ (((𝐹‘𝑥) ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ (𝐹‘𝑥)) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
20 | 15, 17, 19 | syl2anc 691 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
21 | 20 | ralrimiva 2949 |
. . . 4
⊢ (𝐹:𝐴–onto→𝐵 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
22 | | iunss2 4501 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦 → ∪
𝑥 ∈ 𝐴 (𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝐵 𝑦) |
23 | 21, 22 | syl 17 |
. . 3
⊢ (𝐹:𝐴–onto→𝐵 → ∪
𝑥 ∈ 𝐴 (𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝐵 𝑦) |
24 | 13, 23 | eqssd 3585 |
. 2
⊢ (𝐹:𝐴–onto→𝐵 → ∪
𝑦 ∈ 𝐵 𝑦 = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) |
25 | 2, 24 | eqtrd 2644 |
1
⊢ (𝐹:𝐴–onto→𝐵 → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) |