Metamath Proof Explorer

Theorem elovmpt3rab1

Description: Implications for the value of an operation defined by the maps-to notation with a function into a class abstraction as a result having an element. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018) (Revised 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 elovmpt3rab1 
|- ( ( K e. U /\ L e. T ) -> ( A e. ( ( X O Y ) ` Z ) -> ( ( X e. _V /\ Y e. _V ) /\ ( Z e. K /\ A e. L ) ) ) )

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 1 elovmpt3imp 
 |-  ( A e. ( ( X O Y ) ` Z ) -> ( X e. _V /\ Y e. _V ) )
5 simprl 
 |-  ( ( A e. ( ( X O Y ) ` Z ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) -> ( X e. _V /\ Y e. _V ) )
6 elfvdm 
 |-  ( A e. ( ( X O Y ) ` Z ) -> Z e. dom ( X O Y ) )
7 simpl 
 |-  ( ( X e. _V /\ Y e. _V ) -> X e. _V )
8 7 adantr 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) -> X e. _V )
9 simplr 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) -> Y e. _V )
10 simprl 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) -> K e. U )
11 simprr 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) -> L e. T )
12 1 2 3 ovmpt3rabdm 
 |-  ( ( ( X e. _V /\ Y e. _V /\ K e. U ) /\ L e. T ) -> dom ( X O Y ) = K )
13 8 9 10 11 12 syl31anc 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) -> dom ( X O Y ) = K )
14 13 eleq2d 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) -> ( Z e. dom ( X O Y ) <-> Z e. K ) )
15 14 biimpcd 
 |-  ( Z e. dom ( X O Y ) -> ( ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) -> Z e. K ) )
16 15 adantr 
 |-  ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) -> ( ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) -> Z e. K ) )
17 16 imp 
 |-  ( ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) -> Z e. K )
18 simpl 
 |-  ( ( Z e. K /\ ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) ) -> Z e. K )
19 simplr 
 |-  ( ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) -> A e. ( ( X O Y ) ` Z ) )
20 19 adantl 
 |-  ( ( Z e. K /\ ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) ) -> A e. ( ( X O Y ) ` Z ) )
21 simpl 
 |-  ( ( K e. U /\ L e. T ) -> K e. U )
22 21 anim2i 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) -> ( ( X e. _V /\ Y e. _V ) /\ K e. U ) )
23 df-3an 
 |-  ( ( X e. _V /\ Y e. _V /\ K e. U ) <-> ( ( X e. _V /\ Y e. _V ) /\ K e. U ) )
24 22 23 sylibr 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) -> ( X e. _V /\ Y e. _V /\ K e. U ) )
25 24 ad2antll 
 |-  ( ( Z e. K /\ ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) ) -> ( X e. _V /\ Y e. _V /\ K e. U ) )
26 sbceq1a 
 |-  ( y = Y -> ( ph <-> [. Y / y ]. ph ) )
27 sbceq1a 
 |-  ( x = X -> ( [. Y / y ]. ph <-> [. X / x ]. [. Y / y ]. ph ) )
28 26 27 sylan9bbr 
 |-  ( ( x = X /\ y = Y ) -> ( ph <-> [. X / x ]. [. Y / y ]. ph ) )
29 nfsbc1v 
 |-  F/ x [. X / x ]. [. Y / y ]. ph
30 nfcv 
 |-  F/_ y X
31 nfsbc1v 
 |-  F/ y [. Y / y ]. ph
32 30 31 nfsbcw 
 |-  F/ y [. X / x ]. [. Y / y ]. ph
33 1 2 3 28 29 32 ovmpt3rab1 
 |-  ( ( X e. _V /\ Y e. _V /\ K e. U ) -> ( X O Y ) = ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) )
34 33 fveq1d 
 |-  ( ( X e. _V /\ Y e. _V /\ K e. U ) -> ( ( X O Y ) ` Z ) = ( ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) ` Z ) )
35 25 34 syl 
 |-  ( ( Z e. K /\ ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) ) -> ( ( X O Y ) ` Z ) = ( ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) ` Z ) )
36 rabexg 
 |-  ( L e. T -> { a e. L | [. Z / z ]. [. X / x ]. [. Y / y ]. ph } e. _V )
