lmff

Description: If F converges, there is some upper integer set on which F is a total function. (Contributed by Mario Carneiro, 31-Dec-2013)

	Ref	Expression
Hypotheses	lmff.1	$⊢ Z = ℤ_{\geq M}$
	lmff.3	$⊢ φ \to J \in TopOn (X)$
	lmff.4	$⊢ φ \to M \in ℤ$
	lmff.5	$⊢ φ \to F \in dom \underset{t}{⇝} (J)$
Assertion	lmff	$⊢ φ \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X$

Proof

Step	Hyp	Ref	Expression
1		lmff.1	$⊢ Z = ℤ_{\geq M}$
2		lmff.3	$⊢ φ \to J \in TopOn (X)$
3		lmff.4	$⊢ φ \to M \in ℤ$
4		lmff.5	$⊢ φ \to F \in dom \underset{t}{⇝} (J)$
5		eldm2g	$⊢ F \in dom \underset{t}{⇝} (J) \to (F \in dom \underset{t}{⇝} (J) \leftrightarrow \exists y ⟨F, y⟩ \in \underset{t}{⇝} (J))$
6	5	ibi	$⊢ F \in dom \underset{t}{⇝} (J) \to \exists y ⟨F, y⟩ \in \underset{t}{⇝} (J)$
7	4 6	syl	$⊢ φ \to \exists y ⟨F, y⟩ \in \underset{t}{⇝} (J)$
8		df-br	$⊢ F \underset{t}{⇝} (J) y \leftrightarrow ⟨F, y⟩ \in \underset{t}{⇝} (J)$
9	8	exbii	$⊢ \exists y F \underset{t}{⇝} (J) y \leftrightarrow \exists y ⟨F, y⟩ \in \underset{t}{⇝} (J)$
10	7 9	sylibr	$⊢ φ \to \exists y F \underset{t}{⇝} (J) y$
11		lmcl	$⊢ (J \in TopOn (X) \land F \underset{t}{⇝} (J) y) \to y \in X$
12	2 11	sylan	$⊢ (φ \land F \underset{t}{⇝} (J) y) \to y \in X$
13		eleq2	$⊢ j = X \to (y \in j \leftrightarrow y \in X)$
14		feq3	$⊢ j = X \to (({F ↾}_{x}) : x ⟶ j \leftrightarrow ({F ↾}_{x}) : x ⟶ X)$
15	14	rexbidv	$⊢ j = X \to (\exists x \in ran ℤ_{\geq} ({F ↾}_{x}) : x ⟶ j \leftrightarrow \exists x \in ran ℤ_{\geq} ({F ↾}_{x}) : x ⟶ X)$
16	13 15	imbi12d	$⊢ j = X \to ((y \in j \to \exists x \in ran ℤ_{\geq} ({F ↾}_{x}) : x ⟶ j) \leftrightarrow (y \in X \to \exists x \in ran ℤ_{\geq} ({F ↾}_{x}) : x ⟶ X))$
17	2	lmbr	$⊢ φ \to (F \underset{t}{⇝} (J) y \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land y \in X \land \forall j \in J (y \in j \to \exists x \in ran ℤ_{\geq} ({F ↾}_{x}) : x ⟶ j)))$
18	17	biimpa	$⊢ (φ \land F \underset{t}{⇝} (J) y) \to (F \in (X ↑_{𝑝𝑚} ℂ) \land y \in X \land \forall j \in J (y \in j \to \exists x \in ran ℤ_{\geq} ({F ↾}_{x}) : x ⟶ j))$
19	18	simp3d	$⊢ (φ \land F \underset{t}{⇝} (J) y) \to \forall j \in J (y \in j \to \exists x \in ran ℤ_{\geq} ({F ↾}_{x}) : x ⟶ j)$
20		toponmax	$⊢ J \in TopOn (X) \to X \in J$
21	2 20	syl	$⊢ φ \to X \in J$
22	21	adantr	$⊢ (φ \land F \underset{t}{⇝} (J) y) \to X \in J$
23	16 19 22	rspcdva	$⊢ (φ \land F \underset{t}{⇝} (J) y) \to (y \in X \to \exists x \in ran ℤ_{\geq} ({F ↾}_{x}) : x ⟶ X)$
24	12 23	mpd	$⊢ (φ \land F \underset{t}{⇝} (J) y) \to \exists x \in ran ℤ_{\geq} ({F ↾}_{x}) : x ⟶ X$
25	10 24	exlimddv	$⊢ φ \to \exists x \in ran ℤ_{\geq} ({F ↾}_{x}) : x ⟶ X$
26		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
27		ffn	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ \to ℤ_{\geq} Fn ℤ$
28		reseq2	$⊢ x = ℤ_{\geq j} \to {F ↾}_{x} = {F ↾}_{ℤ_{\geq j}}$
29		id	$⊢ x = ℤ_{\geq j} \to x = ℤ_{\geq j}$
30	28 29	feq12d	$⊢ x = ℤ_{\geq j} \to (({F ↾}_{x}) : x ⟶ X \leftrightarrow ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)$
31	30	rexrn	$⊢ ℤ_{\geq} Fn ℤ \to (\exists x \in ran ℤ_{\geq} ({F ↾}_{x}) : x ⟶ X \leftrightarrow \exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)$
32	26 27 31	mp2b	$⊢ \exists x \in ran ℤ_{\geq} ({F ↾}_{x}) : x ⟶ X \leftrightarrow \exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X$
33	25 32	sylib	$⊢ φ \to \exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X$
34	1	rexuz3	$⊢ M \in ℤ \to (\exists j \in Z \forall x \in ℤ_{\geq j} (x \in dom F \land F (x) \in X) \leftrightarrow \exists j \in ℤ \forall x \in ℤ_{\geq j} (x \in dom F \land F (x) \in X))$
35	3 34	syl	$⊢ φ \to (\exists j \in Z \forall x \in ℤ_{\geq j} (x \in dom F \land F (x) \in X) \leftrightarrow \exists j \in ℤ \forall x \in ℤ_{\geq j} (x \in dom F \land F (x) \in X))$
36	18	simp1d	$⊢ (φ \land F \underset{t}{⇝} (J) y) \to F \in (X ↑_{𝑝𝑚} ℂ)$
37	10 36	exlimddv	$⊢ φ \to F \in (X ↑_{𝑝𝑚} ℂ)$
38		pmfun	$⊢ F \in (X ↑_{𝑝𝑚} ℂ) \to Fun F$
39	37 38	syl	$⊢ φ \to Fun F$
40		ffvresb	$⊢ Fun F \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X \leftrightarrow \forall x \in ℤ_{\geq j} (x \in dom F \land F (x) \in X))$
41	39 40	syl	$⊢ φ \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X \leftrightarrow \forall x \in ℤ_{\geq j} (x \in dom F \land F (x) \in X))$
42	41	rexbidv	$⊢ φ \to (\exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X \leftrightarrow \exists j \in Z \forall x \in ℤ_{\geq j} (x \in dom F \land F (x) \in X))$
43	41	rexbidv	$⊢ φ \to (\exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X \leftrightarrow \exists j \in ℤ \forall x \in ℤ_{\geq j} (x \in dom F \land F (x) \in X))$
44	35 42 43	3bitr4d	$⊢ φ \to (\exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X \leftrightarrow \exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)$
45	33 44	mpbird	$⊢ φ \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X$

Metamath Proof Explorer

Theorem lmff

Proof