stoweidlem44

Description: This lemma is used to prove the existence of a function p as in Lemma 1 of BrosowskiDeutsh p. 90: p is in the subalgebra, such that 0 <= p <= 1, p__(t_0) = 0, and p > 0 on T - U. Z is used to represent t_0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem44.1	$⊢ Ⅎ j φ$
	stoweidlem44.2	$⊢ Ⅎ t φ$
	stoweidlem44.3	$⊢ K = topGen (ran (.))$
	stoweidlem44.4	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
	stoweidlem44.5	$⊢ P = (t \in T ⟼ (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (t))$
	stoweidlem44.6	$⊢ φ \to M \in ℕ$
	stoweidlem44.7	$⊢ φ \to G : (1 \dots M) ⟶ Q$
	stoweidlem44.8	$⊢ φ \to \forall t \in (T ∖ U) \exists j \in (1 \dots M) 0 < G (j) (t)$
	stoweidlem44.9	$⊢ T = ⋃ J$
	stoweidlem44.10	$⊢ φ \to A \subseteq J Cn K$
	stoweidlem44.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem44.12	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem44.13	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem44.14	$⊢ φ \to Z \in T$
Assertion	stoweidlem44	$⊢ φ \to \exists p \in A (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem44.1	$⊢ Ⅎ j φ$
2		stoweidlem44.2	$⊢ Ⅎ t φ$
3		stoweidlem44.3	$⊢ K = topGen (ran (.))$
4		stoweidlem44.4	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
5		stoweidlem44.5	$⊢ P = (t \in T ⟼ (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (t))$
6		stoweidlem44.6	$⊢ φ \to M \in ℕ$
7		stoweidlem44.7	$⊢ φ \to G : (1 \dots M) ⟶ Q$
8		stoweidlem44.8	$⊢ φ \to \forall t \in (T ∖ U) \exists j \in (1 \dots M) 0 < G (j) (t)$
9		stoweidlem44.9	$⊢ T = ⋃ J$
10		stoweidlem44.10	$⊢ φ \to A \subseteq J Cn K$
11		stoweidlem44.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
12		stoweidlem44.12	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
13		stoweidlem44.13	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
14		stoweidlem44.14	$⊢ φ \to Z \in T$
15		eqid	$⊢ (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t)) = (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t))$
16		eqid	$⊢ (t \in T ⟼ \frac{1}{M}) = (t \in T ⟼ \frac{1}{M})$
17	6	nnrecred	$⊢ φ \to \frac{1}{M} \in ℝ$
18		ssrab2	$⊢ \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\} \subseteq A$
19	4 18	eqsstri	$⊢ Q \subseteq A$
20		fss	$⊢ (G : (1 \dots M) ⟶ Q \land Q \subseteq A) \to G : (1 \dots M) ⟶ A$
21	7 19 20	sylancl	$⊢ φ \to G : (1 \dots M) ⟶ A$
22		eqid	$⊢ J Cn K = J Cn K$
23	10	sselda	$⊢ (φ \land f \in A) \to f \in (J Cn K)$
24	3 9 22 23	fcnre	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
25	2 5 15 16 6 17 21 11 12 13 24	stoweidlem32	$⊢ φ \to P \in A$
26	4 5 6 7 24	stoweidlem38	$⊢ (φ \land t \in T) \to (0 \leq P (t) \land P (t) \leq 1)$
27	26	ex	$⊢ φ \to (t \in T \to (0 \leq P (t) \land P (t) \leq 1))$
28	2 27	ralrimi	$⊢ φ \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
29	4 5 6 7 24 14	stoweidlem37	$⊢ φ \to P (Z) = 0$
30		nfv	$⊢ Ⅎ j t \in (T ∖ U)$
31	1 30	nfan	$⊢ Ⅎ j (φ \land t \in (T ∖ U))$
32		nfv	$⊢ Ⅎ j 0 < (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (t)$
33	8	r19.21bi	$⊢ (φ \land t \in (T ∖ U)) \to \exists j \in (1 \dots M) 0 < G (j) (t)$
34		df-rex	$⊢ \exists j \in (1 \dots M) 0 < G (j) (t) \leftrightarrow \exists j (j \in (1 \dots M) \land 0 < G (j) (t))$
35	33 34	sylib	$⊢ (φ \land t \in (T ∖ U)) \to \exists j (j \in (1 \dots M) \land 0 < G (j) (t))$
36	17	ad2antrr	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to \frac{1}{M} \in ℝ$
37		simpll	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to φ$
38		eldifi	$⊢ t \in (T ∖ U) \to t \in T$
39	38	ad2antlr	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to t \in T$
40		fzfid	$⊢ (φ \land t \in T) \to (1 \dots M) \in Fin$
41	4 7 24	stoweidlem15	$⊢ ((φ \land i \in (1 \dots M)) \land t \in T) \to (G (i) (t) \in ℝ \land 0 \leq G (i) (t) \land G (i) (t) \leq 1)$
42	41	an32s	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to (G (i) (t) \in ℝ \land 0 \leq G (i) (t) \land G (i) (t) \leq 1)$
43	42	simp1d	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to G (i) (t) \in ℝ$
44	40 43	fsumrecl	$⊢ (φ \land t \in T) \to \sum_{i = 1}^{M} G (i) (t) \in ℝ$
45	37 39 44	syl2anc	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to \sum_{i = 1}^{M} G (i) (t) \in ℝ$
46	6	nnred	$⊢ φ \to M \in ℝ$
47	6	nngt0d	$⊢ φ \to 0 < M$
48	46 47	recgt0d	$⊢ φ \to 0 < \frac{1}{M}$
49	48	ad2antrr	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to 0 < \frac{1}{M}$
50		0red	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to 0 \in ℝ$
51		simprl	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to j \in (1 \dots M)$
52	37 51 39	3jca	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to (φ \land j \in (1 \dots M) \land t \in T)$
53		snfi	$⊢ \{j\} \in Fin$
54	53	a1i	$⊢ (φ \land j \in (1 \dots M) \land t \in T) \to \{j\} \in Fin$
55		simpl1	$⊢ ((φ \land j \in (1 \dots M) \land t \in T) \land i \in \{j\}) \to φ$
56		simpl3	$⊢ ((φ \land j \in (1 \dots M) \land t \in T) \land i \in \{j\}) \to t \in T$
57		elsni	$⊢ i \in \{j\} \to i = j$
58	57	adantl	$⊢ ((φ \land j \in (1 \dots M) \land t \in T) \land i \in \{j\}) \to i = j$
59		simpl2	$⊢ ((φ \land j \in (1 \dots M) \land t \in T) \land i \in \{j\}) \to j \in (1 \dots M)$
60	58 59	eqeltrd	$⊢ ((φ \land j \in (1 \dots M) \land t \in T) \land i \in \{j\}) \to i \in (1 \dots M)$
61	55 56 60 43	syl21anc	$⊢ ((φ \land j \in (1 \dots M) \land t \in T) \land i \in \{j\}) \to G (i) (t) \in ℝ$
62	54 61	fsumrecl	$⊢ (φ \land j \in (1 \dots M) \land t \in T) \to \sum_{i \in \{j\}} G (i) (t) \in ℝ$
63	52 62	syl	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to \sum_{i \in \{j\}} G (i) (t) \in ℝ$
64	50 63	readdcld	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to 0 + \sum_{i \in \{j\}} G (i) (t) \in ℝ$
65		fzfi	$⊢ (1 \dots M) \in Fin$
66		diffi	$⊢ (1 \dots M) \in Fin \to (1 \dots M) ∖ \{j\} \in Fin$
67	65 66	mp1i	$⊢ (φ \land t \in T) \to (1 \dots M) ∖ \{j\} \in Fin$
68		eldifi	$⊢ i \in ((1 \dots M) ∖ \{j\}) \to i \in (1 \dots M)$
69	68 43	sylan2	$⊢ ((φ \land t \in T) \land i \in ((1 \dots M) ∖ \{j\})) \to G (i) (t) \in ℝ$
70	67 69	fsumrecl	$⊢ (φ \land t \in T) \to \sum_{i \in (1 \dots M) ∖ \{j\}} G (i) (t) \in ℝ$
71	37 39 70	syl2anc	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to \sum_{i \in (1 \dots M) ∖ \{j\}} G (i) (t) \in ℝ$
72	71 63	readdcld	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to \sum_{i \in (1 \dots M) ∖ \{j\}} G (i) (t) + \sum_{i \in \{j\}} G (i) (t) \in ℝ$
73		00id	$⊢ 0 + 0 = 0$
74		simprr	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to 0 < G (j) (t)$
75	4 7 24	stoweidlem15	$⊢ ((φ \land j \in (1 \dots M)) \land t \in T) \to (G (j) (t) \in ℝ \land 0 \leq G (j) (t) \land G (j) (t) \leq 1)$
76	75	simp1d	$⊢ ((φ \land j \in (1 \dots M)) \land t \in T) \to G (j) (t) \in ℝ$
77	37 51 39 76	syl21anc	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to G (j) (t) \in ℝ$
78	77	recnd	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to G (j) (t) \in ℂ$
79		fveq2	$⊢ i = j \to G (i) = G (j)$
80	79	fveq1d	$⊢ i = j \to G (i) (t) = G (j) (t)$
81	80	sumsn	$⊢ (j \in (1 \dots M) \land G (j) (t) \in ℂ) \to \sum_{i \in \{j\}} G (i) (t) = G (j) (t)$
82	51 78 81	syl2anc	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to \sum_{i \in \{j\}} G (i) (t) = G (j) (t)$
83	74 82	breqtrrd	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to 0 < \sum_{i \in \{j\}} G (i) (t)$
84	50 63 50 83	ltadd2dd	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to 0 + 0 < 0 + \sum_{i \in \{j\}} G (i) (t)$
85	73 84	eqbrtrrid	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to 0 < 0 + \sum_{i \in \{j\}} G (i) (t)$
86		0red	$⊢ (φ \land j \in (1 \dots M) \land t \in T) \to 0 \in ℝ$
87	70	3adant2	$⊢ (φ \land j \in (1 \dots M) \land t \in T) \to \sum_{i \in (1 \dots M) ∖ \{j\}} G (i) (t) \in ℝ$
88		simpll	$⊢ ((φ \land t \in T) \land i \in ((1 \dots M) ∖ \{j\})) \to φ$
89	68	adantl	$⊢ ((φ \land t \in T) \land i \in ((1 \dots M) ∖ \{j\})) \to i \in (1 \dots M)$
90		simplr	$⊢ ((φ \land t \in T) \land i \in ((1 \dots M) ∖ \{j\})) \to t \in T$
91	88 89 90 41	syl21anc	$⊢ ((φ \land t \in T) \land i \in ((1 \dots M) ∖ \{j\})) \to (G (i) (t) \in ℝ \land 0 \leq G (i) (t) \land G (i) (t) \leq 1)$
92	91	simp2d	$⊢ ((φ \land t \in T) \land i \in ((1 \dots M) ∖ \{j\})) \to 0 \leq G (i) (t)$
93	67 69 92	fsumge0	$⊢ (φ \land t \in T) \to 0 \leq \sum_{i \in (1 \dots M) ∖ \{j\}} G (i) (t)$
94	93	3adant2	$⊢ (φ \land j \in (1 \dots M) \land t \in T) \to 0 \leq \sum_{i \in (1 \dots M) ∖ \{j\}} G (i) (t)$
95	86 87 62 94	leadd1dd	$⊢ (φ \land j \in (1 \dots M) \land t \in T) \to 0 + \sum_{i \in \{j\}} G (i) (t) \leq \sum_{i \in (1 \dots M) ∖ \{j\}} G (i) (t) + \sum_{i \in \{j\}} G (i) (t)$
96	52 95	syl	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to 0 + \sum_{i \in \{j\}} G (i) (t) \leq \sum_{i \in (1 \dots M) ∖ \{j\}} G (i) (t) + \sum_{i \in \{j\}} G (i) (t)$
97	50 64 72 85 96	ltletrd	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to 0 < \sum_{i \in (1 \dots M) ∖ \{j\}} G (i) (t) + \sum_{i \in \{j\}} G (i) (t)$
98		eldifn	$⊢ x \in ((1 \dots M) ∖ \{j\}) \to \neg x \in \{j\}$
99		imnan	$⊢ (x \in ((1 \dots M) ∖ \{j\}) \to \neg x \in \{j\}) \leftrightarrow \neg (x \in ((1 \dots M) ∖ \{j\}) \land x \in \{j\})$
100	98 99	mpbi	$⊢ \neg (x \in ((1 \dots M) ∖ \{j\}) \land x \in \{j\})$
101		elin	$⊢ x \in (((1 \dots M) ∖ \{j\}) \cap \{j\}) \leftrightarrow (x \in ((1 \dots M) ∖ \{j\}) \land x \in \{j\})$
102	100 101	mtbir	$⊢ \neg x \in (((1 \dots M) ∖ \{j\}) \cap \{j\})$
103	102	nel0	$⊢ ((1 \dots M) ∖ \{j\}) \cap \{j\} = \emptyset$
104	103	a1i	$⊢ (φ \land j \in (1 \dots M) \land t \in T) \to ((1 \dots M) ∖ \{j\}) \cap \{j\} = \emptyset$
105		undif1	$⊢ ((1 \dots M) ∖ \{j\}) \cup \{j\} = (1 \dots M) \cup \{j\}$
106		snssi	$⊢ j \in (1 \dots M) \to \{j\} \subseteq (1 \dots M)$
107	106	3ad2ant2	$⊢ (φ \land j \in (1 \dots M) \land t \in T) \to \{j\} \subseteq (1 \dots M)$
108		ssequn2	$⊢ \{j\} \subseteq (1 \dots M) \leftrightarrow (1 \dots M) \cup \{j\} = (1 \dots M)$
109	107 108	sylib	$⊢ (φ \land j \in (1 \dots M) \land t \in T) \to (1 \dots M) \cup \{j\} = (1 \dots M)$
110	105 109	eqtr2id	$⊢ (φ \land j \in (1 \dots M) \land t \in T) \to (1 \dots M) = ((1 \dots M) ∖ \{j\}) \cup \{j\}$
111		fzfid	$⊢ (φ \land j \in (1 \dots M) \land t \in T) \to (1 \dots M) \in Fin$
112	43	3adantl2	$⊢ ((φ \land j \in (1 \dots M) \land t \in T) \land i \in (1 \dots M)) \to G (i) (t) \in ℝ$
113	112	recnd	$⊢ ((φ \land j \in (1 \dots M) \land t \in T) \land i \in (1 \dots M)) \to G (i) (t) \in ℂ$
114	104 110 111 113	fsumsplit	$⊢ (φ \land j \in (1 \dots M) \land t \in T) \to \sum_{i = 1}^{M} G (i) (t) = \sum_{i \in (1 \dots M) ∖ \{j\}} G (i) (t) + \sum_{i \in \{j\}} G (i) (t)$
115	52 114	syl	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to \sum_{i = 1}^{M} G (i) (t) = \sum_{i \in (1 \dots M) ∖ \{j\}} G (i) (t) + \sum_{i \in \{j\}} G (i) (t)$
116	97 115	breqtrrd	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to 0 < \sum_{i = 1}^{M} G (i) (t)$
117	36 45 49 116	mulgt0d	$⊢ ((φ \land t \in (T ∖ U)) \land (j \in (1 \dots M) \land 0 < G (j) (t))) \to 0 < (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (t)$
118	31 32 35 117	exlimdd	$⊢ (φ \land t \in (T ∖ U)) \to 0 < (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (t)$
119	4 5 6 7 24	stoweidlem30	$⊢ (φ \land t \in T) \to P (t) = (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (t)$
120	38 119	sylan2	$⊢ (φ \land t \in (T ∖ U)) \to P (t) = (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (t)$
121	118 120	breqtrrd	$⊢ (φ \land t \in (T ∖ U)) \to 0 < P (t)$
122	121	ex	$⊢ φ \to (t \in (T ∖ U) \to 0 < P (t))$
123	2 122	ralrimi	$⊢ φ \to \forall t \in (T ∖ U) 0 < P (t)$
124	28 29 123	3jca	$⊢ φ \to (\forall t \in T (0 \leq P (t) \land P (t) \leq 1) \land P (Z) = 0 \land \forall t \in (T ∖ U) 0 < P (t))$
125		eleq1	$⊢ p = P \to (p \in A \leftrightarrow P \in A)$
126		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ (\frac{1}{M}) \sum_{i = 1}^{M} G (i) (t))$
127	5 126	nfcxfr	$⊢ \underline{Ⅎ} t P$
128	127	nfeq2	$⊢ Ⅎ t p = P$
129		fveq1	$⊢ p = P \to p (t) = P (t)$
130	129	breq2d	$⊢ p = P \to (0 \leq p (t) \leftrightarrow 0 \leq P (t))$
131	129	breq1d	$⊢ p = P \to (p (t) \leq 1 \leftrightarrow P (t) \leq 1)$
132	130 131	anbi12d	$⊢ p = P \to ((0 \leq p (t) \land p (t) \leq 1) \leftrightarrow (0 \leq P (t) \land P (t) \leq 1))$
133	128 132	ralbid	$⊢ p = P \to (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq P (t) \land P (t) \leq 1))$
134		fveq1	$⊢ p = P \to p (Z) = P (Z)$
135	134	eqeq1d	$⊢ p = P \to (p (Z) = 0 \leftrightarrow P (Z) = 0)$
136	129	breq2d	$⊢ p = P \to (0 < p (t) \leftrightarrow 0 < P (t))$
137	128 136	ralbid	$⊢ p = P \to (\forall t \in (T ∖ U) 0 < p (t) \leftrightarrow \forall t \in (T ∖ U) 0 < P (t))$
138	133 135 137	3anbi123d	$⊢ p = P \to ((\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)) \leftrightarrow (\forall t \in T (0 \leq P (t) \land P (t) \leq 1) \land P (Z) = 0 \land \forall t \in (T ∖ U) 0 < P (t)))$
139	125 138	anbi12d	$⊢ p = P \to ((p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t))) \leftrightarrow (P \in A \land (\forall t \in T (0 \leq P (t) \land P (t) \leq 1) \land P (Z) = 0 \land \forall t \in (T ∖ U) 0 < P (t))))$
140	139	spcegv	$⊢ P \in A \to ((P \in A \land (\forall t \in T (0 \leq P (t) \land P (t) \leq 1) \land P (Z) = 0 \land \forall t \in (T ∖ U) 0 < P (t))) \to \exists p (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t))))$
141	25 140	syl	$⊢ φ \to ((P \in A \land (\forall t \in T (0 \leq P (t) \land P (t) \leq 1) \land P (Z) = 0 \land \forall t \in (T ∖ U) 0 < P (t))) \to \exists p (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t))))$
142	25 124 141	mp2and	$⊢ φ \to \exists p (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))$
143		df-rex	$⊢ \exists p \in A (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)) \leftrightarrow \exists p (p \in A \land (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t)))$
144	142 143	sylibr	$⊢ φ \to \exists p \in A (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t))$

Metamath Proof Explorer

Theorem stoweidlem44

Proof