37 36 adantl 
 |-  ( ( K e. U /\ L e. T ) -> { a e. L | [. Z / z ]. [. X / x ]. [. Y / y ]. ph } e. _V )
38 37 ad2antll 
 |-  ( ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) -> { a e. L | [. Z / z ]. [. X / x ]. [. Y / y ]. ph } e. _V )
39 nfcv 
 |-  F/_ z Z
40 nfsbc1v 
 |-  F/ z [. Z / z ]. [. X / x ]. [. Y / y ]. ph
41 nfcv 
 |-  F/_ z L
42 40 41 nfrabw 
 |-  F/_ z { a e. L | [. Z / z ]. [. X / x ]. [. Y / y ]. ph }
43 sbceq1a 
 |-  ( z = Z -> ( [. X / x ]. [. Y / y ]. ph <-> [. Z / z ]. [. X / x ]. [. Y / y ]. ph ) )
44 43 rabbidv 
 |-  ( z = Z -> { a e. L | [. X / x ]. [. Y / y ]. ph } = { a e. L | [. Z / z ]. [. X / x ]. [. Y / y ]. ph } )
45 eqid 
 |-  ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) = ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } )
46 39 42 44 45 fvmptf 
 |-  ( ( Z e. K /\ { a e. L | [. Z / z ]. [. X / x ]. [. Y / y ]. ph } e. _V ) -> ( ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) ` Z ) = { a e. L | [. Z / z ]. [. X / x ]. [. Y / y ]. ph } )
47 38 46 sylan2 
 |-  ( ( Z e. K /\ ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) ) -> ( ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) ` Z ) = { a e. L | [. Z / z ]. [. X / x ]. [. Y / y ]. ph } )
48 35 47 eqtr2d 
 |-  ( ( Z e. K /\ ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) ) -> { a e. L | [. Z / z ]. [. X / x ]. [. Y / y ]. ph } = ( ( X O Y ) ` Z ) )
49 20 48 eleqtrrd 
 |-  ( ( Z e. K /\ ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) ) -> A e. { a e. L | [. Z / z ]. [. X / x ]. [. Y / y ]. ph } )
50 elrabi 
 |-  ( A e. { a e. L | [. Z / z ]. [. X / x ]. [. Y / y ]. ph } -> A e. L )
51 49 50 syl 
 |-  ( ( Z e. K /\ ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) ) -> A e. L )
52 18 51 jca 
 |-  ( ( Z e. K /\ ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) ) -> ( Z e. K /\ A e. L ) )
53 17 52 mpancom 
 |-  ( ( ( Z e. dom ( X O Y ) /\ A e. ( ( X O Y ) ` Z ) ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) -> ( Z e. K /\ A e. L ) )
54 53 exp31 
 |-  ( Z e. dom ( X O Y ) -> ( A e. ( ( X O Y ) ` Z ) -> ( ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) -> ( Z e. K /\ A e. L ) ) ) )
55 6 54 mpcom 
 |-  ( A e. ( ( X O Y ) ` Z ) -> ( ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) -> ( Z e. K /\ A e. L ) ) )
56 55 imp 
 |-  ( ( A e. ( ( X O Y ) ` Z ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) -> ( Z e. K /\ A e. L ) )
57 5 56 jca 
 |-  ( ( A e. ( ( X O Y ) ` Z ) /\ ( ( X e. _V /\ Y e. _V ) /\ ( K e. U /\ L e. T ) ) ) -> ( ( X e. _V /\ Y e. _V ) /\ ( Z e. K /\ A e. L ) ) )
58 57 exp32 
 |-  ( A e. ( ( X O Y ) ` Z ) -> ( ( X e. _V /\ Y e. _V ) -> ( ( K e. U /\ L e. T ) -> ( ( X e. _V /\ Y e. _V ) /\ ( Z e. K /\ A e. L ) ) ) ) )
59 4 58 mpd 
 |-  ( A e. ( ( X O Y ) ` Z ) -> ( ( K e. U /\ L e. T ) -> ( ( X e. _V /\ Y e. _V ) /\ ( Z e. K /\ A e. L ) ) ) )
60 59 com12 
 |-  ( ( K e. U /\ L e. T ) -> ( A e. ( ( X O Y ) ` Z ) -> ( ( X e. _V /\ Y e. _V ) /\ ( Z e. K /\ A e. L ) ) ) )