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

Metamath Proof Explorer

Theorem ovmpt3rabdm

Description: If the value of a function which is the result of an operation defined by the maps-to notation is not empty, the operands and the argument of the function must be sets. (Contributed by AV, 16-May-2019)

Ref Expression
Hypotheses ovmpt3rab1.o 
|- O = ( x e. _V , y e. _V |-> ( z e. M |-> { a e. N | ph } ) )
ovmpt3rab1.m 
|- ( ( x = X /\ y = Y ) -> M = K )
ovmpt3rab1.n 
|- ( ( x = X /\ y = Y ) -> N = L )
Assertion ovmpt3rabdm 
|- ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> dom ( X O Y ) = K )

Proof

Step Hyp Ref Expression
1 ovmpt3rab1.o 
 |-  O = ( x e. _V , y e. _V |-> ( z e. M |-> { a e. N | ph } ) )
2 ovmpt3rab1.m 
 |-  ( ( x = X /\ y = Y ) -> M = K )
3 ovmpt3rab1.n 
 |-  ( ( x = X /\ y = Y ) -> N = L )
4 sbceq1a 
 |-  ( y = Y -> ( ph <-> [. Y / y ]. ph ) )
5 sbceq1a 
 |-  ( x = X -> ( [. Y / y ]. ph <-> [. X / x ]. [. Y / y ]. ph ) )
6 4 5 sylan9bbr 
 |-  ( ( x = X /\ y = Y ) -> ( ph <-> [. X / x ]. [. Y / y ]. ph ) )
7 nfsbc1v 
 |-  F/ x [. X / x ]. [. Y / y ]. ph
8 nfcv 
 |-  F/_ y X
9 nfsbc1v 
 |-  F/ y [. Y / y ]. ph
10 8 9 nfsbcw 
 |-  F/ y [. X / x ]. [. Y / y ]. ph
11 1 2 3 6 7 10 ovmpt3rab1 
 |-  ( ( X e. V /\ Y e. W /\ K e. U ) -> ( X O Y ) = ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) )
12 11 adantr 
 |-  ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> ( X O Y ) = ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) )
13 12 dmeqd 
 |-  ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> dom ( X O Y ) = dom ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) )
14 rabexg 
 |-  ( L e. T -> { a e. L | [. X / x ]. [. Y / y ]. ph } e. _V )
15 14 adantl 
 |-  ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> { a e. L | [. X / x ]. [. Y / y ]. ph } e. _V )
16 15 ralrimivw 
 |-  ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> A. z e. K { a e. L | [. X / x ]. [. Y / y ]. ph } e. _V )
17 dmmptg 
 |-  ( A. z e. K { a e. L | [. X / x ]. [. Y / y ]. ph } e. _V -> dom ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) = K )
18 16 17 syl 
 |-  ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> dom ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) = K )
19 13 18 eqtrd 
 |-  ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> dom ( X O Y ) = K )