Step |
Hyp |
Ref |
Expression |
1 |
|
fvssunirn |
⊢ ( 𝐹 ‘ 𝑧 ) ⊆ ∪ ran 𝐹 |
2 |
|
simplrr |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑦 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑦 ) = ∪ ran 𝐹 ) ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑦 ) = ∪ ran 𝐹 ) |
3 |
1 2
|
sseqtrrid |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑦 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑦 ) = ∪ ran 𝐹 ) ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) |
4 |
|
simpll3 |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑦 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑦 ) = ∪ ran 𝐹 ) ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) → ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) |
5 |
|
simplrl |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑦 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑦 ) = ∪ ran 𝐹 ) ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) → 𝑦 ∈ ℕ0 ) |
6 |
|
simpr |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑦 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑦 ) = ∪ ran 𝐹 ) ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) → 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) |
7 |
|
incssnn0 |
⊢ ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑧 ) ) |
8 |
4 5 6 7
|
syl3anc |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑦 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑦 ) = ∪ ran 𝐹 ) ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑧 ) ) |
9 |
3 8
|
eqssd |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑦 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑦 ) = ∪ ran 𝐹 ) ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) ) |
10 |
9
|
ralrimiva |
⊢ ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑦 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑦 ) = ∪ ran 𝐹 ) ) → ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) ) |
11 |
|
frn |
⊢ ( 𝐹 : ℕ0 ⟶ 𝐶 → ran 𝐹 ⊆ 𝐶 ) |
12 |
11
|
3ad2ant2 |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ran 𝐹 ⊆ 𝐶 ) |
13 |
|
elpw2g |
⊢ ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) → ( ran 𝐹 ∈ 𝒫 𝐶 ↔ ran 𝐹 ⊆ 𝐶 ) ) |
14 |
13
|
3ad2ant1 |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ( ran 𝐹 ∈ 𝒫 𝐶 ↔ ran 𝐹 ⊆ 𝐶 ) ) |
15 |
12 14
|
mpbird |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ran 𝐹 ∈ 𝒫 𝐶 ) |
16 |
|
elex |
⊢ ( ran 𝐹 ∈ 𝒫 𝐶 → ran 𝐹 ∈ V ) |
17 |
15 16
|
syl |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ran 𝐹 ∈ V ) |
18 |
|
ffn |
⊢ ( 𝐹 : ℕ0 ⟶ 𝐶 → 𝐹 Fn ℕ0 ) |
19 |
18
|
3ad2ant2 |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → 𝐹 Fn ℕ0 ) |
20 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
21 |
|
fnfvelrn |
⊢ ( ( 𝐹 Fn ℕ0 ∧ 0 ∈ ℕ0 ) → ( 𝐹 ‘ 0 ) ∈ ran 𝐹 ) |
22 |
19 20 21
|
sylancl |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ( 𝐹 ‘ 0 ) ∈ ran 𝐹 ) |
23 |
22
|
ne0d |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ran 𝐹 ≠ ∅ ) |
24 |
|
nn0re |
⊢ ( 𝑎 ∈ ℕ0 → 𝑎 ∈ ℝ ) |
25 |
24
|
ad2antrl |
⊢ ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) → 𝑎 ∈ ℝ ) |
26 |
|
nn0re |
⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℝ ) |
27 |
26
|
ad2antll |
⊢ ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) → 𝑏 ∈ ℝ ) |
28 |
|
simplrr |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑎 ≤ 𝑏 ) → 𝑏 ∈ ℕ0 ) |
29 |
|
simpll3 |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑎 ≤ 𝑏 ) → ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) |
30 |
|
simplrl |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑎 ≤ 𝑏 ) → 𝑎 ∈ ℕ0 ) |
31 |
|
nn0z |
⊢ ( 𝑎 ∈ ℕ0 → 𝑎 ∈ ℤ ) |
32 |
|
nn0z |
⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℤ ) |
33 |
|
eluz |
⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑏 ∈ ( ℤ≥ ‘ 𝑎 ) ↔ 𝑎 ≤ 𝑏 ) ) |
34 |
31 32 33
|
syl2an |
⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑏 ∈ ( ℤ≥ ‘ 𝑎 ) ↔ 𝑎 ≤ 𝑏 ) ) |
35 |
34
|
biimpar |
⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑎 ≤ 𝑏 ) → 𝑏 ∈ ( ℤ≥ ‘ 𝑎 ) ) |
36 |
35
|
adantll |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑎 ≤ 𝑏 ) → 𝑏 ∈ ( ℤ≥ ‘ 𝑎 ) ) |
37 |
|
incssnn0 |
⊢ ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝑎 ) ) → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) |
38 |
29 30 36 37
|
syl3anc |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑎 ≤ 𝑏 ) → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) |
39 |
|
ssequn1 |
⊢ ( ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑏 ) ↔ ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑏 ) ) |
40 |
38 39
|
sylib |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑎 ≤ 𝑏 ) → ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑏 ) ) |
41 |
|
eqimss |
⊢ ( ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑏 ) → ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑏 ) ) |
42 |
40 41
|
syl |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑎 ≤ 𝑏 ) → ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑏 ) ) |
43 |
|
fveq2 |
⊢ ( 𝑐 = 𝑏 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝑏 ) ) |
44 |
43
|
sseq2d |
⊢ ( 𝑐 = 𝑏 → ( ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ↔ ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑏 ) ) ) |
45 |
44
|
rspcev |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑏 ) ) → ∃ 𝑐 ∈ ℕ0 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) |
46 |
28 42 45
|
syl2anc |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑎 ≤ 𝑏 ) → ∃ 𝑐 ∈ ℕ0 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) |
47 |
|
simplrl |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑏 ≤ 𝑎 ) → 𝑎 ∈ ℕ0 ) |
48 |
|
simpll3 |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑏 ≤ 𝑎 ) → ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) |
49 |
|
simplrr |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑏 ≤ 𝑎 ) → 𝑏 ∈ ℕ0 ) |
50 |
|
eluz |
⊢ ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) → ( 𝑎 ∈ ( ℤ≥ ‘ 𝑏 ) ↔ 𝑏 ≤ 𝑎 ) ) |
51 |
32 31 50
|
syl2anr |
⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑎 ∈ ( ℤ≥ ‘ 𝑏 ) ↔ 𝑏 ≤ 𝑎 ) ) |
52 |
51
|
biimpar |
⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑏 ≤ 𝑎 ) → 𝑎 ∈ ( ℤ≥ ‘ 𝑏 ) ) |
53 |
52
|
adantll |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑏 ≤ 𝑎 ) → 𝑎 ∈ ( ℤ≥ ‘ 𝑏 ) ) |
54 |
|
incssnn0 |
⊢ ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝑏 ∈ ℕ0 ∧ 𝑎 ∈ ( ℤ≥ ‘ 𝑏 ) ) → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ 𝑎 ) ) |
55 |
48 49 53 54
|
syl3anc |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑏 ≤ 𝑎 ) → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ 𝑎 ) ) |
56 |
|
ssequn2 |
⊢ ( ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ 𝑎 ) ↔ ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑎 ) ) |
57 |
55 56
|
sylib |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑏 ≤ 𝑎 ) → ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑎 ) ) |
58 |
|
eqimss |
⊢ ( ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑎 ) → ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑎 ) ) |
59 |
57 58
|
syl |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑏 ≤ 𝑎 ) → ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑎 ) ) |
60 |
|
fveq2 |
⊢ ( 𝑐 = 𝑎 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝑎 ) ) |
61 |
60
|
sseq2d |
⊢ ( 𝑐 = 𝑎 → ( ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ↔ ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑎 ) ) ) |
62 |
61
|
rspcev |
⊢ ( ( 𝑎 ∈ ℕ0 ∧ ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑎 ) ) → ∃ 𝑐 ∈ ℕ0 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) |
63 |
47 59 62
|
syl2anc |
⊢ ( ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) ∧ 𝑏 ≤ 𝑎 ) → ∃ 𝑐 ∈ ℕ0 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) |
64 |
25 27 46 63
|
lecasei |
⊢ ( ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) → ∃ 𝑐 ∈ ℕ0 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) |
65 |
64
|
ralrimivva |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ∀ 𝑎 ∈ ℕ0 ∀ 𝑏 ∈ ℕ0 ∃ 𝑐 ∈ ℕ0 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) |
66 |
|
uneq1 |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑎 ) → ( 𝑦 ∪ 𝑧 ) = ( ( 𝐹 ‘ 𝑎 ) ∪ 𝑧 ) ) |
67 |
66
|
sseq1d |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑎 ) → ( ( 𝑦 ∪ 𝑧 ) ⊆ 𝑤 ↔ ( ( 𝐹 ‘ 𝑎 ) ∪ 𝑧 ) ⊆ 𝑤 ) ) |
68 |
67
|
rexbidv |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑎 ) → ( ∃ 𝑤 ∈ ran 𝐹 ( 𝑦 ∪ 𝑧 ) ⊆ 𝑤 ↔ ∃ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) ∪ 𝑧 ) ⊆ 𝑤 ) ) |
69 |
68
|
ralbidv |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑎 ) → ( ∀ 𝑧 ∈ ran 𝐹 ∃ 𝑤 ∈ ran 𝐹 ( 𝑦 ∪ 𝑧 ) ⊆ 𝑤 ↔ ∀ 𝑧 ∈ ran 𝐹 ∃ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) ∪ 𝑧 ) ⊆ 𝑤 ) ) |
70 |
69
|
ralrn |
⊢ ( 𝐹 Fn ℕ0 → ( ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐹 ∃ 𝑤 ∈ ran 𝐹 ( 𝑦 ∪ 𝑧 ) ⊆ 𝑤 ↔ ∀ 𝑎 ∈ ℕ0 ∀ 𝑧 ∈ ran 𝐹 ∃ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) ∪ 𝑧 ) ⊆ 𝑤 ) ) |
71 |
|
uneq2 |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑏 ) → ( ( 𝐹 ‘ 𝑎 ) ∪ 𝑧 ) = ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ) |
72 |
71
|
sseq1d |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑏 ) → ( ( ( 𝐹 ‘ 𝑎 ) ∪ 𝑧 ) ⊆ 𝑤 ↔ ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ 𝑤 ) ) |
73 |
72
|
rexbidv |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑏 ) → ( ∃ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) ∪ 𝑧 ) ⊆ 𝑤 ↔ ∃ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ 𝑤 ) ) |
74 |
73
|
ralrn |
⊢ ( 𝐹 Fn ℕ0 → ( ∀ 𝑧 ∈ ran 𝐹 ∃ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) ∪ 𝑧 ) ⊆ 𝑤 ↔ ∀ 𝑏 ∈ ℕ0 ∃ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ 𝑤 ) ) |
75 |
|
sseq2 |
⊢ ( 𝑤 = ( 𝐹 ‘ 𝑐 ) → ( ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ 𝑤 ↔ ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) ) |
76 |
75
|
rexrn |
⊢ ( 𝐹 Fn ℕ0 → ( ∃ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ 𝑤 ↔ ∃ 𝑐 ∈ ℕ0 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) ) |
77 |
76
|
ralbidv |
⊢ ( 𝐹 Fn ℕ0 → ( ∀ 𝑏 ∈ ℕ0 ∃ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ 𝑤 ↔ ∀ 𝑏 ∈ ℕ0 ∃ 𝑐 ∈ ℕ0 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) ) |
78 |
74 77
|
bitrd |
⊢ ( 𝐹 Fn ℕ0 → ( ∀ 𝑧 ∈ ran 𝐹 ∃ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) ∪ 𝑧 ) ⊆ 𝑤 ↔ ∀ 𝑏 ∈ ℕ0 ∃ 𝑐 ∈ ℕ0 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) ) |
79 |
78
|
ralbidv |
⊢ ( 𝐹 Fn ℕ0 → ( ∀ 𝑎 ∈ ℕ0 ∀ 𝑧 ∈ ran 𝐹 ∃ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) ∪ 𝑧 ) ⊆ 𝑤 ↔ ∀ 𝑎 ∈ ℕ0 ∀ 𝑏 ∈ ℕ0 ∃ 𝑐 ∈ ℕ0 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) ) |
80 |
70 79
|
bitrd |
⊢ ( 𝐹 Fn ℕ0 → ( ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐹 ∃ 𝑤 ∈ ran 𝐹 ( 𝑦 ∪ 𝑧 ) ⊆ 𝑤 ↔ ∀ 𝑎 ∈ ℕ0 ∀ 𝑏 ∈ ℕ0 ∃ 𝑐 ∈ ℕ0 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) ) |
81 |
19 80
|
syl |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ( ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐹 ∃ 𝑤 ∈ ran 𝐹 ( 𝑦 ∪ 𝑧 ) ⊆ 𝑤 ↔ ∀ 𝑎 ∈ ℕ0 ∀ 𝑏 ∈ ℕ0 ∃ 𝑐 ∈ ℕ0 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) ) |
82 |
65 81
|
mpbird |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐹 ∃ 𝑤 ∈ ran 𝐹 ( 𝑦 ∪ 𝑧 ) ⊆ 𝑤 ) |
83 |
|
isipodrs |
⊢ ( ( toInc ‘ ran 𝐹 ) ∈ Dirset ↔ ( ran 𝐹 ∈ V ∧ ran 𝐹 ≠ ∅ ∧ ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐹 ∃ 𝑤 ∈ ran 𝐹 ( 𝑦 ∪ 𝑧 ) ⊆ 𝑤 ) ) |
84 |
17 23 82 83
|
syl3anbrc |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ( toInc ‘ ran 𝐹 ) ∈ Dirset ) |
85 |
|
isnacs3 |
⊢ ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑦 ) ∈ Dirset → ∪ 𝑦 ∈ 𝑦 ) ) ) |
86 |
85
|
simprbi |
⊢ ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) → ∀ 𝑦 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑦 ) ∈ Dirset → ∪ 𝑦 ∈ 𝑦 ) ) |
87 |
86
|
3ad2ant1 |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ∀ 𝑦 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑦 ) ∈ Dirset → ∪ 𝑦 ∈ 𝑦 ) ) |
88 |
|
fveq2 |
⊢ ( 𝑦 = ran 𝐹 → ( toInc ‘ 𝑦 ) = ( toInc ‘ ran 𝐹 ) ) |
89 |
88
|
eleq1d |
⊢ ( 𝑦 = ran 𝐹 → ( ( toInc ‘ 𝑦 ) ∈ Dirset ↔ ( toInc ‘ ran 𝐹 ) ∈ Dirset ) ) |
90 |
|
unieq |
⊢ ( 𝑦 = ran 𝐹 → ∪ 𝑦 = ∪ ran 𝐹 ) |
91 |
|
id |
⊢ ( 𝑦 = ran 𝐹 → 𝑦 = ran 𝐹 ) |
92 |
90 91
|
eleq12d |
⊢ ( 𝑦 = ran 𝐹 → ( ∪ 𝑦 ∈ 𝑦 ↔ ∪ ran 𝐹 ∈ ran 𝐹 ) ) |
93 |
89 92
|
imbi12d |
⊢ ( 𝑦 = ran 𝐹 → ( ( ( toInc ‘ 𝑦 ) ∈ Dirset → ∪ 𝑦 ∈ 𝑦 ) ↔ ( ( toInc ‘ ran 𝐹 ) ∈ Dirset → ∪ ran 𝐹 ∈ ran 𝐹 ) ) ) |
94 |
93
|
rspcva |
⊢ ( ( ran 𝐹 ∈ 𝒫 𝐶 ∧ ∀ 𝑦 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑦 ) ∈ Dirset → ∪ 𝑦 ∈ 𝑦 ) ) → ( ( toInc ‘ ran 𝐹 ) ∈ Dirset → ∪ ran 𝐹 ∈ ran 𝐹 ) ) |
95 |
15 87 94
|
syl2anc |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ( ( toInc ‘ ran 𝐹 ) ∈ Dirset → ∪ ran 𝐹 ∈ ran 𝐹 ) ) |
96 |
84 95
|
mpd |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ∪ ran 𝐹 ∈ ran 𝐹 ) |
97 |
|
fvelrnb |
⊢ ( 𝐹 Fn ℕ0 → ( ∪ ran 𝐹 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ ℕ0 ( 𝐹 ‘ 𝑦 ) = ∪ ran 𝐹 ) ) |
98 |
19 97
|
syl |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ( ∪ ran 𝐹 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ ℕ0 ( 𝐹 ‘ 𝑦 ) = ∪ ran 𝐹 ) ) |
99 |
96 98
|
mpbid |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ∃ 𝑦 ∈ ℕ0 ( 𝐹 ‘ 𝑦 ) = ∪ ran 𝐹 ) |
100 |
10 99
|
reximddv |
⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) ) |