Metamath Proof Explorer

Theorem supmullem2

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

Ref Expression
Hypotheses supmul.1 ⊢C=z|∃v∈A∃b∈Bz=v⁢b
supmul.2 ⊢φ↔∀x∈A0≤x∧∀x∈B0≤x∧A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧B⊆ℝ∧B≠∅∧∃x∈ℝ∀y∈By≤x
Assertion supmullem2 ⊢φ→C⊆ℝ∧C≠∅∧∃x∈ℝ∀w∈Cw≤x

Proof

Step Hyp Ref Expression
1 supmul.1 ⊢C=z|∃v∈A∃b∈Bz=v⁢b
2 supmul.2 ⊢φ↔∀x∈A0≤x∧∀x∈B0≤x∧A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧B⊆ℝ∧B≠∅∧∃x∈ℝ∀y∈By≤x
3 vex ⊢w∈V
4 oveq1 ⊢v=a→v⁢b=a⁢b
5 4 eqeq2d ⊢v=a→z=v⁢b↔z=a⁢b
6 5 rexbidv ⊢v=a→∃b∈Bz=v⁢b↔∃b∈Bz=a⁢b
7 6 cbvrexvw ⊢∃v∈A∃b∈Bz=v⁢b↔∃a∈A∃b∈Bz=a⁢b
8 eqeq1 ⊢z=w→z=a⁢b↔w=a⁢b
9 8 2rexbidv ⊢z=w→∃a∈A∃b∈Bz=a⁢b↔∃a∈A∃b∈Bw=a⁢b
10 7 9 bitrid ⊢z=w→∃v∈A∃b∈Bz=v⁢b↔∃a∈A∃b∈Bw=a⁢b
11 3 10 1 elab2 ⊢w∈C↔∃a∈A∃b∈Bw=a⁢b
12 2 simp2bi ⊢φ→A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x
13 12 simp1d ⊢φ→A⊆ℝ
14 13 sseld ⊢φ→a∈A→a∈ℝ
15 2 simp3bi ⊢φ→B⊆ℝ∧B≠∅∧∃x∈ℝ∀y∈By≤x
16 15 simp1d ⊢φ→B⊆ℝ
17 16 sseld ⊢φ→b∈B→b∈ℝ
18 14 17 anim12d ⊢φ→a∈A∧b∈B→a∈ℝ∧b∈ℝ
19 remulcl ⊢a∈ℝ∧b∈ℝ→a⁢b∈ℝ
20 18 19 syl6 ⊢φ→a∈A∧b∈B→a⁢b∈ℝ
21 eleq1a ⊢a⁢b∈ℝ→w=a⁢b→w∈ℝ
22 20 21 syl6 ⊢φ→a∈A∧b∈B→w=a⁢b→w∈ℝ
23 22 rexlimdvv ⊢φ→∃a∈A∃b∈Bw=a⁢b→w∈ℝ
24 11 23 biimtrid ⊢φ→w∈C→w∈ℝ
25 24 ssrdv ⊢φ→C⊆ℝ
26 12 simp2d ⊢φ→A≠∅
27 15 simp2d ⊢φ→B≠∅
28 ovex ⊢a⁢b∈V
29 28 isseti ⊢∃ww=a⁢b
30 29 rgenw ⊢∀b∈B∃ww=a⁢b
31 r19.2z ⊢B≠∅∧∀b∈B∃ww=a⁢b→∃b∈B∃ww=a⁢b
32 27 30 31 sylancl ⊢φ→∃b∈B∃ww=a⁢b
33 rexcom4 ⊢∃b∈B∃ww=a⁢b↔∃w∃b∈Bw=a⁢b
34 32 33 sylib ⊢φ→∃w∃b∈Bw=a⁢b
35 34 ralrimivw ⊢φ→∀a∈A∃w∃b∈Bw=a⁢b
36 r19.2z ⊢A≠∅∧∀a∈A∃w∃b∈Bw=a⁢b→∃a∈A∃w∃b∈Bw=a⁢b
37 26 35 36 syl2anc ⊢φ→∃a∈A∃w∃b∈Bw=a⁢b
38 rexcom4 ⊢∃a∈A∃w∃b∈Bw=a⁢b↔∃w∃a∈A∃b∈Bw=a⁢b
39 37 38 sylib ⊢φ→∃w∃a∈A∃b∈Bw=a⁢b
40 n0 ⊢C≠∅↔∃ww∈C
41 11 exbii ⊢∃ww∈C↔∃w∃a∈A∃b∈Bw=a⁢b
42 40 41 bitri ⊢C≠∅↔∃w∃a∈A∃b∈Bw=a⁢b
43 39 42 sylibr ⊢φ→C≠∅
44 suprcl ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→supAℝ<∈ℝ
45 12 44 syl ⊢φ→supAℝ<∈ℝ
46 suprcl ⊢B⊆ℝ∧B≠∅∧∃x∈ℝ∀y∈By≤x→supBℝ<∈ℝ
47 15 46 syl ⊢φ→supBℝ<∈ℝ
48 45 47 remulcld ⊢φ→supAℝ<⁢supBℝ<∈ℝ
49 1 2 supmullem1 ⊢φ→∀w∈Cw≤supAℝ<⁢supBℝ<
50 brralrspcev ⊢supAℝ<⁢supBℝ<∈ℝ∧∀w∈Cw≤supAℝ<⁢supBℝ<→∃x∈ℝ∀w∈Cw≤x
51 48 49 50 syl2anc ⊢φ→∃x∈ℝ∀w∈Cw≤x
52 25 43 51 3jca ⊢φ→C⊆ℝ∧C≠∅∧∃x∈ℝ∀w∈Cw≤x