Step | Hyp | Ref
| Expression |
1 | | uniiun 4793 |
. . 3
⊢ ∪ 𝐵 =
∪ 𝑦 ∈ 𝐵 𝑦 |
2 | 1 | a1i 11 |
. 2
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝐵 =
∪ 𝑦 ∈ 𝐵 𝑦) |
3 | | simpl 476 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑦 ∈ 𝐵) → 𝐹:𝐴–onto→(𝐵 ∪ {∅})) |
4 | | elun1 4007 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ (𝐵 ∪ {∅})) |
5 | 4 | adantl 475 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ (𝐵 ∪ {∅})) |
6 | | foelrni 6491 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑦 ∈ (𝐵 ∪ {∅})) → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦) |
7 | 3, 5, 6 | syl2anc 581 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦) |
8 | | eqimss2 3883 |
. . . . . . 7
⊢ ((𝐹‘𝑥) = 𝑦 → 𝑦 ⊆ (𝐹‘𝑥)) |
9 | 8 | reximi 3219 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 (𝐹‘𝑥) = 𝑦 → ∃𝑥 ∈ 𝐴 𝑦 ⊆ (𝐹‘𝑥)) |
10 | 7, 9 | syl 17 |
. . . . 5
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ⊆ (𝐹‘𝑥)) |
11 | 10 | ralrimiva 3175 |
. . . 4
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 ⊆ (𝐹‘𝑥)) |
12 | | iunss2 4785 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 ∃𝑥 ∈ 𝐴 𝑦 ⊆ (𝐹‘𝑥) → ∪
𝑦 ∈ 𝐵 𝑦 ⊆ ∪
𝑥 ∈ 𝐴 (𝐹‘𝑥)) |
13 | 11, 12 | syl 17 |
. . 3
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝑦 ∈ 𝐵 𝑦 ⊆ ∪
𝑥 ∈ 𝐴 (𝐹‘𝑥)) |
14 | | simpl 476 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝐵 = ∅) → 𝐹:𝐴–onto→(𝐵 ∪ {∅})) |
15 | | uneq1 3987 |
. . . . . . . . 9
⊢ (𝐵 = ∅ → (𝐵 ∪ {∅}) = (∅
∪ {∅})) |
16 | | 0un 40032 |
. . . . . . . . . 10
⊢ (∅
∪ {∅}) = {∅} |
17 | 16 | a1i 11 |
. . . . . . . . 9
⊢ (𝐵 = ∅ → (∅ ∪
{∅}) = {∅}) |
18 | 15, 17 | eqtrd 2861 |
. . . . . . . 8
⊢ (𝐵 = ∅ → (𝐵 ∪ {∅}) =
{∅}) |
19 | 18 | adantl 475 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝐵 = ∅) → (𝐵 ∪ {∅}) =
{∅}) |
20 | | foeq3 6351 |
. . . . . . 7
⊢ ((𝐵 ∪ {∅}) = {∅}
→ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) ↔ 𝐹:𝐴–onto→{∅})) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝐵 = ∅) → (𝐹:𝐴–onto→(𝐵 ∪ {∅}) ↔ 𝐹:𝐴–onto→{∅})) |
22 | 14, 21 | mpbid 224 |
. . . . 5
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝐵 = ∅) → 𝐹:𝐴–onto→{∅}) |
23 | | unisn0 40039 |
. . . . . . . . 9
⊢ ∪ {∅} = ∅ |
24 | 23 | eqcomi 2834 |
. . . . . . . 8
⊢ ∅ =
∪ {∅} |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ (𝐹:𝐴–onto→{∅} → ∅ = ∪ {∅}) |
26 | | founiiun 40169 |
. . . . . . 7
⊢ (𝐹:𝐴–onto→{∅} → ∪
{∅} = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) |
27 | 25, 26 | eqtr2d 2862 |
. . . . . 6
⊢ (𝐹:𝐴–onto→{∅} → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∅) |
28 | | 0ss 4197 |
. . . . . . 7
⊢ ∅
⊆ ∪ 𝑦 ∈ 𝐵 𝑦 |
29 | 28 | a1i 11 |
. . . . . 6
⊢ (𝐹:𝐴–onto→{∅} → ∅ ⊆ ∪ 𝑦 ∈ 𝐵 𝑦) |
30 | 27, 29 | eqsstrd 3864 |
. . . . 5
⊢ (𝐹:𝐴–onto→{∅} → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝐵 𝑦) |
31 | 22, 30 | syl 17 |
. . . 4
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝐵 = ∅) → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝐵 𝑦) |
32 | | ssid 3848 |
. . . . . . . . 9
⊢ (𝐹‘𝑥) ⊆ (𝐹‘𝑥) |
33 | | sseq2 3852 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑥) → ((𝐹‘𝑥) ⊆ 𝑦 ↔ (𝐹‘𝑥) ⊆ (𝐹‘𝑥))) |
34 | 33 | rspcev 3526 |
. . . . . . . . 9
⊢ (((𝐹‘𝑥) ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ (𝐹‘𝑥)) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
35 | 32, 34 | mpan2 684 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ 𝐵 → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
36 | 35 | adantl 475 |
. . . . . . 7
⊢ ((((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ (𝐹‘𝑥) ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
37 | | simpl 476 |
. . . . . . . 8
⊢ ((((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ ¬ (𝐹‘𝑥) ∈ 𝐵) → ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) ∧ 𝑥 ∈ 𝐴)) |
38 | | fof 6353 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → 𝐹:𝐴⟶(𝐵 ∪ {∅})) |
39 | 38 | ffvelrnda 6608 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝐵 ∪ {∅})) |
40 | 39 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑥 ∈ 𝐴) ∧ ¬ (𝐹‘𝑥) ∈ 𝐵) → (𝐹‘𝑥) ∈ (𝐵 ∪ {∅})) |
41 | | simpr 479 |
. . . . . . . . . . 11
⊢ (((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑥 ∈ 𝐴) ∧ ¬ (𝐹‘𝑥) ∈ 𝐵) → ¬ (𝐹‘𝑥) ∈ 𝐵) |
42 | | elunnel1 3981 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) ∈ (𝐵 ∪ {∅}) ∧ ¬ (𝐹‘𝑥) ∈ 𝐵) → (𝐹‘𝑥) ∈ {∅}) |
43 | 40, 41, 42 | syl2anc 581 |
. . . . . . . . . 10
⊢ (((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑥 ∈ 𝐴) ∧ ¬ (𝐹‘𝑥) ∈ 𝐵) → (𝐹‘𝑥) ∈ {∅}) |
44 | | elsni 4414 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ {∅} → (𝐹‘𝑥) = ∅) |
45 | 43, 44 | syl 17 |
. . . . . . . . 9
⊢ (((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ 𝑥 ∈ 𝐴) ∧ ¬ (𝐹‘𝑥) ∈ 𝐵) → (𝐹‘𝑥) = ∅) |
46 | 45 | adantllr 712 |
. . . . . . . 8
⊢ ((((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ ¬ (𝐹‘𝑥) ∈ 𝐵) → (𝐹‘𝑥) = ∅) |
47 | | neq0 4159 |
. . . . . . . . . . . . 13
⊢ (¬
𝐵 = ∅ ↔
∃𝑦 𝑦 ∈ 𝐵) |
48 | 47 | biimpi 208 |
. . . . . . . . . . . 12
⊢ (¬
𝐵 = ∅ →
∃𝑦 𝑦 ∈ 𝐵) |
49 | 48 | adantr 474 |
. . . . . . . . . . 11
⊢ ((¬
𝐵 = ∅ ∧ (𝐹‘𝑥) = ∅) → ∃𝑦 𝑦 ∈ 𝐵) |
50 | | simpr 479 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑥) = ∅ ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
51 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑥) = ∅ → (𝐹‘𝑥) = ∅) |
52 | | 0ss 4197 |
. . . . . . . . . . . . . . . . . 18
⊢ ∅
⊆ 𝑦 |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑥) = ∅ → ∅ ⊆ 𝑦) |
54 | 51, 53 | eqsstrd 3864 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) = ∅ → (𝐹‘𝑥) ⊆ 𝑦) |
55 | 54 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑥) = ∅ ∧ 𝑦 ∈ 𝐵) → (𝐹‘𝑥) ⊆ 𝑦) |
56 | 50, 55 | jca 509 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑥) = ∅ ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ 𝑦)) |
57 | 56 | ex 403 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥) = ∅ → (𝑦 ∈ 𝐵 → (𝑦 ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ 𝑦))) |
58 | 57 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((¬
𝐵 = ∅ ∧ (𝐹‘𝑥) = ∅) → (𝑦 ∈ 𝐵 → (𝑦 ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ 𝑦))) |
59 | 58 | eximdv 2018 |
. . . . . . . . . . 11
⊢ ((¬
𝐵 = ∅ ∧ (𝐹‘𝑥) = ∅) → (∃𝑦 𝑦 ∈ 𝐵 → ∃𝑦(𝑦 ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ 𝑦))) |
60 | 49, 59 | mpd 15 |
. . . . . . . . . 10
⊢ ((¬
𝐵 = ∅ ∧ (𝐹‘𝑥) = ∅) → ∃𝑦(𝑦 ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ 𝑦)) |
61 | | df-rex 3123 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈
𝐵 (𝐹‘𝑥) ⊆ 𝑦 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ (𝐹‘𝑥) ⊆ 𝑦)) |
62 | 60, 61 | sylibr 226 |
. . . . . . . . 9
⊢ ((¬
𝐵 = ∅ ∧ (𝐹‘𝑥) = ∅) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
63 | 62 | ad4ant24 765 |
. . . . . . . 8
⊢ ((((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ (𝐹‘𝑥) = ∅) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
64 | 37, 46, 63 | syl2anc 581 |
. . . . . . 7
⊢ ((((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ ¬ (𝐹‘𝑥) ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
65 | 36, 64 | pm2.61dan 849 |
. . . . . 6
⊢ (((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
66 | 65 | ralrimiva 3175 |
. . . . 5
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦) |
67 | | iunss2 4785 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 (𝐹‘𝑥) ⊆ 𝑦 → ∪
𝑥 ∈ 𝐴 (𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝐵 𝑦) |
68 | 66, 67 | syl 17 |
. . . 4
⊢ ((𝐹:𝐴–onto→(𝐵 ∪ {∅}) ∧ ¬ 𝐵 = ∅) → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝐵 𝑦) |
69 | 31, 68 | pm2.61dan 849 |
. . 3
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝐵 𝑦) |
70 | 13, 69 | eqssd 3844 |
. 2
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝑦 ∈ 𝐵 𝑦 = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) |
71 | 2, 70 | eqtrd 2861 |
1
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝐵 =
∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) |