Theorem i1fposd

Description: Deduction form of i1fposd . (Contributed by Mario Carneiro, 6-Aug-2014)

	Ref	Expression
Hypothesis	i1fposd.1	$$⊢\phi \to \left(x\in ℝ⟼A\right)\in \mathrm{dom}{\int }^1$$
Assertion	i1fposd	$$⊢\phi \to \left(x\in ℝ⟼if\left(0\le A,A,0\right)\right)\in \mathrm{dom}{\int }^1$$

Proof

Step	Hyp	Ref	Expression
1		i1fposd.1	$$⊢\phi \to \left(x\in ℝ⟼A\right)\in \mathrm{dom}{\int }^1$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}x0$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}x\le$$
4		nffvmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in ℝ⟼A\right)\left(y\right)$$
5	2 3 4	nfbr	$$⊢Ⅎx0\le \left(x\in ℝ⟼A\right)\left(y\right)$$
6	5 4 2	nfif	$$⊢\underset{\_}{Ⅎ}xif\left(0\le \left(x\in ℝ⟼A\right)\left(y\right),\left(x\in ℝ⟼A\right)\left(y\right),0\right)$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}yif\left(0\le \left(x\in ℝ⟼A\right)\left(x\right),\left(x\in ℝ⟼A\right)\left(x\right),0\right)$$
8		fveq2	$$⊢y=x\to \left(x\in ℝ⟼A\right)\left(y\right)=\left(x\in ℝ⟼A\right)\left(x\right)$$
9	8	breq2d	$$⊢y=x\to \left(0\le \left(x\in ℝ⟼A\right)\left(y\right)\leftrightarrow 0\le \left(x\in ℝ⟼A\right)\left(x\right)\right)$$
10	9 8	ifbieq1d	$$⊢y=x\to if\left(0\le \left(x\in ℝ⟼A\right)\left(y\right),\left(x\in ℝ⟼A\right)\left(y\right),0\right)=if\left(0\le \left(x\in ℝ⟼A\right)\left(x\right),\left(x\in ℝ⟼A\right)\left(x\right),0\right)$$
11	6 7 10	cbvmpt	$$⊢\left(y\in ℝ⟼if\left(0\le \left(x\in ℝ⟼A\right)\left(y\right),\left(x\in ℝ⟼A\right)\left(y\right),0\right)\right)=\left(x\in ℝ⟼if\left(0\le \left(x\in ℝ⟼A\right)\left(x\right),\left(x\in ℝ⟼A\right)\left(x\right),0\right)\right)$$
12		simpr	$$⊢\left(\phi \wedge x\in ℝ\right)\to x\in ℝ$$
13		i1ff	$$⊢\left(x\in ℝ⟼A\right)\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼A\right):ℝ⟶ℝ$$
14	1 13	syl	$$⊢\phi \to \left(x\in ℝ⟼A\right):ℝ⟶ℝ$$
15	14	fvmptelcdm	$$⊢\left(\phi \wedge x\in ℝ\right)\to A\in ℝ$$
16		eqid	$$⊢\left(x\in ℝ⟼A\right)=\left(x\in ℝ⟼A\right)$$
17	16	fvmpt2	$$⊢\left(x\in ℝ\wedge A\in ℝ\right)\to \left(x\in ℝ⟼A\right)\left(x\right)=A$$
18	12 15 17	syl2anc	$$⊢\left(\phi \wedge x\in ℝ\right)\to \left(x\in ℝ⟼A\right)\left(x\right)=A$$
19	18	breq2d	$$⊢\left(\phi \wedge x\in ℝ\right)\to \left(0\le \left(x\in ℝ⟼A\right)\left(x\right)\leftrightarrow 0\le A\right)$$
20	19 18	ifbieq1d	$$⊢\left(\phi \wedge x\in ℝ\right)\to if\left(0\le \left(x\in ℝ⟼A\right)\left(x\right),\left(x\in ℝ⟼A\right)\left(x\right),0\right)=if\left(0\le A,A,0\right)$$
21	20	mpteq2dva	$$⊢\phi \to \left(x\in ℝ⟼if\left(0\le \left(x\in ℝ⟼A\right)\left(x\right),\left(x\in ℝ⟼A\right)\left(x\right),0\right)\right)=\left(x\in ℝ⟼if\left(0\le A,A,0\right)\right)$$
22	11 21	eqtrid	$$⊢\phi \to \left(y\in ℝ⟼if\left(0\le \left(x\in ℝ⟼A\right)\left(y\right),\left(x\in ℝ⟼A\right)\left(y\right),0\right)\right)=\left(x\in ℝ⟼if\left(0\le A,A,0\right)\right)$$
23		eqid	$$⊢\left(y\in ℝ⟼if\left(0\le \left(x\in ℝ⟼A\right)\left(y\right),\left(x\in ℝ⟼A\right)\left(y\right),0\right)\right)=\left(y\in ℝ⟼if\left(0\le \left(x\in ℝ⟼A\right)\left(y\right),\left(x\in ℝ⟼A\right)\left(y\right),0\right)\right)$$
24	23	i1fpos	$$⊢\left(x\in ℝ⟼A\right)\in \mathrm{dom}{\int }^1\to \left(y\in ℝ⟼if\left(0\le \left(x\in ℝ⟼A\right)\left(y\right),\left(x\in ℝ⟼A\right)\left(y\right),0\right)\right)\in \mathrm{dom}{\int }^1$$
25	1 24	syl	$$⊢\phi \to \left(y\in ℝ⟼if\left(0\le \left(x\in ℝ⟼A\right)\left(y\right),\left(x\in ℝ⟼A\right)\left(y\right),0\right)\right)\in \mathrm{dom}{\int }^1$$
26	22 25	eqeltrrd	$$⊢\phi \to \left(x\in ℝ⟼if\left(0\le A,A,0\right)\right)\in \mathrm{dom}{\int }^1$$