Step | Hyp | Ref
| Expression |
1 | | uniiun 4988 |
. 2
⊢ ∪ 𝐵 =
∪ 𝑦 ∈ 𝐵 𝑦 |
2 | | elun1 4110 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ (𝐵 ∪ {∅})) |
3 | | foelrni 6831 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑦 ∈ (𝐵 ∪ {∅})) → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦) |
4 | 2, 3 | sylan2 593 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦) |
5 | | eqimss2 3978 |
. . . . . . 7
⊢ ((𝐹‘𝑥) = 𝑦 → 𝑦 ⊆ (𝐹‘𝑥)) |
6 | 5 | reximi 3178 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 (𝐹‘𝑥) = 𝑦 → ∃𝑥 ∈ 𝐴 𝑦 ⊆ (𝐹‘𝑥)) |
7 | 4, 6 | syl 17 |
. . . . 5
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ⊆ (𝐹‘𝑥)) |
8 | 7 | ralrimiva 3103 |
. . . 4
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 ⊆ (𝐹‘𝑥)) |
9 | | iunss2 4979 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 ∃𝑥 ∈ 𝐴 𝑦 ⊆ (𝐹‘𝑥) → ∪
𝑦 ∈ 𝐵 𝑦 ⊆ ∪
𝑥 ∈ 𝐴 (𝐹‘𝑥)) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝑦 ∈ 𝐵 𝑦 ⊆ ∪
𝑥 ∈ 𝐴 (𝐹‘𝑥)) |
11 | | simpl 483 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝐵 = ∅) → 𝐹:𝐴–onto→(𝐵 ∪ {∅})) |
12 | | uneq1 4090 |
. . . . . . . . 9
⊢ (𝐵 = ∅ → (𝐵 ∪ {∅}) = (∅
∪ {∅})) |
13 | | 0un 4326 |
. . . . . . . . 9
⊢ (∅
∪ {∅}) = {∅} |
14 | 12, 13 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝐵 = ∅ → (𝐵 ∪ {∅}) =
{∅}) |
15 | 14 | adantl 482 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝐵 = ∅) → (𝐵 ∪ {∅}) =
{∅}) |
16 | | foeq3 6686 |
. . . . . . 7
⊢ ((𝐵 ∪ {∅}) = {∅}
→ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) ↔ 𝐹:𝐴–onto→{∅})) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝐵 = ∅) → (𝐹:𝐴–onto→(𝐵 ∪ {∅}) ↔ 𝐹:𝐴–onto→{∅})) |
18 | 11, 17 | mpbid 231 |
. . . . 5
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝐵 = ∅) → 𝐹:𝐴–onto→{∅}) |
19 | | founiiun 42715 |
. . . . . . 7
⊢ (𝐹:𝐴–onto→{∅} → ∪
{∅} = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) |
20 | | unisn0 42602 |
. . . . . . 7
⊢ ∪ {∅} = ∅ |
21 | 19, 20 | eqtr3di 2793 |
. . . . . 6
⊢ (𝐹:𝐴–onto→{∅} → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∅) |
22 | | 0ss 4330 |
. . . . . 6
⊢ ∅
⊆ ∪ 𝑦 ∈ 𝐵 𝑦 |
23 | 21, 22 | eqsstrdi 3975 |
. . . . 5
⊢ (𝐹:𝐴–onto→{∅} → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝐵 𝑦) |
24 | 18, 23 | syl 17 |
. . . 4
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝐵 = ∅) → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝐵 𝑦) |
25 | | ssid 3943 |
. . . . . . . . 9
⊢ (𝐹‘𝑥) ⊆ (𝐹‘𝑥) |
26 | | sseq2 3947 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑥) → ((𝐹‘𝑥) ⊆ 𝑦 ↔ (𝐹‘𝑥) ⊆ (𝐹‘𝑥))) |
27 | 26 | rspcev 3561 |
. . . . . . . . 9
⊢ (((𝐹‘𝑥) ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ (𝐹‘𝑥)) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
28 | 25, 27 | mpan2 688 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ 𝐵 → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
29 | 28 | adantl 482 |
. . . . . . 7
⊢ ((((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ (𝐹‘𝑥) ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
30 | | fof 6688 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → 𝐹:𝐴⟶(𝐵 ∪ {∅})) |
31 | 30 | ffvelrnda 6961 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝐵 ∪ {∅})) |
32 | | elunnel1 4084 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) ∈ (𝐵 ∪ {∅}) ∧ ¬ (𝐹‘𝑥) ∈ 𝐵) → (𝐹‘𝑥) ∈ {∅}) |
33 | 31, 32 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑥 ∈ 𝐴) ∧ ¬ (𝐹‘𝑥) ∈ 𝐵) → (𝐹‘𝑥) ∈ {∅}) |
34 | | elsni 4578 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ {∅} → (𝐹‘𝑥) = ∅) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ (((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑥 ∈ 𝐴) ∧ ¬ (𝐹‘𝑥) ∈ 𝐵) → (𝐹‘𝑥) = ∅) |
36 | 35 | adantllr 716 |
. . . . . . . 8
⊢ ((((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ ¬ (𝐹‘𝑥) ∈ 𝐵) → (𝐹‘𝑥) = ∅) |
37 | | neq0 4279 |
. . . . . . . . . . . . 13
⊢ (¬
𝐵 = ∅ ↔
∃𝑦 𝑦 ∈ 𝐵) |
38 | 37 | biimpi 215 |
. . . . . . . . . . . 12
⊢ (¬
𝐵 = ∅ →
∃𝑦 𝑦 ∈ 𝐵) |
39 | 38 | adantr 481 |
. . . . . . . . . . 11
⊢ ((¬
𝐵 = ∅ ∧ (𝐹‘𝑥) = ∅) → ∃𝑦 𝑦 ∈ 𝐵) |
40 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) = ∅ → (𝐹‘𝑥) = ∅) |
41 | | 0ss 4330 |
. . . . . . . . . . . . . . . 16
⊢ ∅
⊆ 𝑦 |
42 | 40, 41 | eqsstrdi 3975 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑥) = ∅ → (𝐹‘𝑥) ⊆ 𝑦) |
43 | 42 | anim1ci 616 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑥) = ∅ ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ 𝑦)) |
44 | 43 | ex 413 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥) = ∅ → (𝑦 ∈ 𝐵 → (𝑦 ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ 𝑦))) |
45 | 44 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((¬
𝐵 = ∅ ∧ (𝐹‘𝑥) = ∅) → (𝑦 ∈ 𝐵 → (𝑦 ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ 𝑦))) |
46 | 45 | eximdv 1920 |
. . . . . . . . . . 11
⊢ ((¬
𝐵 = ∅ ∧ (𝐹‘𝑥) = ∅) → (∃𝑦 𝑦 ∈ 𝐵 → ∃𝑦(𝑦 ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ 𝑦))) |
47 | 39, 46 | mpd 15 |
. . . . . . . . . 10
⊢ ((¬
𝐵 = ∅ ∧ (𝐹‘𝑥) = ∅) → ∃𝑦(𝑦 ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ 𝑦)) |
48 | | df-rex 3070 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈
𝐵 (𝐹‘𝑥) ⊆ 𝑦 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ 𝑦)) |
49 | 47, 48 | sylibr 233 |
. . . . . . . . 9
⊢ ((¬
𝐵 = ∅ ∧ (𝐹‘𝑥) = ∅) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
50 | 49 | ad4ant24 751 |
. . . . . . . 8
⊢ ((((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ (𝐹‘𝑥) = ∅) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
51 | 36, 50 | syldan 591 |
. . . . . . 7
⊢ ((((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ ¬ (𝐹‘𝑥) ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
52 | 29, 51 | pm2.61dan 810 |
. . . . . 6
⊢ (((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
53 | 52 | ralrimiva 3103 |
. . . . 5
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
54 | | iunss2 4979 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦 → ∪
𝑥 ∈ 𝐴 (𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝐵 𝑦) |
55 | 53, 54 | syl 17 |
. . . 4
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝐵 𝑦) |
56 | 24, 55 | pm2.61dan 810 |
. . 3
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝐵 𝑦) |
57 | 10, 56 | eqssd 3938 |
. 2
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝑦 ∈ 𝐵 𝑦 = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) |
58 | 1, 57 | eqtrid 2790 |
1
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝐵 =
∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) |