poimir

Description: Poincare-Miranda theorem. Theorem on Kulpa p. 547. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimir.i	$⊢ I = {[0, 1]}^{(1 \dots N)}$
	poimir.r	$⊢ R = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\})$
	poimir.1	$⊢ φ \to F \in ((R ↾_{𝑡} I) Cn R)$
	poimir.2	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 0)) \to F (z) (n) \leq 0$
	poimir.3	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 1)) \to 0 \leq F (z) (n)$
Assertion	poimir	$⊢ φ \to \exists c \in I F (c) = (1 \dots N) \times \{0\}$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimir.i	$⊢ I = {[0, 1]}^{(1 \dots N)}$
3		poimir.r	$⊢ R = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\})$
4		poimir.1	$⊢ φ \to F \in ((R ↾_{𝑡} I) Cn R)$
5		poimir.2	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 0)) \to F (z) (n) \leq 0$
6		poimir.3	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 1)) \to 0 \leq F (z) (n)$
7	1 2 3 4 5 6	poimirlem32	$⊢ φ \to \exists c \in I \forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
8		ovex	$⊢ (1 \dots N) \in V$
9		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
10	3	pttoponconst	$⊢ ((1 \dots N) \in V \land topGen (ran (.)) \in TopOn (ℝ)) \to R \in TopOn (ℝ^{(1 \dots N)})$
11	8 9 10	mp2an	$⊢ R \in TopOn (ℝ^{(1 \dots N)})$
12	11	topontopi	$⊢ R \in Top$
13		reex	$⊢ ℝ \in V$
14		unitssre	$⊢ [0, 1] \subseteq ℝ$
15		mapss	$⊢ (ℝ \in V \land [0, 1] \subseteq ℝ) \to {[0, 1]}^{(1 \dots N)} \subseteq ℝ^{(1 \dots N)}$
16	13 14 15	mp2an	$⊢ {[0, 1]}^{(1 \dots N)} \subseteq ℝ^{(1 \dots N)}$
17	2 16	eqsstri	$⊢ I \subseteq ℝ^{(1 \dots N)}$
18	11	toponunii	$⊢ ℝ^{(1 \dots N)} = ⋃ R$
19	18	restuni	$⊢ (R \in Top \land I \subseteq ℝ^{(1 \dots N)}) \to I = ⋃ (R ↾_{𝑡} I)$
20	12 17 19	mp2an	$⊢ I = ⋃ (R ↾_{𝑡} I)$
21	20 18	cnf	$⊢ F \in ((R ↾_{𝑡} I) Cn R) \to F : I ⟶ ℝ^{(1 \dots N)}$
22	4 21	syl	$⊢ φ \to F : I ⟶ ℝ^{(1 \dots N)}$
23	22	ffvelcdmda	$⊢ (φ \land c \in I) \to F (c) \in (ℝ^{(1 \dots N)})$
24		elmapi	$⊢ F (c) \in (ℝ^{(1 \dots N)}) \to F (c) : (1 \dots N) ⟶ ℝ$
25	23 24	syl	$⊢ (φ \land c \in I) \to F (c) : (1 \dots N) ⟶ ℝ$
26	25	ffvelcdmda	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to F (c) (n) \in ℝ$
27		recn	$⊢ F (c) (n) \in ℝ \to F (c) (n) \in ℂ$
28		absrpcl	$⊢ (F (c) (n) \in ℂ \land F (c) (n) \neq 0) \to \|F (c) (n)\| \in ℝ^{+}$
29	28	ex	$⊢ F (c) (n) \in ℂ \to (F (c) (n) \neq 0 \to \|F (c) (n)\| \in ℝ^{+})$
30	27 29	syl	$⊢ F (c) (n) \in ℝ \to (F (c) (n) \neq 0 \to \|F (c) (n)\| \in ℝ^{+})$
31		ltsubrp	$⊢ (F (c) (n) \in ℝ \land \|F (c) (n)\| \in ℝ^{+}) \to F (c) (n) - \|F (c) (n)\| < F (c) (n)$
32		ltaddrp	$⊢ (F (c) (n) \in ℝ \land \|F (c) (n)\| \in ℝ^{+}) \to F (c) (n) < F (c) (n) + \|F (c) (n)\|$
33	31 32	jca	$⊢ (F (c) (n) \in ℝ \land \|F (c) (n)\| \in ℝ^{+}) \to (F (c) (n) - \|F (c) (n)\| < F (c) (n) \land F (c) (n) < F (c) (n) + \|F (c) (n)\|)$
34	33	ex	$⊢ F (c) (n) \in ℝ \to (\|F (c) (n)\| \in ℝ^{+} \to (F (c) (n) - \|F (c) (n)\| < F (c) (n) \land F (c) (n) < F (c) (n) + \|F (c) (n)\|))$
35	30 34	syld	$⊢ F (c) (n) \in ℝ \to (F (c) (n) \neq 0 \to (F (c) (n) - \|F (c) (n)\| < F (c) (n) \land F (c) (n) < F (c) (n) + \|F (c) (n)\|))$
36	27	abscld	$⊢ F (c) (n) \in ℝ \to \|F (c) (n)\| \in ℝ$
37		resubcl	$⊢ (F (c) (n) \in ℝ \land \|F (c) (n)\| \in ℝ) \to F (c) (n) - \|F (c) (n)\| \in ℝ$
38	36 37	mpdan	$⊢ F (c) (n) \in ℝ \to F (c) (n) - \|F (c) (n)\| \in ℝ$
39	38	rexrd	$⊢ F (c) (n) \in ℝ \to F (c) (n) - \|F (c) (n)\| \in ℝ^{*}$
40		readdcl	$⊢ (F (c) (n) \in ℝ \land \|F (c) (n)\| \in ℝ) \to F (c) (n) + \|F (c) (n)\| \in ℝ$
41	36 40	mpdan	$⊢ F (c) (n) \in ℝ \to F (c) (n) + \|F (c) (n)\| \in ℝ$
42	41	rexrd	$⊢ F (c) (n) \in ℝ \to F (c) (n) + \|F (c) (n)\| \in ℝ^{*}$
43		rexr	$⊢ F (c) (n) \in ℝ \to F (c) (n) \in ℝ^{*}$
44		elioo5	$⊢ (F (c) (n) - \|F (c) (n)\| \in ℝ^{} \land F (c) (n) + \|F (c) (n)\| \in ℝ^{} \land F (c) (n) \in ℝ^{*}) \to (F (c) (n) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \leftrightarrow (F (c) (n) - \|F (c) (n)\| < F (c) (n) \land F (c) (n) < F (c) (n) + \|F (c) (n)\|))$
45	39 42 43 44	syl3anc	$⊢ F (c) (n) \in ℝ \to (F (c) (n) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \leftrightarrow (F (c) (n) - \|F (c) (n)\| < F (c) (n) \land F (c) (n) < F (c) (n) + \|F (c) (n)\|))$
46	35 45	sylibrd	$⊢ F (c) (n) \in ℝ \to (F (c) (n) \neq 0 \to F (c) (n) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|))$
47	26 46	syl	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to (F (c) (n) \neq 0 \to F (c) (n) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|))$
48		fveq2	$⊢ x = c \to F (x) = F (c)$
49	48	fveq1d	$⊢ x = c \to F (x) (n) = F (c) (n)$
50		eqid	$⊢ (x \in I ⟼ F (x) (n)) = (x \in I ⟼ F (x) (n))$
51		fvex	$⊢ F (c) (n) \in V$
52	49 50 51	fvmpt	$⊢ c \in I \to (x \in I ⟼ F (x) (n)) (c) = F (c) (n)$
53	52	eleq1d	$⊢ c \in I \to ((x \in I ⟼ F (x) (n)) (c) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \leftrightarrow F (c) (n) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|))$
54	53	ad2antlr	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to ((x \in I ⟼ F (x) (n)) (c) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \leftrightarrow F (c) (n) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|))$
55	47 54	sylibrd	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to (F (c) (n) \neq 0 \to (x \in I ⟼ F (x) (n)) (c) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|))$
56		iooretop	$⊢ (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \in topGen (ran (.))$
57		resttopon	$⊢ (R \in TopOn (ℝ^{(1 \dots N)}) \land I \subseteq ℝ^{(1 \dots N)}) \to R ↾_{𝑡} I \in TopOn (I)$
58	11 17 57	mp2an	$⊢ R ↾_{𝑡} I \in TopOn (I)$
59	58	a1i	$⊢ (φ \land n \in (1 \dots N)) \to R ↾_{𝑡} I \in TopOn (I)$
60	22	feqmptd	$⊢ φ \to F = (x \in I ⟼ F (x))$
61	60 4	eqeltrrd	$⊢ φ \to (x \in I ⟼ F (x)) \in ((R ↾_{𝑡} I) Cn R)$
62	61	adantr	$⊢ (φ \land n \in (1 \dots N)) \to (x \in I ⟼ F (x)) \in ((R ↾_{𝑡} I) Cn R)$
63	11	a1i	$⊢ (φ \land n \in (1 \dots N)) \to R \in TopOn (ℝ^{(1 \dots N)})$
64		retop	$⊢ topGen (ran (.)) \in Top$
65	64	fconst6	$⊢ ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Top$
66	18 3	ptpjcn	$⊢ ((1 \dots N) \in V \land ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Top \land n \in (1 \dots N)) \to (z \in (ℝ^{(1 \dots N)}) ⟼ z (n)) \in (R Cn ((1 \dots N) \times \{topGen (ran (.))\}) (n))$
67	8 65 66	mp3an12	$⊢ n \in (1 \dots N) \to (z \in (ℝ^{(1 \dots N)}) ⟼ z (n)) \in (R Cn ((1 \dots N) \times \{topGen (ran (.))\}) (n))$
68		fvex	$⊢ topGen (ran (.)) \in V$
69	68	fvconst2	$⊢ n \in (1 \dots N) \to ((1 \dots N) \times \{topGen (ran (.))\}) (n) = topGen (ran (.))$
70	69	oveq2d	$⊢ n \in (1 \dots N) \to R Cn ((1 \dots N) \times \{topGen (ran (.))\}) (n) = R Cn topGen (ran (.))$
71	67 70	eleqtrd	$⊢ n \in (1 \dots N) \to (z \in (ℝ^{(1 \dots N)}) ⟼ z (n)) \in (R Cn topGen (ran (.)))$
72	71	adantl	$⊢ (φ \land n \in (1 \dots N)) \to (z \in (ℝ^{(1 \dots N)}) ⟼ z (n)) \in (R Cn topGen (ran (.)))$
73		fveq1	$⊢ z = F (x) \to z (n) = F (x) (n)$
74	59 62 63 72 73	cnmpt11	$⊢ (φ \land n \in (1 \dots N)) \to (x \in I ⟼ F (x) (n)) \in ((R ↾_{𝑡} I) Cn topGen (ran (.)))$
75	20	cncnpi	$⊢ ((x \in I ⟼ F (x) (n)) \in ((R ↾_{𝑡} I) Cn topGen (ran (.))) \land c \in I) \to (x \in I ⟼ F (x) (n)) \in ((R ↾_{𝑡} I) CnP topGen (ran (.))) (c)$
76	74 75	sylan	$⊢ ((φ \land n \in (1 \dots N)) \land c \in I) \to (x \in I ⟼ F (x) (n)) \in ((R ↾_{𝑡} I) CnP topGen (ran (.))) (c)$
77	76	an32s	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to (x \in I ⟼ F (x) (n)) \in ((R ↾_{𝑡} I) CnP topGen (ran (.))) (c)$
78		iscnp	$⊢ (R ↾_{𝑡} I \in TopOn (I) \land topGen (ran (.)) \in TopOn (ℝ) \land c \in I) \to ((x \in I ⟼ F (x) (n)) \in ((R ↾_{𝑡} I) CnP topGen (ran (.))) (c) \leftrightarrow ((x \in I ⟼ F (x) (n)) : I ⟶ ℝ \land \forall z \in topGen (ran (.)) ((x \in I ⟼ F (x) (n)) (c) \in z \to \exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq z))))$
79	58 9 78	mp3an12	$⊢ c \in I \to ((x \in I ⟼ F (x) (n)) \in ((R ↾_{𝑡} I) CnP topGen (ran (.))) (c) \leftrightarrow ((x \in I ⟼ F (x) (n)) : I ⟶ ℝ \land \forall z \in topGen (ran (.)) ((x \in I ⟼ F (x) (n)) (c) \in z \to \exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq z))))$
80	79	ad2antlr	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to ((x \in I ⟼ F (x) (n)) \in ((R ↾_{𝑡} I) CnP topGen (ran (.))) (c) \leftrightarrow ((x \in I ⟼ F (x) (n)) : I ⟶ ℝ \land \forall z \in topGen (ran (.)) ((x \in I ⟼ F (x) (n)) (c) \in z \to \exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq z))))$
81	77 80	mpbid	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to ((x \in I ⟼ F (x) (n)) : I ⟶ ℝ \land \forall z \in topGen (ran (.)) ((x \in I ⟼ F (x) (n)) (c) \in z \to \exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq z)))$
82	81	simprd	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to \forall z \in topGen (ran (.)) ((x \in I ⟼ F (x) (n)) (c) \in z \to \exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq z))$
83		eleq2	$⊢ z = (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to ((x \in I ⟼ F (x) (n)) (c) \in z \leftrightarrow (x \in I ⟼ F (x) (n)) (c) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|))$
84		sseq2	$⊢ z = (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to ((x \in I ⟼ F (x) (n)) [v] \subseteq z \leftrightarrow (x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|))$
85	84	anbi2d	$⊢ z = (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to ((c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq z) \leftrightarrow (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|)))$
86	85	rexbidv	$⊢ z = (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to (\exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq z) \leftrightarrow \exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|)))$
87	83 86	imbi12d	$⊢ z = (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to (((x \in I ⟼ F (x) (n)) (c) \in z \to \exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq z)) \leftrightarrow ((x \in I ⟼ F (x) (n)) (c) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to \exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|))))$
88	87	rspcv	$⊢ (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \in topGen (ran (.)) \to (\forall z \in topGen (ran (.)) ((x \in I ⟼ F (x) (n)) (c) \in z \to \exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq z)) \to ((x \in I ⟼ F (x) (n)) (c) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to \exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|))))$
89	56 82 88	mpsyl	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to ((x \in I ⟼ F (x) (n)) (c) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to \exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|)))$
90	55 89	syld	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to (F (c) (n) \neq 0 \to \exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|)))$
91		0re	$⊢ 0 \in ℝ$
92		letric	$⊢ (F (c) (n) \in ℝ \land 0 \in ℝ) \to (F (c) (n) \leq 0 \lor 0 \leq F (c) (n))$
93	26 91 92	sylancl	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to (F (c) (n) \leq 0 \lor 0 \leq F (c) (n))$
94	90 93	jctird	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to (F (c) (n) \neq 0 \to (\exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|)) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n))))$
95		r19.41v	$⊢ \exists v \in (R ↾_{𝑡} I) ((c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|)) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n))) \leftrightarrow (\exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|)) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n)))$
96		anass	$⊢ ((c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|)) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n))) \leftrightarrow (c \in v \land ((x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n))))$
97	96	rexbii	$⊢ \exists v \in (R ↾_{𝑡} I) ((c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|)) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n))) \leftrightarrow \exists v \in (R ↾_{𝑡} I) (c \in v \land ((x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n))))$
98	95 97	bitr3i	$⊢ (\exists v \in (R ↾_{𝑡} I) (c \in v \land (x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|)) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n))) \leftrightarrow \exists v \in (R ↾_{𝑡} I) (c \in v \land ((x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n))))$
99	94 98	imbitrdi	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to (F (c) (n) \neq 0 \to \exists v \in (R ↾_{𝑡} I) (c \in v \land ((x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n)))))$
100	58	topontopi	$⊢ R ↾_{𝑡} I \in Top$
101	20	eltopss	$⊢ (R ↾_{𝑡} I \in Top \land v \in (R ↾_{𝑡} I)) \to v \subseteq I$
102	100 101	mpan	$⊢ v \in (R ↾_{𝑡} I) \to v \subseteq I$
103		fvex	$⊢ F (x) (n) \in V$
104	103 50	dmmpti	$⊢ dom (x \in I ⟼ F (x) (n)) = I$
105	104	sseq2i	$⊢ v \subseteq dom (x \in I ⟼ F (x) (n)) \leftrightarrow v \subseteq I$
106		funmpt	$⊢ Fun (x \in I ⟼ F (x) (n))$
107		funimass4	$⊢ (Fun (x \in I ⟼ F (x) (n)) \land v \subseteq dom (x \in I ⟼ F (x) (n))) \to ((x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \leftrightarrow \forall z \in v (x \in I ⟼ F (x) (n)) (z) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|))$
108	106 107	mpan	$⊢ v \subseteq dom (x \in I ⟼ F (x) (n)) \to ((x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \leftrightarrow \forall z \in v (x \in I ⟼ F (x) (n)) (z) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|))$
109	105 108	sylbir	$⊢ v \subseteq I \to ((x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \leftrightarrow \forall z \in v (x \in I ⟼ F (x) (n)) (z) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|))$
110		ssel2	$⊢ (v \subseteq I \land z \in v) \to z \in I$
111		fveq2	$⊢ x = z \to F (x) = F (z)$
112	111	fveq1d	$⊢ x = z \to F (x) (n) = F (z) (n)$
113		fvex	$⊢ F (z) (n) \in V$
114	112 50 113	fvmpt	$⊢ z \in I \to (x \in I ⟼ F (x) (n)) (z) = F (z) (n)$
115	114	eleq1d	$⊢ z \in I \to ((x \in I ⟼ F (x) (n)) (z) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \leftrightarrow F (z) (n) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|))$
116		eliooord	$⊢ F (z) (n) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|)$
117	115 116	syl6bi	$⊢ z \in I \to ((x \in I ⟼ F (x) (n)) (z) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|))$
118	110 117	syl	$⊢ (v \subseteq I \land z \in v) \to ((x \in I ⟼ F (x) (n)) (z) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|))$
119	118	ralimdva	$⊢ v \subseteq I \to (\forall z \in v (x \in I ⟼ F (x) (n)) (z) \in (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to \forall z \in v (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|))$
120	109 119	sylbid	$⊢ v \subseteq I \to ((x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to \forall z \in v (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|))$
121	120	adantl	$⊢ (((φ \land c \in I) \land n \in (1 \dots N)) \land v \subseteq I) \to ((x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \to \forall z \in v (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|))$
122		absnid	$⊢ (F (c) (n) \in ℝ \land F (c) (n) \leq 0) \to \|F (c) (n)\| = - F (c) (n)$
123	122	oveq2d	$⊢ (F (c) (n) \in ℝ \land F (c) (n) \leq 0) \to F (c) (n) + \|F (c) (n)\| = F (c) (n) + (- F (c) (n))$
124	27	negidd	$⊢ F (c) (n) \in ℝ \to F (c) (n) + (- F (c) (n)) = 0$
125	124	adantr	$⊢ (F (c) (n) \in ℝ \land F (c) (n) \leq 0) \to F (c) (n) + (- F (c) (n)) = 0$
126	123 125	eqtrd	$⊢ (F (c) (n) \in ℝ \land F (c) (n) \leq 0) \to F (c) (n) + \|F (c) (n)\| = 0$
127	26 126	sylan	$⊢ (((φ \land c \in I) \land n \in (1 \dots N)) \land F (c) (n) \leq 0) \to F (c) (n) + \|F (c) (n)\| = 0$
128	127	adantr	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land F (c) (n) \leq 0) \land z \in I) \to F (c) (n) + \|F (c) (n)\| = 0$
129	128	breq2d	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land F (c) (n) \leq 0) \land z \in I) \to (F (z) (n) < F (c) (n) + \|F (c) (n)\| \leftrightarrow F (z) (n) < 0)$
130	22	ffvelcdmda	$⊢ (φ \land z \in I) \to F (z) \in (ℝ^{(1 \dots N)})$
131		elmapi	$⊢ F (z) \in (ℝ^{(1 \dots N)}) \to F (z) : (1 \dots N) ⟶ ℝ$
132	130 131	syl	$⊢ (φ \land z \in I) \to F (z) : (1 \dots N) ⟶ ℝ$
133	132	ffvelcdmda	$⊢ ((φ \land z \in I) \land n \in (1 \dots N)) \to F (z) (n) \in ℝ$
134	133	an32s	$⊢ ((φ \land n \in (1 \dots N)) \land z \in I) \to F (z) (n) \in ℝ$
135		0red	$⊢ ((φ \land n \in (1 \dots N)) \land z \in I) \to 0 \in ℝ$
136	134 135	ltnled	$⊢ ((φ \land n \in (1 \dots N)) \land z \in I) \to (F (z) (n) < 0 \leftrightarrow \neg 0 \leq F (z) (n))$
137	136	adantllr	$⊢ (((φ \land c \in I) \land n \in (1 \dots N)) \land z \in I) \to (F (z) (n) < 0 \leftrightarrow \neg 0 \leq F (z) (n))$
138	137	adantlr	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land F (c) (n) \leq 0) \land z \in I) \to (F (z) (n) < 0 \leftrightarrow \neg 0 \leq F (z) (n))$
139	129 138	bitrd	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land F (c) (n) \leq 0) \land z \in I) \to (F (z) (n) < F (c) (n) + \|F (c) (n)\| \leftrightarrow \neg 0 \leq F (z) (n))$
140	139	biimpd	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land F (c) (n) \leq 0) \land z \in I) \to (F (z) (n) < F (c) (n) + \|F (c) (n)\| \to \neg 0 \leq F (z) (n))$
141	110 140	sylan2	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land F (c) (n) \leq 0) \land (v \subseteq I \land z \in v)) \to (F (z) (n) < F (c) (n) + \|F (c) (n)\| \to \neg 0 \leq F (z) (n))$
142	141	anassrs	$⊢ (((((φ \land c \in I) \land n \in (1 \dots N)) \land F (c) (n) \leq 0) \land v \subseteq I) \land z \in v) \to (F (z) (n) < F (c) (n) + \|F (c) (n)\| \to \neg 0 \leq F (z) (n))$
143	142	adantld	$⊢ (((((φ \land c \in I) \land n \in (1 \dots N)) \land F (c) (n) \leq 0) \land v \subseteq I) \land z \in v) \to ((F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|) \to \neg 0 \leq F (z) (n))$
144	143	ralimdva	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land F (c) (n) \leq 0) \land v \subseteq I) \to (\forall z \in v (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|) \to \forall z \in v \neg 0 \leq F (z) (n))$
145	144	an32s	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land v \subseteq I) \land F (c) (n) \leq 0) \to (\forall z \in v (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|) \to \forall z \in v \neg 0 \leq F (z) (n))$
146	145	impancom	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land v \subseteq I) \land \forall z \in v (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|)) \to (F (c) (n) \leq 0 \to \forall z \in v \neg 0 \leq F (z) (n))$
147		absid	$⊢ (F (c) (n) \in ℝ \land 0 \leq F (c) (n)) \to \|F (c) (n)\| = F (c) (n)$
148	147	oveq2d	$⊢ (F (c) (n) \in ℝ \land 0 \leq F (c) (n)) \to F (c) (n) - \|F (c) (n)\| = F (c) (n) - F (c) (n)$
149	27	subidd	$⊢ F (c) (n) \in ℝ \to F (c) (n) - F (c) (n) = 0$
150	149	adantr	$⊢ (F (c) (n) \in ℝ \land 0 \leq F (c) (n)) \to F (c) (n) - F (c) (n) = 0$
151	148 150	eqtrd	$⊢ (F (c) (n) \in ℝ \land 0 \leq F (c) (n)) \to F (c) (n) - \|F (c) (n)\| = 0$
152	26 151	sylan	$⊢ (((φ \land c \in I) \land n \in (1 \dots N)) \land 0 \leq F (c) (n)) \to F (c) (n) - \|F (c) (n)\| = 0$
153	152	adantr	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land 0 \leq F (c) (n)) \land z \in I) \to F (c) (n) - \|F (c) (n)\| = 0$
154	153	breq1d	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land 0 \leq F (c) (n)) \land z \in I) \to (F (c) (n) - \|F (c) (n)\| < F (z) (n) \leftrightarrow 0 < F (z) (n))$
155	135 134	ltnled	$⊢ ((φ \land n \in (1 \dots N)) \land z \in I) \to (0 < F (z) (n) \leftrightarrow \neg F (z) (n) \leq 0)$
156	155	adantllr	$⊢ (((φ \land c \in I) \land n \in (1 \dots N)) \land z \in I) \to (0 < F (z) (n) \leftrightarrow \neg F (z) (n) \leq 0)$
157	156	adantlr	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land 0 \leq F (c) (n)) \land z \in I) \to (0 < F (z) (n) \leftrightarrow \neg F (z) (n) \leq 0)$
158	154 157	bitrd	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land 0 \leq F (c) (n)) \land z \in I) \to (F (c) (n) - \|F (c) (n)\| < F (z) (n) \leftrightarrow \neg F (z) (n) \leq 0)$
159	158	biimpd	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land 0 \leq F (c) (n)) \land z \in I) \to (F (c) (n) - \|F (c) (n)\| < F (z) (n) \to \neg F (z) (n) \leq 0)$
160	110 159	sylan2	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land 0 \leq F (c) (n)) \land (v \subseteq I \land z \in v)) \to (F (c) (n) - \|F (c) (n)\| < F (z) (n) \to \neg F (z) (n) \leq 0)$
161	160	anassrs	$⊢ (((((φ \land c \in I) \land n \in (1 \dots N)) \land 0 \leq F (c) (n)) \land v \subseteq I) \land z \in v) \to (F (c) (n) - \|F (c) (n)\| < F (z) (n) \to \neg F (z) (n) \leq 0)$
162	161	adantrd	$⊢ (((((φ \land c \in I) \land n \in (1 \dots N)) \land 0 \leq F (c) (n)) \land v \subseteq I) \land z \in v) \to ((F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|) \to \neg F (z) (n) \leq 0)$
163	162	ralimdva	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land 0 \leq F (c) (n)) \land v \subseteq I) \to (\forall z \in v (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|) \to \forall z \in v \neg F (z) (n) \leq 0)$
164	163	an32s	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land v \subseteq I) \land 0 \leq F (c) (n)) \to (\forall z \in v (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|) \to \forall z \in v \neg F (z) (n) \leq 0)$
165	164	impancom	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land v \subseteq I) \land \forall z \in v (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|)) \to (0 \leq F (c) (n) \to \forall z \in v \neg F (z) (n) \leq 0)$
166	146 165	orim12d	$⊢ ((((φ \land c \in I) \land n \in (1 \dots N)) \land v \subseteq I) \land \forall z \in v (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|)) \to ((F (c) (n) \leq 0 \lor 0 \leq F (c) (n)) \to (\forall z \in v \neg 0 \leq F (z) (n) \lor \forall z \in v \neg F (z) (n) \leq 0))$
167	166	expimpd	$⊢ (((φ \land c \in I) \land n \in (1 \dots N)) \land v \subseteq I) \to ((\forall z \in v (F (c) (n) - \|F (c) (n)\| < F (z) (n) \land F (z) (n) < F (c) (n) + \|F (c) (n)\|) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n))) \to (\forall z \in v \neg 0 \leq F (z) (n) \lor \forall z \in v \neg F (z) (n) \leq 0))$
168	121 167	syland	$⊢ (((φ \land c \in I) \land n \in (1 \dots N)) \land v \subseteq I) \to (((x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n))) \to (\forall z \in v \neg 0 \leq F (z) (n) \lor \forall z \in v \neg F (z) (n) \leq 0))$
169	102 168	sylan2	$⊢ (((φ \land c \in I) \land n \in (1 \dots N)) \land v \in (R ↾_{𝑡} I)) \to (((x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n))) \to (\forall z \in v \neg 0 \leq F (z) (n) \lor \forall z \in v \neg F (z) (n) \leq 0))$
170	169	anim2d	$⊢ (((φ \land c \in I) \land n \in (1 \dots N)) \land v \in (R ↾_{𝑡} I)) \to ((c \in v \land ((x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n)))) \to (c \in v \land (\forall z \in v \neg 0 \leq F (z) (n) \lor \forall z \in v \neg F (z) (n) \leq 0)))$
171	170	reximdva	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to (\exists v \in (R ↾_{𝑡} I) (c \in v \land ((x \in I ⟼ F (x) (n)) [v] \subseteq (F (c) (n) - \|F (c) (n)\|, F (c) (n) + \|F (c) (n)\|) \land (F (c) (n) \leq 0 \lor 0 \leq F (c) (n)))) \to \exists v \in (R ↾_{𝑡} I) (c \in v \land (\forall z \in v \neg 0 \leq F (z) (n) \lor \forall z \in v \neg F (z) (n) \leq 0)))$
172	99 171	syld	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to (F (c) (n) \neq 0 \to \exists v \in (R ↾_{𝑡} I) (c \in v \land (\forall z \in v \neg 0 \leq F (z) (n) \lor \forall z \in v \neg F (z) (n) \leq 0)))$
173		ralnex	$⊢ \forall z \in v \neg 0 r F (z) (n) \leftrightarrow \neg \exists z \in v 0 r F (z) (n)$
174	173	rexbii	$⊢ \exists r \in \{\leq \leq^{-1}\} \forall z \in v \neg 0 r F (z) (n) \leftrightarrow \exists r \in \{\leq \leq^{-1}\} \neg \exists z \in v 0 r F (z) (n)$
175		letsr	$⊢ \leq \in TosetRel$
176	175	elexi	$⊢ \leq \in V$
177	176	cnvex	$⊢ \leq^{-1} \in V$
178		breq	$⊢ r = \leq \to (0 r F (z) (n) \leftrightarrow 0 \leq F (z) (n))$
179	178	notbid	$⊢ r = \leq \to (\neg 0 r F (z) (n) \leftrightarrow \neg 0 \leq F (z) (n))$
180	179	ralbidv	$⊢ r = \leq \to (\forall z \in v \neg 0 r F (z) (n) \leftrightarrow \forall z \in v \neg 0 \leq F (z) (n))$
181		breq	$⊢ r = \leq^{-1} \to (0 r F (z) (n) \leftrightarrow 0 \leq^{-1} F (z) (n))$
182		c0ex	$⊢ 0 \in V$
183	182 113	brcnv	$⊢ 0 \leq^{-1} F (z) (n) \leftrightarrow F (z) (n) \leq 0$
184	181 183	bitrdi	$⊢ r = \leq^{-1} \to (0 r F (z) (n) \leftrightarrow F (z) (n) \leq 0)$
185	184	notbid	$⊢ r = \leq^{-1} \to (\neg 0 r F (z) (n) \leftrightarrow \neg F (z) (n) \leq 0)$
186	185	ralbidv	$⊢ r = \leq^{-1} \to (\forall z \in v \neg 0 r F (z) (n) \leftrightarrow \forall z \in v \neg F (z) (n) \leq 0)$
187	176 177 180 186	rexpr	$⊢ \exists r \in \{\leq \leq^{-1}\} \forall z \in v \neg 0 r F (z) (n) \leftrightarrow (\forall z \in v \neg 0 \leq F (z) (n) \lor \forall z \in v \neg F (z) (n) \leq 0)$
188		rexnal	$⊢ \exists r \in \{\leq \leq^{-1}\} \neg \exists z \in v 0 r F (z) (n) \leftrightarrow \neg \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)$
189	174 187 188	3bitr3i	$⊢ (\forall z \in v \neg 0 \leq F (z) (n) \lor \forall z \in v \neg F (z) (n) \leq 0) \leftrightarrow \neg \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)$
190	189	anbi2i	$⊢ (c \in v \land (\forall z \in v \neg 0 \leq F (z) (n) \lor \forall z \in v \neg F (z) (n) \leq 0)) \leftrightarrow (c \in v \land \neg \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
191		annim	$⊢ (c \in v \land \neg \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)) \leftrightarrow \neg (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
192	190 191	bitri	$⊢ (c \in v \land (\forall z \in v \neg 0 \leq F (z) (n) \lor \forall z \in v \neg F (z) (n) \leq 0)) \leftrightarrow \neg (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
193	192	rexbii	$⊢ \exists v \in (R ↾_{𝑡} I) (c \in v \land (\forall z \in v \neg 0 \leq F (z) (n) \lor \forall z \in v \neg F (z) (n) \leq 0)) \leftrightarrow \exists v \in (R ↾_{𝑡} I) \neg (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
194		rexnal	$⊢ \exists v \in (R ↾_{𝑡} I) \neg (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)) \leftrightarrow \neg \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
195	193 194	bitri	$⊢ \exists v \in (R ↾_{𝑡} I) (c \in v \land (\forall z \in v \neg 0 \leq F (z) (n) \lor \forall z \in v \neg F (z) (n) \leq 0)) \leftrightarrow \neg \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
196	172 195	imbitrdi	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to (F (c) (n) \neq 0 \to \neg \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)))$
197	196	necon4ad	$⊢ ((φ \land c \in I) \land n \in (1 \dots N)) \to (\forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)) \to F (c) (n) = 0)$
198	197	ralimdva	$⊢ (φ \land c \in I) \to (\forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)) \to \forall n \in (1 \dots N) F (c) (n) = 0)$
199	25	ffnd	$⊢ (φ \land c \in I) \to F (c) Fn (1 \dots N)$
200	198 199	jctild	$⊢ (φ \land c \in I) \to (\forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)) \to (F (c) Fn (1 \dots N) \land \forall n \in (1 \dots N) F (c) (n) = 0))$
201		fconstfv	$⊢ F (c) : (1 \dots N) ⟶ \{0\} \leftrightarrow (F (c) Fn (1 \dots N) \land \forall n \in (1 \dots N) F (c) (n) = 0)$
202	182	fconst2	$⊢ F (c) : (1 \dots N) ⟶ \{0\} \leftrightarrow F (c) = (1 \dots N) \times \{0\}$
203	201 202	bitr3i	$⊢ (F (c) Fn (1 \dots N) \land \forall n \in (1 \dots N) F (c) (n) = 0) \leftrightarrow F (c) = (1 \dots N) \times \{0\}$
204	200 203	imbitrdi	$⊢ (φ \land c \in I) \to (\forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)) \to F (c) = (1 \dots N) \times \{0\})$
205	204	reximdva	$⊢ φ \to (\exists c \in I \forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)) \to \exists c \in I F (c) = (1 \dots N) \times \{0\})$
206	7 205	mpd	$⊢ φ \to \exists c \in I F (c) = (1 \dots N) \times \{0\}$

Metamath Proof Explorer

Theorem poimir

Proof