Metamath Proof Explorer

Theorem mbfconstlem

Description: Lemma for mbfconst and related theorems. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion mbfconstlem ⊢A∈dom⁡vol∧C∈ℝ→A×C-1B∈dom⁡vol

Proof

Step Hyp Ref Expression
1 cnvimass ⊢A×C-1B⊆dom⁡A×C
2 1 a1i ⊢A∈dom⁡vol∧C∈ℝ∧C∈B→A×C-1B⊆dom⁡A×C
3 cnvimarndm ⊢A×C-1ran⁡A×C=dom⁡A×C
4 fconst6g ⊢C∈B→A×C:A⟶B
5 4 adantl ⊢A∈dom⁡vol∧C∈ℝ∧C∈B→A×C:A⟶B
6 frn ⊢A×C:A⟶B→ran⁡A×C⊆B
7 imass2 ⊢ran⁡A×C⊆B→A×C-1ran⁡A×C⊆A×C-1B
8 5 6 7 3syl ⊢A∈dom⁡vol∧C∈ℝ∧C∈B→A×C-1ran⁡A×C⊆A×C-1B
9 3 8 eqsstrrid ⊢A∈dom⁡vol∧C∈ℝ∧C∈B→dom⁡A×C⊆A×C-1B
10 2 9 eqssd ⊢A∈dom⁡vol∧C∈ℝ∧C∈B→A×C-1B=dom⁡A×C
11 fconstg ⊢C∈ℝ→A×C:A⟶C
12 11 ad2antlr ⊢A∈dom⁡vol∧C∈ℝ∧C∈B→A×C:A⟶C
13 12 fdmd ⊢A∈dom⁡vol∧C∈ℝ∧C∈B→dom⁡A×C=A
14 10 13 eqtrd ⊢A∈dom⁡vol∧C∈ℝ∧C∈B→A×C-1B=A
15 simpll ⊢A∈dom⁡vol∧C∈ℝ∧C∈B→A∈dom⁡vol
16 14 15 eqeltrd ⊢A∈dom⁡vol∧C∈ℝ∧C∈B→A×C-1B∈dom⁡vol
17 11 ad2antlr ⊢A∈dom⁡vol∧C∈ℝ∧¬C∈B→A×C:A⟶C
18 incom ⊢C∩B=B∩C
19 simpr ⊢A∈dom⁡vol∧C∈ℝ∧¬C∈B→¬C∈B
20 disjsn ⊢B∩C=∅↔¬C∈B
21 19 20 sylibr ⊢A∈dom⁡vol∧C∈ℝ∧¬C∈B→B∩C=∅
22 18 21 eqtrid ⊢A∈dom⁡vol∧C∈ℝ∧¬C∈B→C∩B=∅
23 fimacnvdisj ⊢A×C:A⟶C∧C∩B=∅→A×C-1B=∅
24 17 22 23 syl2anc ⊢A∈dom⁡vol∧C∈ℝ∧¬C∈B→A×C-1B=∅
25 0mbl ⊢∅∈dom⁡vol
26 24 25 eqeltrdi ⊢A∈dom⁡vol∧C∈ℝ∧¬C∈B→A×C-1B∈dom⁡vol
27 16 26 pm2.61dan ⊢A∈dom⁡vol∧C∈ℝ→A×C-1B∈dom⁡vol