Step |
Hyp |
Ref |
Expression |
1 |
|
brdom2 |
⊢ ( 𝐴 ≼ ℕ ↔ ( 𝐴 ≺ ℕ ∨ 𝐴 ≈ ℕ ) ) |
2 |
|
nnenom |
⊢ ℕ ≈ ω |
3 |
|
sdomentr |
⊢ ( ( 𝐴 ≺ ℕ ∧ ℕ ≈ ω ) → 𝐴 ≺ ω ) |
4 |
2 3
|
mpan2 |
⊢ ( 𝐴 ≺ ℕ → 𝐴 ≺ ω ) |
5 |
|
isfinite |
⊢ ( 𝐴 ∈ Fin ↔ 𝐴 ≺ ω ) |
6 |
|
finiunmbl |
⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) |
7 |
6
|
ex |
⊢ ( 𝐴 ∈ Fin → ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) ) |
8 |
5 7
|
sylbir |
⊢ ( 𝐴 ≺ ω → ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) ) |
9 |
4 8
|
syl |
⊢ ( 𝐴 ≺ ℕ → ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) ) |
10 |
|
bren |
⊢ ( 𝐴 ≈ ℕ ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ ℕ ) |
11 |
|
nfv |
⊢ Ⅎ 𝑛 𝑓 : 𝐴 –1-1-onto→ ℕ |
12 |
|
nfcv |
⊢ Ⅎ 𝑛 ℕ |
13 |
|
nfcsb1v |
⊢ Ⅎ 𝑛 ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 |
14 |
13
|
nfcri |
⊢ Ⅎ 𝑛 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 |
15 |
12 14
|
nfrex |
⊢ Ⅎ 𝑛 ∃ 𝑘 ∈ ℕ 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 |
16 |
|
f1of |
⊢ ( 𝑓 : 𝐴 –1-1-onto→ ℕ → 𝑓 : 𝐴 ⟶ ℕ ) |
17 |
16
|
ffvelrnda |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ 𝑛 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑛 ) ∈ ℕ ) |
18 |
17
|
3adant3 |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑓 ‘ 𝑛 ) ∈ ℕ ) |
19 |
|
simp3 |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 ) |
20 |
|
f1ocnvfv1 |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ 𝑛 ∈ 𝐴 ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑛 ) ) = 𝑛 ) |
21 |
20
|
3adant3 |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑛 ) ) = 𝑛 ) |
22 |
21
|
eqcomd |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑛 = ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑛 ) ) ) |
23 |
|
csbeq1a |
⊢ ( 𝑛 = ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑛 ) ) → 𝐵 = ⦋ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑛 ) ) / 𝑛 ⦌ 𝐵 ) |
24 |
22 23
|
syl |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝐵 = ⦋ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑛 ) ) / 𝑛 ⦌ 𝐵 ) |
25 |
19 24
|
eleqtrd |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑛 ) ) / 𝑛 ⦌ 𝐵 ) |
26 |
|
fveq2 |
⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ◡ 𝑓 ‘ 𝑘 ) = ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑛 ) ) ) |
27 |
26
|
csbeq1d |
⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 = ⦋ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑛 ) ) / 𝑛 ⦌ 𝐵 ) |
28 |
27
|
eleq2d |
⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ↔ 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑛 ) ) / 𝑛 ⦌ 𝐵 ) ) |
29 |
28
|
rspcev |
⊢ ( ( ( 𝑓 ‘ 𝑛 ) ∈ ℕ ∧ 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑛 ) ) / 𝑛 ⦌ 𝐵 ) → ∃ 𝑘 ∈ ℕ 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) |
30 |
18 25 29
|
syl2anc |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ 𝑛 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑘 ∈ ℕ 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) |
31 |
30
|
3exp |
⊢ ( 𝑓 : 𝐴 –1-1-onto→ ℕ → ( 𝑛 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 → ∃ 𝑘 ∈ ℕ 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) ) |
32 |
11 15 31
|
rexlimd |
⊢ ( 𝑓 : 𝐴 –1-1-onto→ ℕ → ( ∃ 𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃ 𝑘 ∈ ℕ 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) |
33 |
|
f1ocnvdm |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ 𝑘 ∈ ℕ ) → ( ◡ 𝑓 ‘ 𝑘 ) ∈ 𝐴 ) |
34 |
|
csbeq1a |
⊢ ( 𝑛 = ( ◡ 𝑓 ‘ 𝑘 ) → 𝐵 = ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) |
35 |
34
|
eleq2d |
⊢ ( 𝑛 = ( ◡ 𝑓 ‘ 𝑘 ) → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) |
36 |
14 35
|
rspce |
⊢ ( ( ( ◡ 𝑓 ‘ 𝑘 ) ∈ 𝐴 ∧ 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) → ∃ 𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 ) |
37 |
36
|
ex |
⊢ ( ( ◡ 𝑓 ‘ 𝑘 ) ∈ 𝐴 → ( 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 → ∃ 𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 ) ) |
38 |
33 37
|
syl |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 → ∃ 𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 ) ) |
39 |
38
|
rexlimdva |
⊢ ( 𝑓 : 𝐴 –1-1-onto→ ℕ → ( ∃ 𝑘 ∈ ℕ 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 → ∃ 𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 ) ) |
40 |
32 39
|
impbid |
⊢ ( 𝑓 : 𝐴 –1-1-onto→ ℕ → ( ∃ 𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∃ 𝑘 ∈ ℕ 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) |
41 |
|
eliun |
⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝐴 𝐵 ↔ ∃ 𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 ) |
42 |
|
eliun |
⊢ ( 𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ↔ ∃ 𝑘 ∈ ℕ 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) |
43 |
40 41 42
|
3bitr4g |
⊢ ( 𝑓 : 𝐴 –1-1-onto→ ℕ → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝐴 𝐵 ↔ 𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) ) |
44 |
43
|
eqrdv |
⊢ ( 𝑓 : 𝐴 –1-1-onto→ ℕ → ∪ 𝑛 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ ℕ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) |
45 |
44
|
adantr |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) → ∪ 𝑛 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ ℕ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ) |
46 |
|
rspcsbela |
⊢ ( ( ( ◡ 𝑓 ‘ 𝑘 ) ∈ 𝐴 ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) → ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ∈ dom vol ) |
47 |
33 46
|
sylan |
⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ 𝑘 ∈ ℕ ) ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) → ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ∈ dom vol ) |
48 |
47
|
an32s |
⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) ∧ 𝑘 ∈ ℕ ) → ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ∈ dom vol ) |
49 |
48
|
ralrimiva |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) → ∀ 𝑘 ∈ ℕ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ∈ dom vol ) |
50 |
|
iunmbl |
⊢ ( ∀ 𝑘 ∈ ℕ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ∈ dom vol → ∪ 𝑘 ∈ ℕ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ∈ dom vol ) |
51 |
49 50
|
syl |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) → ∪ 𝑘 ∈ ℕ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵 ∈ dom vol ) |
52 |
45 51
|
eqeltrd |
⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ℕ ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) |
53 |
52
|
ex |
⊢ ( 𝑓 : 𝐴 –1-1-onto→ ℕ → ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) ) |
54 |
53
|
exlimiv |
⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ ℕ → ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) ) |
55 |
10 54
|
sylbi |
⊢ ( 𝐴 ≈ ℕ → ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) ) |
56 |
9 55
|
jaoi |
⊢ ( ( 𝐴 ≺ ℕ ∨ 𝐴 ≈ ℕ ) → ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) ) |
57 |
1 56
|
sylbi |
⊢ ( 𝐴 ≼ ℕ → ( ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) ) |
58 |
57
|
imp |
⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ) |