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	syl5eq	|- ( ( ( 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 )