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	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to \exists y \in ℕ_{0} \forall z \in ℤ_{\geq y} F (z) = F (y)$

Proof

Step	Hyp	Ref	Expression
1		fvssunirn	$⊢ F (z) \subseteq ⋃ ran F$
2		simplrr	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (y \in ℕ_{0} \land F (y) = ⋃ ran F)) \land z \in ℤ_{\geq y}) \to F (y) = ⋃ ran F$
3	1 2	sseqtrrid	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (y \in ℕ_{0} \land F (y) = ⋃ ran F)) \land z \in ℤ_{\geq y}) \to F (z) \subseteq F (y)$
4		simpll3	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (y \in ℕ_{0} \land F (y) = ⋃ ran F)) \land z \in ℤ_{\geq y}) \to \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)$
5		simplrl	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (y \in ℕ_{0} \land F (y) = ⋃ ran F)) \land z \in ℤ_{\geq y}) \to y \in ℕ_{0}$
6		simpr	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (y \in ℕ_{0} \land F (y) = ⋃ ran F)) \land z \in ℤ_{\geq y}) \to z \in ℤ_{\geq y}$
7		incssnn0	$⊢ (\forall x \in ℕ_{0} F (x) \subseteq F (x + 1) \land y \in ℕ_{0} \land z \in ℤ_{\geq y}) \to F (y) \subseteq F (z)$
8	4 5 6 7	syl3anc	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (y \in ℕ_{0} \land F (y) = ⋃ ran F)) \land z \in ℤ_{\geq y}) \to F (y) \subseteq F (z)$
9	3 8	eqssd	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (y \in ℕ_{0} \land F (y) = ⋃ ran F)) \land z \in ℤ_{\geq y}) \to F (z) = F (y)$
10	9	ralrimiva	$⊢ ((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (y \in ℕ_{0} \land F (y) = ⋃ ran F)) \to \forall z \in ℤ_{\geq y} F (z) = F (y)$
11		frn	$⊢ F : ℕ_{0} ⟶ C \to ran F \subseteq C$
12	11	3ad2ant2	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to ran F \subseteq C$
13		elpw2g	$⊢ C \in NoeACS (X) \to (ran F \in 𝒫 C \leftrightarrow ran F \subseteq C)$
14	13	3ad2ant1	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to (ran F \in 𝒫 C \leftrightarrow ran F \subseteq C)$
15	12 14	mpbird	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to ran F \in 𝒫 C$
16		elex	$⊢ ran F \in 𝒫 C \to ran F \in V$
17	15 16	syl	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to ran F \in V$
18		ffn	$⊢ F : ℕ_{0} ⟶ C \to F Fn ℕ_{0}$
19	18	3ad2ant2	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to F Fn ℕ_{0}$
20		0nn0	$⊢ 0 \in ℕ_{0}$
21		fnfvelrn	$⊢ (F Fn ℕ_{0} \land 0 \in ℕ_{0}) \to F (0) \in ran F$
22	19 20 21	sylancl	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to F (0) \in ran F$
23	22	ne0d	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to ran F \neq \emptyset$
24		nn0re	$⊢ a \in ℕ_{0} \to a \in ℝ$
25	24	ad2antrl	$⊢ ((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \to a \in ℝ$
26		nn0re	$⊢ b \in ℕ_{0} \to b \in ℝ$
27	26	ad2antll	$⊢ ((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \to b \in ℝ$
28		simplrr	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a \leq b) \to b \in ℕ_{0}$
29		simpll3	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a \leq b) \to \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)$
30		simplrl	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a \leq b) \to a \in ℕ_{0}$
31		nn0z	$⊢ a \in ℕ_{0} \to a \in ℤ$
32		nn0z	$⊢ b \in ℕ_{0} \to b \in ℤ$
33		eluz	$⊢ (a \in ℤ \land b \in ℤ) \to (b \in ℤ_{\geq a} \leftrightarrow a \leq b)$
34	31 32 33	syl2an	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to (b \in ℤ_{\geq a} \leftrightarrow a \leq b)$
35	34	biimpar	$⊢ ((a \in ℕ_{0} \land b \in ℕ_{0}) \land a \leq b) \to b \in ℤ_{\geq a}$
36	35	adantll	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a \leq b) \to b \in ℤ_{\geq a}$
37		incssnn0	$⊢ (\forall x \in ℕ_{0} F (x) \subseteq F (x + 1) \land a \in ℕ_{0} \land b \in ℤ_{\geq a}) \to F (a) \subseteq F (b)$
38	29 30 36 37	syl3anc	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a \leq b) \to F (a) \subseteq F (b)$
39		ssequn1	$⊢ F (a) \subseteq F (b) \leftrightarrow F (a) \cup F (b) = F (b)$
40	38 39	sylib	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a \leq b) \to F (a) \cup F (b) = F (b)$
41		eqimss	$⊢ F (a) \cup F (b) = F (b) \to F (a) \cup F (b) \subseteq F (b)$
42	40 41	syl	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a \leq b) \to F (a) \cup F (b) \subseteq F (b)$
43		fveq2	$⊢ c = b \to F (c) = F (b)$
44	43	sseq2d	$⊢ c = b \to (F (a) \cup F (b) \subseteq F (c) \leftrightarrow F (a) \cup F (b) \subseteq F (b))$
45	44	rspcev	$⊢ (b \in ℕ_{0} \land F (a) \cup F (b) \subseteq F (b)) \to \exists c \in ℕ_{0} F (a) \cup F (b) \subseteq F (c)$
46	28 42 45	syl2anc	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land a \leq b) \to \exists c \in ℕ_{0} F (a) \cup F (b) \subseteq F (c)$
47		simplrl	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land b \leq a) \to a \in ℕ_{0}$
48		simpll3	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land b \leq a) \to \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)$
49		simplrr	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land b \leq a) \to b \in ℕ_{0}$
50		eluz	$⊢ (b \in ℤ \land a \in ℤ) \to (a \in ℤ_{\geq b} \leftrightarrow b \leq a)$
51	32 31 50	syl2anr	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to (a \in ℤ_{\geq b} \leftrightarrow b \leq a)$
52	51	biimpar	$⊢ ((a \in ℕ_{0} \land b \in ℕ_{0}) \land b \leq a) \to a \in ℤ_{\geq b}$
53	52	adantll	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land b \leq a) \to a \in ℤ_{\geq b}$
54		incssnn0	$⊢ (\forall x \in ℕ_{0} F (x) \subseteq F (x + 1) \land b \in ℕ_{0} \land a \in ℤ_{\geq b}) \to F (b) \subseteq F (a)$
55	48 49 53 54	syl3anc	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land b \leq a) \to F (b) \subseteq F (a)$
56		ssequn2	$⊢ F (b) \subseteq F (a) \leftrightarrow F (a) \cup F (b) = F (a)$
57	55 56	sylib	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land b \leq a) \to F (a) \cup F (b) = F (a)$
58		eqimss	$⊢ F (a) \cup F (b) = F (a) \to F (a) \cup F (b) \subseteq F (a)$
59	57 58	syl	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land b \leq a) \to F (a) \cup F (b) \subseteq F (a)$
60		fveq2	$⊢ c = a \to F (c) = F (a)$
61	60	sseq2d	$⊢ c = a \to (F (a) \cup F (b) \subseteq F (c) \leftrightarrow F (a) \cup F (b) \subseteq F (a))$
62	61	rspcev	$⊢ (a \in ℕ_{0} \land F (a) \cup F (b) \subseteq F (a)) \to \exists c \in ℕ_{0} F (a) \cup F (b) \subseteq F (c)$
63	47 59 62	syl2anc	$⊢ (((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \land b \leq a) \to \exists c \in ℕ_{0} F (a) \cup F (b) \subseteq F (c)$
64	25 27 46 63	lecasei	$⊢ ((C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \land (a \in ℕ_{0} \land b \in ℕ_{0})) \to \exists c \in ℕ_{0} F (a) \cup F (b) \subseteq F (c)$
65	64	ralrimivva	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to \forall a \in ℕ_{0} \forall b \in ℕ_{0} \exists c \in ℕ_{0} F (a) \cup F (b) \subseteq F (c)$
66		uneq1	$⊢ y = F (a) \to y \cup z = F (a) \cup z$
67	66	sseq1d	$⊢ y = F (a) \to (y \cup z \subseteq w \leftrightarrow F (a) \cup z \subseteq w)$
68	67	rexbidv	$⊢ y = F (a) \to (\exists w \in ran F y \cup z \subseteq w \leftrightarrow \exists w \in ran F F (a) \cup z \subseteq w)$
69	68	ralbidv	$⊢ y = F (a) \to (\forall z \in ran F \exists w \in ran F y \cup z \subseteq w \leftrightarrow \forall z \in ran F \exists w \in ran F F (a) \cup z \subseteq w)$
70	69	ralrn	$⊢ F Fn ℕ_{0} \to (\forall y \in ran F \forall z \in ran F \exists w \in ran F y \cup z \subseteq w \leftrightarrow \forall a \in ℕ_{0} \forall z \in ran F \exists w \in ran F F (a) \cup z \subseteq w)$
71		uneq2	$⊢ z = F (b) \to F (a) \cup z = F (a) \cup F (b)$
72	71	sseq1d	$⊢ z = F (b) \to (F (a) \cup z \subseteq w \leftrightarrow F (a) \cup F (b) \subseteq w)$
73	72	rexbidv	$⊢ z = F (b) \to (\exists w \in ran F F (a) \cup z \subseteq w \leftrightarrow \exists w \in ran F F (a) \cup F (b) \subseteq w)$
74	73	ralrn	$⊢ F Fn ℕ_{0} \to (\forall z \in ran F \exists w \in ran F F (a) \cup z \subseteq w \leftrightarrow \forall b \in ℕ_{0} \exists w \in ran F F (a) \cup F (b) \subseteq w)$
75		sseq2	$⊢ w = F (c) \to (F (a) \cup F (b) \subseteq w \leftrightarrow F (a) \cup F (b) \subseteq F (c))$
76	75	rexrn	$⊢ F Fn ℕ_{0} \to (\exists w \in ran F F (a) \cup F (b) \subseteq w \leftrightarrow \exists c \in ℕ_{0} F (a) \cup F (b) \subseteq F (c))$
77	76	ralbidv	$⊢ F Fn ℕ_{0} \to (\forall b \in ℕ_{0} \exists w \in ran F F (a) \cup F (b) \subseteq w \leftrightarrow \forall b \in ℕ_{0} \exists c \in ℕ_{0} F (a) \cup F (b) \subseteq F (c))$
78	74 77	bitrd	$⊢ F Fn ℕ_{0} \to (\forall z \in ran F \exists w \in ran F F (a) \cup z \subseteq w \leftrightarrow \forall b \in ℕ_{0} \exists c \in ℕ_{0} F (a) \cup F (b) \subseteq F (c))$
79	78	ralbidv	$⊢ F Fn ℕ_{0} \to (\forall a \in ℕ_{0} \forall z \in ran F \exists w \in ran F F (a) \cup z \subseteq w \leftrightarrow \forall a \in ℕ_{0} \forall b \in ℕ_{0} \exists c \in ℕ_{0} F (a) \cup F (b) \subseteq F (c))$
80	70 79	bitrd	$⊢ F Fn ℕ_{0} \to (\forall y \in ran F \forall z \in ran F \exists w \in ran F y \cup z \subseteq w \leftrightarrow \forall a \in ℕ_{0} \forall b \in ℕ_{0} \exists c \in ℕ_{0} F (a) \cup F (b) \subseteq F (c))$
81	19 80	syl	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to (\forall y \in ran F \forall z \in ran F \exists w \in ran F y \cup z \subseteq w \leftrightarrow \forall a \in ℕ_{0} \forall b \in ℕ_{0} \exists c \in ℕ_{0} F (a) \cup F (b) \subseteq F (c))$
82	65 81	mpbird	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to \forall y \in ran F \forall z \in ran F \exists w \in ran F y \cup z \subseteq w$
83		isipodrs	$⊢ toInc (ran F) \in Dirset \leftrightarrow (ran F \in V \land ran F \neq \emptyset \land \forall y \in ran F \forall z \in ran F \exists w \in ran F y \cup z \subseteq w)$
84	17 23 82 83	syl3anbrc	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to toInc (ran F) \in Dirset$
85		isnacs3	$⊢ C \in NoeACS (X) \leftrightarrow (C \in Moore (X) \land \forall y \in 𝒫 C (toInc (y) \in Dirset \to ⋃ y \in y))$
86	85	simprbi	$⊢ C \in NoeACS (X) \to \forall y \in 𝒫 C (toInc (y) \in Dirset \to ⋃ y \in y)$
87	86	3ad2ant1	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to \forall y \in 𝒫 C (toInc (y) \in Dirset \to ⋃ y \in y)$
88		fveq2	$⊢ y = ran F \to toInc (y) = toInc (ran F)$
89	88	eleq1d	$⊢ y = ran F \to (toInc (y) \in Dirset \leftrightarrow toInc (ran F) \in Dirset)$
90		unieq	$⊢ y = ran F \to ⋃ y = ⋃ ran F$
91		id	$⊢ y = ran F \to y = ran F$
92	90 91	eleq12d	$⊢ y = ran F \to (⋃ y \in y \leftrightarrow ⋃ ran F \in ran F)$
93	89 92	imbi12d	$⊢ y = ran F \to ((toInc (y) \in Dirset \to ⋃ y \in y) \leftrightarrow (toInc (ran F) \in Dirset \to ⋃ ran F \in ran F))$
94	93	rspcva	$⊢ (ran F \in 𝒫 C \land \forall y \in 𝒫 C (toInc (y) \in Dirset \to ⋃ y \in y)) \to (toInc (ran F) \in Dirset \to ⋃ ran F \in ran F)$
95	15 87 94	syl2anc	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to (toInc (ran F) \in Dirset \to ⋃ ran F \in ran F)$
96	84 95	mpd	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to ⋃ ran F \in ran F$
97		fvelrnb	$⊢ F Fn ℕ_{0} \to (⋃ ran F \in ran F \leftrightarrow \exists y \in ℕ_{0} F (y) = ⋃ ran F)$
98	19 97	syl	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to (⋃ ran F \in ran F \leftrightarrow \exists y \in ℕ_{0} F (y) = ⋃ ran F)$
99	96 98	mpbid	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to \exists y \in ℕ_{0} F (y) = ⋃ ran F$
100	10 99	reximddv	$⊢ (C \in NoeACS (X) \land F : ℕ_{0} ⟶ C \land \forall x \in ℕ_{0} F (x) \subseteq F (x + 1)) \to \exists y \in ℕ_{0} \forall z \in ℤ_{\geq y} F (z) = F (y)$

Metamath Proof Explorer

Theorem nacsfix

Proof