Step | Hyp | Ref
| Expression |
1 | | elmapi 8144 |
. . . 4
⊢ (𝑓 ∈ (𝒫 𝐴 ↑𝑚
ω) → 𝑓:ω⟶𝒫 𝐴) |
2 | | simpl 476 |
. . . . . 6
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → 𝐴 ∈ FinII) |
3 | | frn 6284 |
. . . . . . 7
⊢ (𝑓:ω⟶𝒫 𝐴 → ran 𝑓 ⊆ 𝒫 𝐴) |
4 | 3 | ad2antrl 719 |
. . . . . 6
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → ran 𝑓 ⊆ 𝒫 𝐴) |
5 | | fdm 6286 |
. . . . . . . . 9
⊢ (𝑓:ω⟶𝒫 𝐴 → dom 𝑓 = ω) |
6 | | peano1 7346 |
. . . . . . . . . 10
⊢ ∅
∈ ω |
7 | | ne0i 4150 |
. . . . . . . . . 10
⊢ (∅
∈ ω → ω ≠ ∅) |
8 | 6, 7 | mp1i 13 |
. . . . . . . . 9
⊢ (𝑓:ω⟶𝒫 𝐴 → ω ≠
∅) |
9 | 5, 8 | eqnetrd 3066 |
. . . . . . . 8
⊢ (𝑓:ω⟶𝒫 𝐴 → dom 𝑓 ≠ ∅) |
10 | | dm0rn0 5574 |
. . . . . . . . 9
⊢ (dom
𝑓 = ∅ ↔ ran
𝑓 =
∅) |
11 | 10 | necon3bii 3051 |
. . . . . . . 8
⊢ (dom
𝑓 ≠ ∅ ↔ ran
𝑓 ≠
∅) |
12 | 9, 11 | sylib 210 |
. . . . . . 7
⊢ (𝑓:ω⟶𝒫 𝐴 → ran 𝑓 ≠ ∅) |
13 | 12 | ad2antrl 719 |
. . . . . 6
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → ran 𝑓 ≠ ∅) |
14 | | ffn 6278 |
. . . . . . . . 9
⊢ (𝑓:ω⟶𝒫 𝐴 → 𝑓 Fn ω) |
15 | 14 | ad2antrl 719 |
. . . . . . . 8
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → 𝑓 Fn ω) |
16 | | sspss 3932 |
. . . . . . . . . . 11
⊢ ((𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏) ↔ ((𝑓‘suc 𝑏) ⊊ (𝑓‘𝑏) ∨ (𝑓‘suc 𝑏) = (𝑓‘𝑏))) |
17 | | fvex 6446 |
. . . . . . . . . . . . . 14
⊢ (𝑓‘𝑏) ∈ V |
18 | | fvex 6446 |
. . . . . . . . . . . . . 14
⊢ (𝑓‘suc 𝑏) ∈ V |
19 | 17, 18 | brcnv 5537 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ↔ (𝑓‘suc 𝑏) [⊊] (𝑓‘𝑏)) |
20 | 17 | brrpss 7200 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘suc 𝑏) [⊊] (𝑓‘𝑏) ↔ (𝑓‘suc 𝑏) ⊊ (𝑓‘𝑏)) |
21 | 19, 20 | bitri 267 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ↔ (𝑓‘suc 𝑏) ⊊ (𝑓‘𝑏)) |
22 | | eqcom 2832 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑏) = (𝑓‘suc 𝑏) ↔ (𝑓‘suc 𝑏) = (𝑓‘𝑏)) |
23 | 21, 22 | orbi12i 943 |
. . . . . . . . . . 11
⊢ (((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ∨ (𝑓‘𝑏) = (𝑓‘suc 𝑏)) ↔ ((𝑓‘suc 𝑏) ⊊ (𝑓‘𝑏) ∨ (𝑓‘suc 𝑏) = (𝑓‘𝑏))) |
24 | 16, 23 | sylbb2 230 |
. . . . . . . . . 10
⊢ ((𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏) → ((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ∨ (𝑓‘𝑏) = (𝑓‘suc 𝑏))) |
25 | 24 | ralimi 3161 |
. . . . . . . . 9
⊢
(∀𝑏 ∈
ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏) → ∀𝑏 ∈ ω ((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ∨ (𝑓‘𝑏) = (𝑓‘suc 𝑏))) |
26 | 25 | ad2antll 720 |
. . . . . . . 8
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → ∀𝑏 ∈ ω ((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ∨ (𝑓‘𝑏) = (𝑓‘suc 𝑏))) |
27 | | porpss 7201 |
. . . . . . . . . 10
⊢
[⊊] Po ran 𝑓 |
28 | | cnvpo 5914 |
. . . . . . . . . 10
⊢ (
[⊊] Po ran 𝑓
↔ ◡ [⊊] Po ran 𝑓) |
29 | 27, 28 | mpbi 222 |
. . . . . . . . 9
⊢ ◡ [⊊] Po ran 𝑓 |
30 | 29 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → ◡ [⊊] Po ran 𝑓) |
31 | | sornom 9414 |
. . . . . . . 8
⊢ ((𝑓 Fn ω ∧ ∀𝑏 ∈ ω ((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ∨ (𝑓‘𝑏) = (𝑓‘suc 𝑏)) ∧ ◡ [⊊] Po ran 𝑓) → ◡ [⊊] Or ran 𝑓) |
32 | 15, 26, 30, 31 | syl3anc 1494 |
. . . . . . 7
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → ◡ [⊊] Or ran 𝑓) |
33 | | cnvso 5915 |
. . . . . . 7
⊢ (
[⊊] Or ran 𝑓
↔ ◡ [⊊] Or ran 𝑓) |
34 | 32, 33 | sylibr 226 |
. . . . . 6
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → [⊊] Or ran 𝑓) |
35 | | fin2i2 9455 |
. . . . . 6
⊢ (((𝐴 ∈ FinII ∧
ran 𝑓 ⊆ 𝒫
𝐴) ∧ (ran 𝑓 ≠ ∅ ∧
[⊊] Or ran 𝑓)) → ∩ ran
𝑓 ∈ ran 𝑓) |
36 | 2, 4, 13, 34, 35 | syl22anc 872 |
. . . . 5
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → ∩ ran
𝑓 ∈ ran 𝑓) |
37 | 36 | expr 450 |
. . . 4
⊢ ((𝐴 ∈ FinII ∧
𝑓:ω⟶𝒫
𝐴) → (∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏) → ∩ ran
𝑓 ∈ ran 𝑓)) |
38 | 1, 37 | sylan2 586 |
. . 3
⊢ ((𝐴 ∈ FinII ∧
𝑓 ∈ (𝒫 𝐴 ↑𝑚
ω)) → (∀𝑏
∈ ω (𝑓‘suc
𝑏) ⊆ (𝑓‘𝑏) → ∩ ran
𝑓 ∈ ran 𝑓)) |
39 | 38 | ralrimiva 3175 |
. 2
⊢ (𝐴 ∈ FinII →
∀𝑓 ∈ (𝒫
𝐴
↑𝑚 ω)(∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏) → ∩ ran
𝑓 ∈ ran 𝑓)) |
40 | | fin23lem40.f |
. . 3
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚
ω)(∀𝑥 ∈
ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran
𝑎 ∈ ran 𝑎)} |
41 | 40 | isfin3ds 9466 |
. 2
⊢ (𝐴 ∈ FinII →
(𝐴 ∈ 𝐹 ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑𝑚
ω)(∀𝑏 ∈
ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏) → ∩ ran
𝑓 ∈ ran 𝑓))) |
42 | 39, 41 | mpbird 249 |
1
⊢ (𝐴 ∈ FinII →
𝐴 ∈ 𝐹) |