Metamath Proof Explorer

Theorem mbfconstlem

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

Ref Expression
Assertion mbfconstlem ( ( 𝐴 ∈ dom vol ∧ 𝐶 ∈ ℝ ) → ( ◡ ( 𝐴 × { 𝐶 } ) “ 𝐵 ) ∈ dom vol )

Proof

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