Theorem supmullem2

Description: Lemma for supmul . (Contributed by Mario Carneiro, 5-Jul-2013)

	Ref	Expression
Hypotheses	supmul.1	$$⊢C=\left\{z|\exists v\in A\exists b\in Bz=vb\right\}$$
	supmul.2	$$⊢\phi \leftrightarrow \left(\left(\forall x\in A0\le x\wedge \forall x\in B0\le x\right)\wedge \left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists x\in ℝ\forall y\in Ay\le x\right)\wedge \left(B\subseteq ℝ\wedge B\ne \varnothing \wedge \exists x\in ℝ\forall y\in By\le x\right)\right)$$
Assertion	supmullem2	$$⊢\phi \to \left(C\subseteq ℝ\wedge C\ne \varnothing \wedge \exists x\in ℝ\forall w\in Cw\le x\right)$$

Proof

Step	Hyp	Ref	Expression
1		supmul.1	$$⊢C=\left\{z|\exists v\in A\exists b\in Bz=vb\right\}$$
2		supmul.2	$$⊢\phi \leftrightarrow \left(\left(\forall x\in A0\le x\wedge \forall x\in B0\le x\right)\wedge \left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists x\in ℝ\forall y\in Ay\le x\right)\wedge \left(B\subseteq ℝ\wedge B\ne \varnothing \wedge \exists x\in ℝ\forall y\in By\le x\right)\right)$$
3		vex	$$⊢w\in \mathrm{V}$$
4		oveq1	$$⊢v=a\to vb=ab$$
5	4	eqeq2d	$$⊢v=a\to \left(z=vb\leftrightarrow z=ab\right)$$
6	5	rexbidv	$$⊢v=a\to \left(\exists b\in Bz=vb\leftrightarrow \exists b\in Bz=ab\right)$$
7	6	cbvrexvw	$$⊢\exists v\in A\exists b\in Bz=vb\leftrightarrow \exists a\in A\exists b\in Bz=ab$$
8		eqeq1	$$⊢z=w\to \left(z=ab\leftrightarrow w=ab\right)$$
9	8	2rexbidv	$$⊢z=w\to \left(\exists a\in A\exists b\in Bz=ab\leftrightarrow \exists a\in A\exists b\in Bw=ab\right)$$
10	7 9	bitrid	$$⊢z=w\to \left(\exists v\in A\exists b\in Bz=vb\leftrightarrow \exists a\in A\exists b\in Bw=ab\right)$$
11	3 10 1	elab2	$$⊢w\in C\leftrightarrow \exists a\in A\exists b\in Bw=ab$$
12	2	simp2bi	$$⊢\phi \to \left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists x\in ℝ\forall y\in Ay\le x\right)$$
13	12	simp1d	$$⊢\phi \to A\subseteq ℝ$$
14	13	sseld	$$⊢\phi \to \left(a\in A\to a\in ℝ\right)$$
15	2	simp3bi	$$⊢\phi \to \left(B\subseteq ℝ\wedge B\ne \varnothing \wedge \exists x\in ℝ\forall y\in By\le x\right)$$
16	15	simp1d	$$⊢\phi \to B\subseteq ℝ$$
17	16	sseld	$$⊢\phi \to \left(b\in B\to b\in ℝ\right)$$
18	14 17	anim12d	$$⊢\phi \to \left(\left(a\in A\wedge b\in B\right)\to \left(a\in ℝ\wedge b\in ℝ\right)\right)$$
19		remulcl	$$⊢\left(a\in ℝ\wedge b\in ℝ\right)\to ab\in ℝ$$
20	18 19	syl6	$$⊢\phi \to \left(\left(a\in A\wedge b\in B\right)\to ab\in ℝ\right)$$
21		eleq1a	$$⊢ab\in ℝ\to \left(w=ab\to w\in ℝ\right)$$
22	20 21	syl6	$$⊢\phi \to \left(\left(a\in A\wedge b\in B\right)\to \left(w=ab\to w\in ℝ\right)\right)$$
23	22	rexlimdvv	$$⊢\phi \to \left(\exists a\in A\exists b\in Bw=ab\to w\in ℝ\right)$$
24	11 23	biimtrid	$$⊢\phi \to \left(w\in C\to w\in ℝ\right)$$
25	24	ssrdv	$$⊢\phi \to C\subseteq ℝ$$
26	12	simp2d	$$⊢\phi \to A\ne \varnothing$$
27	15	simp2d	$$⊢\phi \to B\ne \varnothing$$
28		ovex	$$⊢ab\in \mathrm{V}$$
29	28	isseti	$$⊢\exists ww=ab$$
30	29	rgenw	$$⊢\forall b\in B\exists ww=ab$$
31		r19.2z	$$⊢\left(B\ne \varnothing \wedge \forall b\in B\exists ww=ab\right)\to \exists b\in B\exists ww=ab$$
32	27 30 31	sylancl	$$⊢\phi \to \exists b\in B\exists ww=ab$$
33		rexcom4	$$⊢\exists b\in B\exists ww=ab\leftrightarrow \exists w\exists b\in Bw=ab$$
34	32 33	sylib	$$⊢\phi \to \exists w\exists b\in Bw=ab$$
35	34	ralrimivw	$$⊢\phi \to \forall a\in A\exists w\exists b\in Bw=ab$$
36		r19.2z	$$⊢\left(A\ne \varnothing \wedge \forall a\in A\exists w\exists b\in Bw=ab\right)\to \exists a\in A\exists w\exists b\in Bw=ab$$
37	26 35 36	syl2anc	$$⊢\phi \to \exists a\in A\exists w\exists b\in Bw=ab$$
38		rexcom4	$$⊢\exists a\in A\exists w\exists b\in Bw=ab\leftrightarrow \exists w\exists a\in A\exists b\in Bw=ab$$
39	37 38	sylib	$$⊢\phi \to \exists w\exists a\in A\exists b\in Bw=ab$$
40		n0	$$⊢C\ne \varnothing \leftrightarrow \exists ww\in C$$
41	11	exbii	$$⊢\exists ww\in C\leftrightarrow \exists w\exists a\in A\exists b\in Bw=ab$$
42	40 41	bitri	$$⊢C\ne \varnothing \leftrightarrow \exists w\exists a\in A\exists b\in Bw=ab$$
43	39 42	sylibr	$$⊢\phi \to C\ne \varnothing$$
44		suprcl	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists x\in ℝ\forall y\in Ay\le x\right)\to sup\left(A,ℝ,<\right)\in ℝ$$
45	12 44	syl	$$⊢\phi \to sup\left(A,ℝ,<\right)\in ℝ$$
46		suprcl	$$⊢\left(B\subseteq ℝ\wedge B\ne \varnothing \wedge \exists x\in ℝ\forall y\in By\le x\right)\to sup\left(B,ℝ,<\right)\in ℝ$$
47	15 46	syl	$$⊢\phi \to sup\left(B,ℝ,<\right)\in ℝ$$
48	45 47	remulcld	$$⊢\phi \to sup\left(A,ℝ,<\right)sup\left(B,ℝ,<\right)\in ℝ$$
49	1 2	supmullem1	$$⊢\phi \to \forall w\in Cw\le sup\left(A,ℝ,<\right)sup\left(B,ℝ,<\right)$$
50		brralrspcev	$$⊢\left(sup\left(A,ℝ,<\right)sup\left(B,ℝ,<\right)\in ℝ\wedge \forall w\in Cw\le sup\left(A,ℝ,<\right)sup\left(B,ℝ,<\right)\right)\to \exists x\in ℝ\forall w\in Cw\le x$$
51	48 49 50	syl2anc	$$⊢\phi \to \exists x\in ℝ\forall w\in Cw\le x$$
52	25 43 51	3jca	$$⊢\phi \to \left(C\subseteq ℝ\wedge C\ne \varnothing \wedge \exists x\in ℝ\forall w\in Cw\le x\right)$$