Step | Hyp | Ref
| Expression |
1 | | elmapi 8551 |
. . . 4
⊢ (𝑓 ∈ (𝒫 𝐴 ↑m ω)
→ 𝑓:ω⟶𝒫 𝐴) |
2 | | simpl 486 |
. . . . . 6
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → 𝐴 ∈ FinII) |
3 | | frn 6571 |
. . . . . . 7
⊢ (𝑓:ω⟶𝒫 𝐴 → ran 𝑓 ⊆ 𝒫 𝐴) |
4 | 3 | ad2antrl 728 |
. . . . . 6
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → ran 𝑓 ⊆ 𝒫 𝐴) |
5 | | fdm 6573 |
. . . . . . . . 9
⊢ (𝑓:ω⟶𝒫 𝐴 → dom 𝑓 = ω) |
6 | | peano1 7686 |
. . . . . . . . . 10
⊢ ∅
∈ ω |
7 | | ne0i 4264 |
. . . . . . . . . 10
⊢ (∅
∈ ω → ω ≠ ∅) |
8 | 6, 7 | mp1i 13 |
. . . . . . . . 9
⊢ (𝑓:ω⟶𝒫 𝐴 → ω ≠
∅) |
9 | 5, 8 | eqnetrd 3009 |
. . . . . . . 8
⊢ (𝑓:ω⟶𝒫 𝐴 → dom 𝑓 ≠ ∅) |
10 | | dm0rn0 5809 |
. . . . . . . . 9
⊢ (dom
𝑓 = ∅ ↔ ran
𝑓 =
∅) |
11 | 10 | necon3bii 2994 |
. . . . . . . 8
⊢ (dom
𝑓 ≠ ∅ ↔ ran
𝑓 ≠
∅) |
12 | 9, 11 | sylib 221 |
. . . . . . 7
⊢ (𝑓:ω⟶𝒫 𝐴 → ran 𝑓 ≠ ∅) |
13 | 12 | ad2antrl 728 |
. . . . . 6
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → ran 𝑓 ≠ ∅) |
14 | | ffn 6564 |
. . . . . . . . 9
⊢ (𝑓:ω⟶𝒫 𝐴 → 𝑓 Fn ω) |
15 | 14 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → 𝑓 Fn ω) |
16 | | sspss 4029 |
. . . . . . . . . . 11
⊢ ((𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏) ↔ ((𝑓‘suc 𝑏) ⊊ (𝑓‘𝑏) ∨ (𝑓‘suc 𝑏) = (𝑓‘𝑏))) |
17 | | fvex 6749 |
. . . . . . . . . . . . . 14
⊢ (𝑓‘𝑏) ∈ V |
18 | | fvex 6749 |
. . . . . . . . . . . . . 14
⊢ (𝑓‘suc 𝑏) ∈ V |
19 | 17, 18 | brcnv 5766 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ↔ (𝑓‘suc 𝑏) [⊊] (𝑓‘𝑏)) |
20 | 17 | brrpss 7533 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘suc 𝑏) [⊊] (𝑓‘𝑏) ↔ (𝑓‘suc 𝑏) ⊊ (𝑓‘𝑏)) |
21 | 19, 20 | bitri 278 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ↔ (𝑓‘suc 𝑏) ⊊ (𝑓‘𝑏)) |
22 | | eqcom 2745 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑏) = (𝑓‘suc 𝑏) ↔ (𝑓‘suc 𝑏) = (𝑓‘𝑏)) |
23 | 21, 22 | orbi12i 915 |
. . . . . . . . . . 11
⊢ (((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ∨ (𝑓‘𝑏) = (𝑓‘suc 𝑏)) ↔ ((𝑓‘suc 𝑏) ⊊ (𝑓‘𝑏) ∨ (𝑓‘suc 𝑏) = (𝑓‘𝑏))) |
24 | 16, 23 | sylbb2 241 |
. . . . . . . . . 10
⊢ ((𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏) → ((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ∨ (𝑓‘𝑏) = (𝑓‘suc 𝑏))) |
25 | 24 | ralimi 3085 |
. . . . . . . . 9
⊢
(∀𝑏 ∈
ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏) → ∀𝑏 ∈ ω ((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ∨ (𝑓‘𝑏) = (𝑓‘suc 𝑏))) |
26 | 25 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → ∀𝑏 ∈ ω ((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ∨ (𝑓‘𝑏) = (𝑓‘suc 𝑏))) |
27 | | porpss 7534 |
. . . . . . . . . 10
⊢
[⊊] Po ran 𝑓 |
28 | | cnvpo 6165 |
. . . . . . . . . 10
⊢ (
[⊊] Po ran 𝑓
↔ ◡ [⊊] Po ran 𝑓) |
29 | 27, 28 | mpbi 233 |
. . . . . . . . 9
⊢ ◡ [⊊] Po ran 𝑓 |
30 | 29 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → ◡ [⊊] Po ran 𝑓) |
31 | | sornom 9916 |
. . . . . . . 8
⊢ ((𝑓 Fn ω ∧ ∀𝑏 ∈ ω ((𝑓‘𝑏)◡
[⊊] (𝑓‘suc 𝑏) ∨ (𝑓‘𝑏) = (𝑓‘suc 𝑏)) ∧ ◡ [⊊] Po ran 𝑓) → ◡ [⊊] Or ran 𝑓) |
32 | 15, 26, 30, 31 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → ◡ [⊊] Or ran 𝑓) |
33 | | cnvso 6166 |
. . . . . . 7
⊢ (
[⊊] Or ran 𝑓
↔ ◡ [⊊] Or ran 𝑓) |
34 | 32, 33 | sylibr 237 |
. . . . . 6
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → [⊊] Or ran 𝑓) |
35 | | fin2i2 9957 |
. . . . . 6
⊢ (((𝐴 ∈ FinII ∧
ran 𝑓 ⊆ 𝒫
𝐴) ∧ (ran 𝑓 ≠ ∅ ∧
[⊊] Or ran 𝑓)) → ∩ ran
𝑓 ∈ ran 𝑓) |
36 | 2, 4, 13, 34, 35 | syl22anc 839 |
. . . . 5
⊢ ((𝐴 ∈ FinII ∧
(𝑓:ω⟶𝒫
𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏))) → ∩ ran
𝑓 ∈ ran 𝑓) |
37 | 36 | expr 460 |
. . . 4
⊢ ((𝐴 ∈ FinII ∧
𝑓:ω⟶𝒫
𝐴) → (∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏) → ∩ ran
𝑓 ∈ ran 𝑓)) |
38 | 1, 37 | sylan2 596 |
. . 3
⊢ ((𝐴 ∈ FinII ∧
𝑓 ∈ (𝒫 𝐴 ↑m ω))
→ (∀𝑏 ∈
ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏) → ∩ ran
𝑓 ∈ ran 𝑓)) |
39 | 38 | ralrimiva 3106 |
. 2
⊢ (𝐴 ∈ FinII →
∀𝑓 ∈ (𝒫
𝐴 ↑m
ω)(∀𝑏 ∈
ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏) → ∩ ran
𝑓 ∈ ran 𝑓)) |
40 | | fin23lem40.f |
. . 3
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran
𝑎 ∈ ran 𝑎)} |
41 | 40 | isfin3ds 9968 |
. 2
⊢ (𝐴 ∈ FinII →
(𝐴 ∈ 𝐹 ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑m ω)(∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓‘𝑏) → ∩ ran
𝑓 ∈ ran 𝑓))) |
42 | 39, 41 | mpbird 260 |
1
⊢ (𝐴 ∈ FinII →
𝐴 ∈ 𝐹) |