Step | Hyp | Ref
| Expression |
1 | | fvssunirn 6217 |
. . . . 5
⊢ (𝐹‘𝑧) ⊆ ∪ ran
𝐹 |
2 | | simplrr 801 |
. . . . 5
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (𝐹‘𝑦) = ∪ ran 𝐹) |
3 | 1, 2 | syl5sseqr 3654 |
. . . 4
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (𝐹‘𝑧) ⊆ (𝐹‘𝑦)) |
4 | | simpll3 1102 |
. . . . 5
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) |
5 | | simplrl 800 |
. . . . 5
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → 𝑦 ∈ ℕ0) |
6 | | simpr 477 |
. . . . 5
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → 𝑧 ∈ (ℤ≥‘𝑦)) |
7 | | incssnn0 37274 |
. . . . 5
⊢
((∀𝑥 ∈
ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝑦 ∈ ℕ0 ∧ 𝑧 ∈
(ℤ≥‘𝑦)) → (𝐹‘𝑦) ⊆ (𝐹‘𝑧)) |
8 | 4, 5, 6, 7 | syl3anc 1326 |
. . . 4
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (𝐹‘𝑦) ⊆ (𝐹‘𝑧)) |
9 | 3, 8 | eqssd 3620 |
. . 3
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (𝐹‘𝑧) = (𝐹‘𝑦)) |
10 | 9 | ralrimiva 2966 |
. 2
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑦 ∈ ℕ0 ∧ (𝐹‘𝑦) = ∪ ran 𝐹)) → ∀𝑧 ∈
(ℤ≥‘𝑦)(𝐹‘𝑧) = (𝐹‘𝑦)) |
11 | | frn 6053 |
. . . . . . . 8
⊢ (𝐹:ℕ0⟶𝐶 → ran 𝐹 ⊆ 𝐶) |
12 | 11 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ran 𝐹 ⊆ 𝐶) |
13 | | elpw2g 4827 |
. . . . . . . 8
⊢ (𝐶 ∈ (NoeACS‘𝑋) → (ran 𝐹 ∈ 𝒫 𝐶 ↔ ran 𝐹 ⊆ 𝐶)) |
14 | 13 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → (ran 𝐹 ∈ 𝒫 𝐶 ↔ ran 𝐹 ⊆ 𝐶)) |
15 | 12, 14 | mpbird 247 |
. . . . . 6
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ran 𝐹 ∈ 𝒫 𝐶) |
16 | | elex 3212 |
. . . . . 6
⊢ (ran
𝐹 ∈ 𝒫 𝐶 → ran 𝐹 ∈ V) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ran 𝐹 ∈ V) |
18 | | ffn 6045 |
. . . . . . . 8
⊢ (𝐹:ℕ0⟶𝐶 → 𝐹 Fn ℕ0) |
19 | 18 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → 𝐹 Fn ℕ0) |
20 | | 0nn0 11307 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
21 | | fnfvelrn 6356 |
. . . . . . 7
⊢ ((𝐹 Fn ℕ0 ∧ 0
∈ ℕ0) → (𝐹‘0) ∈ ran 𝐹) |
22 | 19, 20, 21 | sylancl 694 |
. . . . . 6
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → (𝐹‘0) ∈ ran 𝐹) |
23 | | ne0i 3921 |
. . . . . 6
⊢ ((𝐹‘0) ∈ ran 𝐹 → ran 𝐹 ≠ ∅) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ran 𝐹 ≠ ∅) |
25 | | nn0re 11301 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
ℝ) |
26 | 25 | ad2antrl 764 |
. . . . . . . 8
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 𝑎 ∈
ℝ) |
27 | | nn0re 11301 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℝ) |
28 | 27 | ad2antll 765 |
. . . . . . . 8
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 𝑏 ∈
ℝ) |
29 | | simplrr 801 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → 𝑏 ∈ ℕ0) |
30 | | simpll3 1102 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) |
31 | | simplrl 800 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → 𝑎 ∈ ℕ0) |
32 | | nn0z 11400 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
ℤ) |
33 | | nn0z 11400 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℤ) |
34 | | eluz 11701 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑏 ∈
(ℤ≥‘𝑎) ↔ 𝑎 ≤ 𝑏)) |
35 | 32, 33, 34 | syl2an 494 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) → (𝑏 ∈ (ℤ≥‘𝑎) ↔ 𝑎 ≤ 𝑏)) |
36 | 35 | biimpar 502 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ 𝑎 ≤ 𝑏) → 𝑏 ∈ (ℤ≥‘𝑎)) |
37 | 36 | adantll 750 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → 𝑏 ∈ (ℤ≥‘𝑎)) |
38 | | incssnn0 37274 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈
(ℤ≥‘𝑎)) → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) |
39 | 30, 31, 37, 38 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) |
40 | | ssequn1 3783 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑎) ⊆ (𝐹‘𝑏) ↔ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = (𝐹‘𝑏)) |
41 | 39, 40 | sylib 208 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = (𝐹‘𝑏)) |
42 | | eqimss 3657 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = (𝐹‘𝑏) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑏)) |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑏)) |
44 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑏 → (𝐹‘𝑐) = (𝐹‘𝑏)) |
45 | 44 | sseq2d 3633 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑏 → (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐) ↔ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑏))) |
46 | 45 | rspcev 3309 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑏)) → ∃𝑐 ∈ ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐)) |
47 | 29, 43, 46 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑎 ≤ 𝑏) → ∃𝑐 ∈ ℕ0
((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐)) |
48 | | simplrl 800 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → 𝑎 ∈ ℕ0) |
49 | | simpll3 1102 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) |
50 | | simplrr 801 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → 𝑏 ∈ ℕ0) |
51 | | eluz 11701 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → (𝑎 ∈
(ℤ≥‘𝑏) ↔ 𝑏 ≤ 𝑎)) |
52 | 33, 32, 51 | syl2anr 495 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) → (𝑎 ∈ (ℤ≥‘𝑏) ↔ 𝑏 ≤ 𝑎)) |
53 | 52 | biimpar 502 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℕ0
∧ 𝑏 ∈
ℕ0) ∧ 𝑏 ≤ 𝑎) → 𝑎 ∈ (ℤ≥‘𝑏)) |
54 | 53 | adantll 750 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → 𝑎 ∈ (ℤ≥‘𝑏)) |
55 | | incssnn0 37274 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝑏 ∈ ℕ0 ∧ 𝑎 ∈
(ℤ≥‘𝑏)) → (𝐹‘𝑏) ⊆ (𝐹‘𝑎)) |
56 | 49, 50, 54, 55 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → (𝐹‘𝑏) ⊆ (𝐹‘𝑎)) |
57 | | ssequn2 3786 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑏) ⊆ (𝐹‘𝑎) ↔ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = (𝐹‘𝑎)) |
58 | 56, 57 | sylib 208 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = (𝐹‘𝑎)) |
59 | | eqimss 3657 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = (𝐹‘𝑎) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑎)) |
60 | 58, 59 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑎)) |
61 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑎 → (𝐹‘𝑐) = (𝐹‘𝑎)) |
62 | 61 | sseq2d 3633 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑎 → (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐) ↔ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑎))) |
63 | 62 | rspcev 3309 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℕ0
∧ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑎)) → ∃𝑐 ∈ ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐)) |
64 | 48, 60, 63 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ 𝑏 ≤ 𝑎) → ∃𝑐 ∈ ℕ0
((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐)) |
65 | 26, 28, 47, 64 | lecasei 10143 |
. . . . . . 7
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ ∃𝑐 ∈
ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐)) |
66 | 65 | ralrimivva 2971 |
. . . . . 6
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∀𝑎 ∈ ℕ0 ∀𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐)) |
67 | | uneq1 3760 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐹‘𝑎) → (𝑦 ∪ 𝑧) = ((𝐹‘𝑎) ∪ 𝑧)) |
68 | 67 | sseq1d 3632 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑎) → ((𝑦 ∪ 𝑧) ⊆ 𝑤 ↔ ((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤)) |
69 | 68 | rexbidv 3052 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑎) → (∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤 ↔ ∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤)) |
70 | 69 | ralbidv 2986 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑎) → (∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤)) |
71 | 70 | ralrn 6362 |
. . . . . . . 8
⊢ (𝐹 Fn ℕ0 →
(∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑎 ∈ ℕ0 ∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤)) |
72 | | uneq2 3761 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐹‘𝑏) → ((𝐹‘𝑎) ∪ 𝑧) = ((𝐹‘𝑎) ∪ (𝐹‘𝑏))) |
73 | 72 | sseq1d 3632 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝐹‘𝑏) → (((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤 ↔ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ 𝑤)) |
74 | 73 | rexbidv 3052 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹‘𝑏) → (∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤 ↔ ∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ 𝑤)) |
75 | 74 | ralrn 6362 |
. . . . . . . . . 10
⊢ (𝐹 Fn ℕ0 →
(∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑏 ∈ ℕ0 ∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ 𝑤)) |
76 | | sseq2 3627 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝐹‘𝑐) → (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ 𝑤 ↔ ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
77 | 76 | rexrn 6361 |
. . . . . . . . . . 11
⊢ (𝐹 Fn ℕ0 →
(∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ 𝑤 ↔ ∃𝑐 ∈ ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
78 | 77 | ralbidv 2986 |
. . . . . . . . . 10
⊢ (𝐹 Fn ℕ0 →
(∀𝑏 ∈
ℕ0 ∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ 𝑤 ↔ ∀𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0
((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
79 | 75, 78 | bitrd 268 |
. . . . . . . . 9
⊢ (𝐹 Fn ℕ0 →
(∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0
((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
80 | 79 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝐹 Fn ℕ0 →
(∀𝑎 ∈
ℕ0 ∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹((𝐹‘𝑎) ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑎 ∈ ℕ0 ∀𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
81 | 71, 80 | bitrd 268 |
. . . . . . 7
⊢ (𝐹 Fn ℕ0 →
(∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑎 ∈ ℕ0 ∀𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
82 | 19, 81 | syl 17 |
. . . . . 6
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤 ↔ ∀𝑎 ∈ ℕ0 ∀𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘𝑐))) |
83 | 66, 82 | mpbird 247 |
. . . . 5
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤) |
84 | | isipodrs 17161 |
. . . . 5
⊢
((toInc‘ran 𝐹)
∈ Dirset ↔ (ran 𝐹
∈ V ∧ ran 𝐹 ≠
∅ ∧ ∀𝑦
∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤 ∈ ran 𝐹(𝑦 ∪ 𝑧) ⊆ 𝑤)) |
85 | 17, 24, 83, 84 | syl3anbrc 1246 |
. . . 4
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → (toInc‘ran 𝐹) ∈
Dirset) |
86 | | isnacs3 37273 |
. . . . . . 7
⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑦 ∈ 𝒫 𝐶((toInc‘𝑦) ∈ Dirset → ∪ 𝑦
∈ 𝑦))) |
87 | 86 | simprbi 480 |
. . . . . 6
⊢ (𝐶 ∈ (NoeACS‘𝑋) → ∀𝑦 ∈ 𝒫 𝐶((toInc‘𝑦) ∈ Dirset → ∪ 𝑦
∈ 𝑦)) |
88 | 87 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∀𝑦 ∈ 𝒫 𝐶((toInc‘𝑦) ∈ Dirset → ∪ 𝑦
∈ 𝑦)) |
89 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑦 = ran 𝐹 → (toInc‘𝑦) = (toInc‘ran 𝐹)) |
90 | 89 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑦 = ran 𝐹 → ((toInc‘𝑦) ∈ Dirset ↔ (toInc‘ran 𝐹) ∈
Dirset)) |
91 | | unieq 4444 |
. . . . . . . 8
⊢ (𝑦 = ran 𝐹 → ∪ 𝑦 = ∪
ran 𝐹) |
92 | | id 22 |
. . . . . . . 8
⊢ (𝑦 = ran 𝐹 → 𝑦 = ran 𝐹) |
93 | 91, 92 | eleq12d 2695 |
. . . . . . 7
⊢ (𝑦 = ran 𝐹 → (∪ 𝑦 ∈ 𝑦 ↔ ∪ ran
𝐹 ∈ ran 𝐹)) |
94 | 90, 93 | imbi12d 334 |
. . . . . 6
⊢ (𝑦 = ran 𝐹 → (((toInc‘𝑦) ∈ Dirset → ∪ 𝑦
∈ 𝑦) ↔
((toInc‘ran 𝐹) ∈
Dirset → ∪ ran 𝐹 ∈ ran 𝐹))) |
95 | 94 | rspcva 3307 |
. . . . 5
⊢ ((ran
𝐹 ∈ 𝒫 𝐶 ∧ ∀𝑦 ∈ 𝒫 𝐶((toInc‘𝑦) ∈ Dirset → ∪ 𝑦
∈ 𝑦)) →
((toInc‘ran 𝐹) ∈
Dirset → ∪ ran 𝐹 ∈ ran 𝐹)) |
96 | 15, 88, 95 | syl2anc 693 |
. . . 4
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ((toInc‘ran 𝐹) ∈ Dirset → ∪ ran 𝐹 ∈ ran 𝐹)) |
97 | 85, 96 | mpd 15 |
. . 3
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∪
ran 𝐹 ∈ ran 𝐹) |
98 | | fvelrnb 6243 |
. . . 4
⊢ (𝐹 Fn ℕ0 →
(∪ ran 𝐹 ∈ ran 𝐹 ↔ ∃𝑦 ∈ ℕ0 (𝐹‘𝑦) = ∪ ran 𝐹)) |
99 | 19, 98 | syl 17 |
. . 3
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → (∪
ran 𝐹 ∈ ran 𝐹 ↔ ∃𝑦 ∈ ℕ0
(𝐹‘𝑦) = ∪ ran 𝐹)) |
100 | 97, 99 | mpbid 222 |
. 2
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∃𝑦 ∈ ℕ0 (𝐹‘𝑦) = ∪ ran 𝐹) |
101 | 10, 100 | reximddv 3018 |
1
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0
(𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∃𝑦 ∈ ℕ0 ∀𝑧 ∈
(ℤ≥‘𝑦)(𝐹‘𝑧) = (𝐹‘𝑦)) |