This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mbfconstlem

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

Ref Expression
Assertion mbfconstlem 
|- ( ( A e. dom vol /\ C e. RR ) -> ( `' ( A X. { C } ) " B ) e. dom vol )

Proof

Step Hyp Ref Expression
1 cnvimass 
 |-  ( `' ( A X. { C } ) " B ) C_ dom ( A X. { C } )
2 1 a1i 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ C e. B ) -> ( `' ( A X. { C } ) " B ) C_ dom ( A X. { C } ) )
3 cnvimarndm 
 |-  ( `' ( A X. { C } ) " ran ( A X. { C } ) ) = dom ( A X. { C } )
4 fconst6g 
 |-  ( C e. B -> ( A X. { C } ) : A --> B )
5 4 adantl 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ C e. B ) -> ( A X. { C } ) : A --> B )
6 frn 
 |-  ( ( A X. { C } ) : A --> B -> ran ( A X. { C } ) C_ B )
7 imass2 
 |-  ( ran ( A X. { C } ) C_ B -> ( `' ( A X. { C } ) " ran ( A X. { C } ) ) C_ ( `' ( A X. { C } ) " B ) )
8 5 6 7 3syl 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ C e. B ) -> ( `' ( A X. { C } ) " ran ( A X. { C } ) ) C_ ( `' ( A X. { C } ) " B ) )
9 3 8 eqsstrrid 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ C e. B ) -> dom ( A X. { C } ) C_ ( `' ( A X. { C } ) " B ) )
10 2 9 eqssd 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ C e. B ) -> ( `' ( A X. { C } ) " B ) = dom ( A X. { C } ) )
11 fconstg 
 |-  ( C e. RR -> ( A X. { C } ) : A --> { C } )
12 11 ad2antlr 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ C e. B ) -> ( A X. { C } ) : A --> { C } )
13 12 fdmd 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ C e. B ) -> dom ( A X. { C } ) = A )
14 10 13 eqtrd 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ C e. B ) -> ( `' ( A X. { C } ) " B ) = A )
15 simpll 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ C e. B ) -> A e. dom vol )
16 14 15 eqeltrd 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ C e. B ) -> ( `' ( A X. { C } ) " B ) e. dom vol )
17 11 ad2antlr 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ -. C e. B ) -> ( A X. { C } ) : A --> { C } )
18 incom 
 |-  ( { C } i^i B ) = ( B i^i { C } )
19 simpr 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ -. C e. B ) -> -. C e. B )
20 disjsn 
 |-  ( ( B i^i { C } ) = (/) <-> -. C e. B )
21 19 20 sylibr 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ -. C e. B ) -> ( B i^i { C } ) = (/) )
22 18 21 eqtrid 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ -. C e. B ) -> ( { C } i^i B ) = (/) )
23 fimacnvdisj 
 |-  ( ( ( A X. { C } ) : A --> { C } /\ ( { C } i^i B ) = (/) ) -> ( `' ( A X. { C } ) " B ) = (/) )
24 17 22 23 syl2anc 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ -. C e. B ) -> ( `' ( A X. { C } ) " B ) = (/) )
25 0mbl 
 |-  (/) e. dom vol
26 24 25 eqeltrdi 
 |-  ( ( ( A e. dom vol /\ C e. RR ) /\ -. C e. B ) -> ( `' ( A X. { C } ) " B ) e. dom vol )
27 16 26 pm2.61dan 
 |-  ( ( A e. dom vol /\ C e. RR ) -> ( `' ( A X. { C } ) " B ) e. dom vol )