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