Metamath Proof Explorer

Theorem nacsfix

Description: An increasing sequence of closed sets in a Noetherian-type closure system eventually fixates. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Assertion nacsfix ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝐹 : ℕ0 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )

Proof

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 ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )