Step |
Hyp |
Ref |
Expression |
1 |
|
uniiun |
⊢ ∪ 𝐵 = ∪ 𝑦 ∈ 𝐵 𝑦 |
2 |
|
elun1 |
⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( 𝐵 ∪ { ∅ } ) ) |
3 |
|
foelrni |
⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝑦 ∈ ( 𝐵 ∪ { ∅ } ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) |
4 |
2 3
|
sylan2 |
⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) |
5 |
|
eqimss2 |
⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) ) |
6 |
5
|
reximi |
⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 → ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) ) |
7 |
4 6
|
syl |
⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) ) |
8 |
7
|
ralrimiva |
⊢ ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) ) |
9 |
|
iunss2 |
⊢ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) → ∪ 𝑦 ∈ 𝐵 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ) |
10 |
8 9
|
syl |
⊢ ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) → ∪ 𝑦 ∈ 𝐵 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ) |
11 |
|
simpl |
⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝐵 = ∅ ) → 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ) |
12 |
|
uneq1 |
⊢ ( 𝐵 = ∅ → ( 𝐵 ∪ { ∅ } ) = ( ∅ ∪ { ∅ } ) ) |
13 |
|
0un |
⊢ ( ∅ ∪ { ∅ } ) = { ∅ } |
14 |
12 13
|
eqtrdi |
⊢ ( 𝐵 = ∅ → ( 𝐵 ∪ { ∅ } ) = { ∅ } ) |
15 |
14
|
adantl |
⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝐵 = ∅ ) → ( 𝐵 ∪ { ∅ } ) = { ∅ } ) |
16 |
|
foeq3 |
⊢ ( ( 𝐵 ∪ { ∅ } ) = { ∅ } → ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ↔ 𝐹 : 𝐴 –onto→ { ∅ } ) ) |
17 |
15 16
|
syl |
⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝐵 = ∅ ) → ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ↔ 𝐹 : 𝐴 –onto→ { ∅ } ) ) |
18 |
11 17
|
mpbid |
⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝐵 = ∅ ) → 𝐹 : 𝐴 –onto→ { ∅ } ) |
19 |
|
founiiun |
⊢ ( 𝐹 : 𝐴 –onto→ { ∅ } → ∪ { ∅ } = ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ) |
20 |
|
unisn0 |
⊢ ∪ { ∅ } = ∅ |
21 |
19 20
|
eqtr3di |
⊢ ( 𝐹 : 𝐴 –onto→ { ∅ } → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∅ ) |
22 |
|
0ss |
⊢ ∅ ⊆ ∪ 𝑦 ∈ 𝐵 𝑦 |
23 |
21 22
|
eqsstrdi |
⊢ ( 𝐹 : 𝐴 –onto→ { ∅ } → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 𝑦 ) |
24 |
18 23
|
syl |
⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝐵 = ∅ ) → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 𝑦 ) |
25 |
|
ssid |
⊢ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) |
26 |
|
sseq2 |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ) |
27 |
26
|
rspcev |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) |
28 |
25 27
|
mpan2 |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) |
29 |
28
|
adantl |
⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) |
30 |
|
fof |
⊢ ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) → 𝐹 : 𝐴 ⟶ ( 𝐵 ∪ { ∅ } ) ) |
31 |
30
|
ffvelrnda |
⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐵 ∪ { ∅ } ) ) |
32 |
|
elunnel1 |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐵 ∪ { ∅ } ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ { ∅ } ) |
33 |
31 32
|
sylan |
⊢ ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ { ∅ } ) |
34 |
|
elsni |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ { ∅ } → ( 𝐹 ‘ 𝑥 ) = ∅ ) |
35 |
33 34
|
syl |
⊢ ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ∅ ) |
36 |
35
|
adantllr |
⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ∅ ) |
37 |
|
neq0 |
⊢ ( ¬ 𝐵 = ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐵 ) |
38 |
37
|
biimpi |
⊢ ( ¬ 𝐵 = ∅ → ∃ 𝑦 𝑦 ∈ 𝐵 ) |
39 |
38
|
adantr |
⊢ ( ( ¬ 𝐵 = ∅ ∧ ( 𝐹 ‘ 𝑥 ) = ∅ ) → ∃ 𝑦 𝑦 ∈ 𝐵 ) |
40 |
|
id |
⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → ( 𝐹 ‘ 𝑥 ) = ∅ ) |
41 |
|
0ss |
⊢ ∅ ⊆ 𝑦 |
42 |
40 41
|
eqsstrdi |
⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) |
43 |
42
|
anim1ci |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) = ∅ ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) ) |
44 |
43
|
ex |
⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → ( 𝑦 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) ) ) |
45 |
44
|
adantl |
⊢ ( ( ¬ 𝐵 = ∅ ∧ ( 𝐹 ‘ 𝑥 ) = ∅ ) → ( 𝑦 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) ) ) |
46 |
45
|
eximdv |
⊢ ( ( ¬ 𝐵 = ∅ ∧ ( 𝐹 ‘ 𝑥 ) = ∅ ) → ( ∃ 𝑦 𝑦 ∈ 𝐵 → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) ) ) |
47 |
39 46
|
mpd |
⊢ ( ( ¬ 𝐵 = ∅ ∧ ( 𝐹 ‘ 𝑥 ) = ∅ ) → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) ) |
48 |
|
df-rex |
⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) ) |
49 |
47 48
|
sylibr |
⊢ ( ( ¬ 𝐵 = ∅ ∧ ( 𝐹 ‘ 𝑥 ) = ∅ ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) |
50 |
49
|
ad4ant24 |
⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ∅ ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) |
51 |
36 50
|
syldan |
⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) |
52 |
29 51
|
pm2.61dan |
⊢ ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) |
53 |
52
|
ralrimiva |
⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) |
54 |
|
iunss2 |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 𝑦 ) |
55 |
53 54
|
syl |
⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 𝑦 ) |
56 |
24 55
|
pm2.61dan |
⊢ ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 𝑦 ) |
57 |
10 56
|
eqssd |
⊢ ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) → ∪ 𝑦 ∈ 𝐵 𝑦 = ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ) |
58 |
1 57
|
syl5eq |
⊢ ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ) |