Step | Hyp | Ref
| Expression |
1 | | fvssunirn 6803 |
. . . . 5
⊢ (𝐹‘𝑧) ⊆ ∪ ran
𝐹 |
2 | | simplrr 775 |
. . . . 5
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (𝐹‘𝑦) = ∪ ran 𝐹) |
3 | 1, 2 | sseqtrrid 3974 |
. . . 4
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (𝐹‘𝑧) ⊆ (𝐹‘𝑦)) |
4 | | simpll3 1213 |
. . . . 5
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) |
5 | | simplrl 774 |
. . . . 5
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → 𝑦 ∈ ℕ0) |
6 | | simpr 485 |
. . . . 5
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → 𝑧 ∈ (ℤ≥‘𝑦)) |
7 | | incssnn0 40533 |
. . . . 5
⊢
((∀𝑥 ∈
ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝑦 ∈ ℕ0 ∧ 𝑧 ∈
(ℤ≥‘𝑦)) → (𝐹‘𝑦) ⊆ (𝐹‘𝑧)) |
8 | 4, 5, 6, 7 | syl3anc 1370 |
. . . 4
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (𝐹‘𝑦) ⊆ (𝐹‘𝑧)) |
9 | 3, 8 | eqssd 3938 |
. . 3
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (𝐹‘𝑧) = (𝐹‘𝑦)) |
10 | 9 | ralrimiva 3103 |
. 2
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) → ∀𝑧 ∈
(ℤ≥‘𝑦)(𝐹‘𝑧) = (𝐹‘𝑦)) |
11 | | frn 6607 |
. . . . . . . 8
⊢ (𝐹:ℕ0⟶𝐶 → ran 𝐹 ⊆ 𝐶) |
12 | 11 | 3ad2ant2 1133 |
. . . . . . 7
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ran 𝐹 ⊆ 𝐶) |
13 | | elpw2g 5268 |
. . . . . . . 8
⊢ (𝐶 ∈ (NoeACS‘𝑋) → (ran 𝐹 ∈ 𝒫 𝐶 ↔ ran 𝐹 ⊆ 𝐶)) |
14 | 13 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → (ran 𝐹 ∈ 𝒫 𝐶 ↔ ran 𝐹 ⊆ 𝐶)) |
15 | 12, 14 | mpbird 256 |
. . . . . 6
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ran 𝐹 ∈ 𝒫 𝐶) |
16 | | elex 3450 |
. . . . . 6
⊢ (ran
𝐹 ∈ 𝒫 𝐶 → ran 𝐹 ∈ V) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ran 𝐹 ∈ V) |
18 | | ffn 6600 |
. . . . . . . 8
⊢ (𝐹:ℕ0⟶𝐶 → 𝐹 Fn ℕ0) |
19 | 18 | 3ad2ant2 1133 |
. . . . . . 7
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → 𝐹 Fn ℕ0) |
20 | | 0nn0 12248 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
21 | | fnfvelrn 6958 |
. . . . . . 7
⊢ ((𝐹 Fn ℕ0 ∧ 0
∈ ℕ0) → (𝐹‘0) ∈ ran 𝐹) |
22 | 19, 20, 21 | sylancl 586 |
. . . . . 6
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → (𝐹‘0) ∈ ran 𝐹) |
23 | 22 | ne0d 4269 |
. . . . 5
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ran 𝐹 ≠ ∅) |
24 | | nn0re 12242 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
ℝ) |
25 | 24 | ad2antrl 725 |
. . . . . . . 8
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 𝑎 ∈
ℝ) |
26 | | nn0re 12242 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℝ) |
27 | 26 | ad2antll 726 |
. . . . . . . 8
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 𝑏 ∈
ℝ) |
28 | | simplrr 775 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → 𝑏 ∈ ℕ0) |
29 | | simpll3 1213 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) |
30 | | simplrl 774 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → 𝑎 ∈ ℕ0) |
31 | | nn0z 12343 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
ℤ) |
32 | | nn0z 12343 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℤ) |
33 | | eluz 12596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑏 ∈
(ℤ≥‘𝑎) ↔ 𝑎 ≤ 𝑏)) |
34 | 31, 32, 33 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) → (𝑏 ∈ (ℤ≥‘𝑎) ↔ 𝑎 ≤ 𝑏)) |
35 | 34 | biimpar 478 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ 𝑎 ≤ 𝑏) → 𝑏 ∈ (ℤ≥‘𝑎)) |
36 | 35 | adantll 711 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → 𝑏 ∈ (ℤ≥‘𝑎)) |
37 | | incssnn0 40533 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈
(ℤ≥‘𝑎)) → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) |
38 | 29, 30, 36, 37 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) |
39 | | ssequn1 4114 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑎) ⊆ (𝐹‘𝑏) ↔ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = (𝐹‘𝑏)) |
40 | 38, 39 | sylib 217 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = (𝐹‘𝑏)) |
41 | | eqimss 3977 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = (𝐹‘𝑏) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑏)) |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑏)) |
43 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑏 → (𝐹‘𝑐) = (𝐹‘𝑏)) |
44 | 43 | sseq2d 3953 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑏 → (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐) ↔ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑏))) |
45 | 44 | rspcev 3561 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑏)) → ∃𝑐 ∈ ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐)) |
46 | 28, 42, 45 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → ∃𝑐 ∈ ℕ0
((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐)) |
47 | | simplrl 774 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → 𝑎 ∈ ℕ0) |
48 | | simpll3 1213 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) |
49 | | simplrr 775 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → 𝑏 ∈ ℕ0) |
50 | | eluz 12596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → (𝑎 ∈
(ℤ≥‘𝑏) ↔ 𝑏 ≤ 𝑎)) |
51 | 32, 31, 50 | syl2anr 597 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) → (𝑎 ∈ (ℤ≥‘𝑏) ↔ 𝑏 ≤ 𝑎)) |
52 | 51 | biimpar 478 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ 𝑏 ≤ 𝑎) → 𝑎 ∈ (ℤ≥‘𝑏)) |
53 | 52 | adantll 711 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → 𝑎 ∈ (ℤ≥‘𝑏)) |
54 | | incssnn0 40533 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝑏 ∈ ℕ0 ∧ 𝑎 ∈
(ℤ≥‘𝑏)) → (𝐹‘𝑏) ⊆ (𝐹‘𝑎)) |
55 | 48, 49, 53, 54 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → (𝐹‘𝑏) ⊆ (𝐹‘𝑎)) |
56 | | ssequn2 4117 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑏) ⊆ (𝐹‘𝑎) ↔ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = (𝐹‘𝑎)) |
57 | 55, 56 | sylib 217 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = (𝐹‘𝑎)) |
58 | | eqimss 3977 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = (𝐹‘𝑎) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑎)) |
59 | 57, 58 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑎)) |
60 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑎 → (𝐹‘𝑐) = (𝐹‘𝑎)) |
61 | 60 | sseq2d 3953 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑎 → (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐) ↔ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑎))) |
62 | 61 | rspcev 3561 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℕ0
∧ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑎)) → ∃𝑐 ∈ ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐)) |
63 | 47, 59, 62 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → ∃𝑐 ∈ ℕ0
((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐)) |
64 | 25, 27, 46, 63 | lecasei 11081 |
. . . . . . 7
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ ∃𝑐 ∈
ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐)) |
65 | 64 | ralrimivva 3123 |
. . . . . 6
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∀𝑎 ∈ ℕ0 ∀𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐)) |
66 | | uneq1 4090 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐹‘𝑎) → (𝑦 ∪ 𝑧) = ((𝐹‘𝑎) ∪ 𝑧)) |
67 | 66 | sseq1d 3952 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑎) → ((𝑦 ∪ 𝑧) ⊆ 𝑤 ↔ ((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤)) |
68 | 67 | rexbidv 3226 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑎) → (∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤 ↔ ∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤)) |
69 | 68 | ralbidv 3112 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑎) → (∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤)) |
70 | 69 | ralrn 6964 |
. . . . . . . 8
⊢ (𝐹 Fn ℕ0 →
(∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑎 ∈ ℕ0 ∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤)) |
71 | | uneq2 4091 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐹‘𝑏) → ((𝐹‘𝑎) ∪ 𝑧) = ((𝐹‘𝑎) ∪ (𝐹‘𝑏))) |
72 | 71 | sseq1d 3952 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝐹‘𝑏) → (((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤 ↔ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ 𝑤)) |
73 | 72 | rexbidv 3226 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹‘𝑏) → (∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤 ↔ ∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ 𝑤)) |
74 | 73 | ralrn 6964 |
. . . . . . . . . 10
⊢ (𝐹 Fn ℕ0 →
(∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑏 ∈ ℕ0 ∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ 𝑤)) |
75 | | sseq2 3947 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝐹‘𝑐) → (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ 𝑤 ↔ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
76 | 75 | rexrn 6963 |
. . . . . . . . . . 11
⊢ (𝐹 Fn ℕ0 →
(∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ 𝑤 ↔ ∃𝑐 ∈ ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
77 | 76 | ralbidv 3112 |
. . . . . . . . . 10
⊢ (𝐹 Fn ℕ0 →
(∀𝑏 ∈
ℕ0 ∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ 𝑤 ↔ ∀𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0
((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
78 | 74, 77 | bitrd 278 |
. . . . . . . . 9
⊢ (𝐹 Fn ℕ0 →
(∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0
((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
79 | 78 | ralbidv 3112 |
. . . . . . . 8
⊢ (𝐹 Fn ℕ0 →
(∀𝑎 ∈
ℕ0 ∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑎 ∈ ℕ0 ∀𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
80 | 70, 79 | bitrd 278 |
. . . . . . 7
⊢ (𝐹 Fn ℕ0 →
(∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑎 ∈ ℕ0 ∀𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
81 | 19, 80 | syl 17 |
. . . . . 6
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑎 ∈ ℕ0 ∀𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
82 | 65, 81 | mpbird 256 |
. . . . 5
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤) |
83 | | isipodrs 18255 |
. . . . 5
⊢
((toInc‘ran 𝐹)
∈ Dirset ↔ (ran 𝐹
∈ V ∧ ran 𝐹 ≠
∅ ∧ ∀𝑦
∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤)) |
84 | 17, 23, 82, 83 | syl3anbrc 1342 |
. . . 4
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → (toInc‘ran 𝐹) ∈
Dirset) |
85 | | isnacs3 40532 |
. . . . . . 7
⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑦 ∈ 𝒫 𝐶((toInc‘𝑦) ∈ Dirset → ∪ 𝑦
∈ 𝑦))) |
86 | 85 | simprbi 497 |
. . . . . 6
⊢ (𝐶 ∈ (NoeACS‘𝑋) → ∀𝑦 ∈ 𝒫 𝐶((toInc‘𝑦) ∈ Dirset → ∪ 𝑦
∈ 𝑦)) |
87 | 86 | 3ad2ant1 1132 |
. . . . 5
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∀𝑦 ∈ 𝒫 𝐶((toInc‘𝑦) ∈ Dirset → ∪ 𝑦
∈ 𝑦)) |
88 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑦 = ran 𝐹 → (toInc‘𝑦) = (toInc‘ran 𝐹)) |
89 | 88 | eleq1d 2823 |
. . . . . . 7
⊢ (𝑦 = ran 𝐹 → ((toInc‘𝑦) ∈ Dirset ↔ (toInc‘ran 𝐹) ∈
Dirset)) |
90 | | unieq 4850 |
. . . . . . . 8
⊢ (𝑦 = ran 𝐹 → ∪ 𝑦 = ∪
ran 𝐹) |
91 | | id 22 |
. . . . . . . 8
⊢ (𝑦 = ran 𝐹 → 𝑦 = ran 𝐹) |
92 | 90, 91 | eleq12d 2833 |
. . . . . . 7
⊢ (𝑦 = ran 𝐹 → (∪ 𝑦 ∈ 𝑦 ↔ ∪ ran
𝐹 ∈ ran 𝐹)) |
93 | 89, 92 | imbi12d 345 |
. . . . . 6
⊢ (𝑦 = ran 𝐹 → (((toInc‘𝑦) ∈ Dirset → ∪ 𝑦
∈ 𝑦) ↔
((toInc‘ran 𝐹) ∈
Dirset → ∪ ran 𝐹 ∈ ran 𝐹))) |
94 | 93 | rspcva 3559 |
. . . . 5
⊢ ((ran
𝐹 ∈ 𝒫 𝐶 ∧ ∀𝑦 ∈ 𝒫 𝐶((toInc‘𝑦) ∈ Dirset → ∪ 𝑦
∈ 𝑦)) →
((toInc‘ran 𝐹) ∈
Dirset → ∪ ran 𝐹 ∈ ran 𝐹)) |
95 | 15, 87, 94 | syl2anc 584 |
. . . 4
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ((toInc‘ran 𝐹) ∈ Dirset → ∪ ran 𝐹 ∈ ran 𝐹)) |
96 | 84, 95 | mpd 15 |
. . 3
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∪
ran 𝐹 ∈ ran 𝐹) |
97 | | fvelrnb 6830 |
. . . 4
⊢ (𝐹 Fn ℕ0 →
(∪ ran 𝐹 ∈ ran 𝐹 ↔ ∃𝑦 ∈ ℕ0 (𝐹‘𝑦) = ∪ ran 𝐹)) |
98 | 19, 97 | syl 17 |
. . 3
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → (∪
ran 𝐹 ∈ ran 𝐹 ↔ ∃𝑦 ∈ ℕ0
(𝐹‘𝑦) = ∪ ran 𝐹)) |
99 | 96, 98 | mpbid 231 |
. 2
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∃𝑦 ∈ ℕ0 (𝐹‘𝑦) = ∪ ran 𝐹) |
100 | 10, 99 | reximddv 3204 |
1
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∃𝑦 ∈ ℕ0 ∀𝑧 ∈
(ℤ≥‘𝑦)(𝐹‘𝑧) = (𝐹‘𝑦)) |