MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bropopvvv Structured version   Visualization version   Unicode version
Theorem bropopvvv 7255
Description: If a binary relation holds for the result of an operation which is a result of an operation, the involved classes are sets. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Proof shortened by AV, 3-Jan-2021.)
Hypotheses
Ref Expression
bropopvvv.o |- O = ( v e. _V , e e. _V |-> ( a e. v , b e. v |-> { <. f , p >. | ph } ) )
bropopvvv.p |- ( ( v = V /\ e = E ) -> ( ph <-> ps ) )
bropopvvv.oo |- ( ( ( V e. _V /\ E e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( A ( V O E ) B ) = { <. f , p >. | th } )
Assertion
Ref Expression
bropopvvv |- ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) )
Distinct variable groups:   E, a, b, e, f, p, v   V, a, b, e, f, p, v   ps, e, v
Allowed substitution hints:   ph( v, e, f, p, a, b)   ps( f, p, a, b)   th( v, e, f, p, a, b)   A( v, e, f, p, a, b)   B( v, e, f, p, a, b)   P( v, e, f, p, a, b)   F( v, e, f, p, a, b)   O( v, e, f, p, a, b)
Proof of Theorem bropopvvv
Dummy variable c is distinct from all other variables.
StepHypRef Expression
1 brovpreldm 7254 . . 3 |- ( F ( A ( V O E ) B ) P -> <. A , B >. e. dom ( V O E ) )
2 simpl 473 . . . . . . . . 9 |- ( ( v = V /\ e = E ) -> v = V )
3 bropopvvv.p . . . . . . . . . 10 |- ( ( v = V /\ e = E ) -> ( ph <-> ps ) )
43opabbidv 4716 . . . . . . . . 9 |- ( ( v = V /\ e = E ) -> { <. f , p >. | ph } = { <. f , p >. | ps } )
52, 2, 4mpt2eq123dv 6717 . . . . . . . 8 |- ( ( v = V /\ e = E ) -> ( a e. v , b e. v |-> { <. f , p >. | ph } ) = ( a e. V , b e. V |-> { <. f , p >. | ps } ) )
6 bropopvvv.o . . . . . . . 8 |- O = ( v e. _V , e e. _V |-> ( a e. v , b e. v |-> { <. f , p >. | ph } ) )
75, 6ovmpt2ga 6790 . . . . . . 7 |- ( ( V e. _V /\ E e. _V /\ ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V ) -> ( V O E ) = ( a e. V , b e. V |-> { <. f , p >. | ps } ) )
87dmeqd 5326 . . . . . 6 |- ( ( V e. _V /\ E e. _V /\ ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V ) -> dom ( V O E ) = dom ( a e. V , b e. V |-> { <. f , p >. | ps } ) )
98eleq2d 2687 . . . . 5 |- ( ( V e. _V /\ E e. _V /\ ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V ) -> ( <. A , B >. e. dom ( V O E ) <-> <. A , B >. e. dom ( a e. V , b e. V |-> { <. f , p >. | ps } ) ) )
10 dmoprabss 6742 . . . . . . . 8 |- dom { <. <. a , b >. , c >. | ( ( a e. V /\ b e. V ) /\ c = { <. f , p >. | ps } ) } C_ ( V X. V )
1110sseli 3599 . . . . . . 7 |- ( <. A , B >. e. dom { <. <. a , b >. , c >. | ( ( a e. V /\ b e. V ) /\ c = { <. f , p >. | ps } ) } -> <. A , B >. e. ( V X. V ) )
12 opelxp 5146 . . . . . . . 8 |- ( <. A , B >. e. ( V X. V ) <-> ( A e. V /\ B e. V ) )
13 df-br 4654 . . . . . . . . . . . . 13 |- ( F ( A ( V O E ) B ) P <-> <. F , P >. e. ( A ( V O E ) B ) )
14 ne0i 3921 . . . . . . . . . . . . . 14 |- ( <. F , P >. e. ( A ( V O E ) B ) -> ( A ( V O E ) B ) =/= (/) )
15 bropopvvv.oo . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( V e. _V /\ E e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( A ( V O E ) B ) = { <. f , p >. | th } )
1615breqd 4664 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( V e. _V /\ E e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( F ( A ( V O E ) B ) P <-> F { <. f , p >. | th } P ) )
17 brabv 6699 . . . . . . . . . . . . . . . . . . . . . 22 |- ( F { <. f , p >. | th } P -> ( F e. _V /\ P e. _V ) )
1817anim2i 593 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( V e. _V /\ E e. _V ) /\ F { <. f , p >. | th } P ) -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) )
1918ex 450 . . . . . . . . . . . . . . . . . . . 20 |- ( ( V e. _V /\ E e. _V ) -> ( F { <. f , p >. | th } P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) )
2019adantr 481 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( V e. _V /\ E e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( F { <. f , p >. | th } P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) )
2116, 20sylbid 230 . . . . . . . . . . . . . . . . . 18 |- ( ( ( V e. _V /\ E e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) )
2221ex 450 . . . . . . . . . . . . . . . . 17 |- ( ( V e. _V /\ E e. _V ) -> ( ( A e. V /\ B e. V ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) ) )
2322com23 86 . . . . . . . . . . . . . . . 16 |- ( ( V e. _V /\ E e. _V ) -> ( F ( A ( V O E ) B ) P -> ( ( A e. V /\ B e. V ) -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) ) )
2423a1d 25 . . . . . . . . . . . . . . 15 |- ( ( V e. _V /\ E e. _V ) -> ( ( A ( V O E ) B ) =/= (/) -> ( F ( A ( V O E ) B ) P -> ( ( A e. V /\ B e. V ) -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) ) ) )
256mpt2ndm0 6875 . . . . . . . . . . . . . . . 16 |- ( -. ( V e. _V /\ E e. _V ) -> ( V O E ) = (/) )
26 df-ov 6653 . . . . . . . . . . . . . . . . . 18 |- ( A ( V O E ) B ) = ( ( V O E ) ` <. A , B >. )
27 fveq1 6190 . . . . . . . . . . . . . . . . . 18 |- ( ( V O E ) = (/) -> ( ( V O E ) ` <. A , B >. ) = ( (/) ` <. A , B >. ) )
2826, 27syl5eq 2668 . . . . . . . . . . . . . . . . 17 |- ( ( V O E ) = (/) -> ( A ( V O E ) B ) = ( (/) ` <. A , B >. ) )
29 0fv 6227 . . . . . . . . . . . . . . . . 17 |- ( (/) ` <. A , B >. ) = (/)
3028, 29syl6eq 2672 . . . . . . . . . . . . . . . 16 |- ( ( V O E ) = (/) -> ( A ( V O E ) B ) = (/) )
31 eqneqall 2805 . . . . . . . . . . . . . . . 16 |- ( ( A ( V O E ) B ) = (/) -> ( ( A ( V O E ) B ) =/= (/) -> ( F ( A ( V O E ) B ) P -> ( ( A e. V /\ B e. V ) -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) ) ) )
3225, 30, 313syl 18 . . . . . . . . . . . . . . 15 |- ( -. ( V e. _V /\ E e. _V ) -> ( ( A ( V O E ) B ) =/= (/) -> ( F ( A ( V O E ) B ) P -> ( ( A e. V /\ B e. V ) -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) ) ) )
3324, 32pm2.61i 176 . . . . . . . . . . . . . 14 |- ( ( A ( V O E ) B ) =/= (/) -> ( F ( A ( V O E ) B ) P -> ( ( A e. V /\ B e. V ) -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) ) )
3414, 33syl 17 . . . . . . . . . . . . 13 |- ( <. F , P >. e. ( A ( V O E ) B ) -> ( F ( A ( V O E ) B ) P -> ( ( A e. V /\ B e. V ) -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) ) )
3513, 34sylbi 207 . . . . . . . . . . . 12 |- ( F ( A ( V O E ) B ) P -> ( F ( A ( V O E ) B ) P -> ( ( A e. V /\ B e. V ) -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) ) )
3635pm2.43i 52 . . . . . . . . . . 11 |- ( F ( A ( V O E ) B ) P -> ( ( A e. V /\ B e. V ) -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) )
3736com12 32 . . . . . . . . . 10 |- ( ( A e. V /\ B e. V ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) )
3837anc2ri 581 . . . . . . . . 9 |- ( ( A e. V /\ B e. V ) -> ( F ( A ( V O E ) B ) P -> ( ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) /\ ( A e. V /\ B e. V ) ) ) )
39 df-3an 1039 . . . . . . . . 9 |- ( ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) <-> ( ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) /\ ( A e. V /\ B e. V ) ) )
4038, 39syl6ibr 242 . . . . . . . 8 |- ( ( A e. V /\ B e. V ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) )
4112, 40sylbi 207 . . . . . . 7 |- ( <. A , B >. e. ( V X. V ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) )
4211, 41syl 17 . . . . . 6 |- ( <. A , B >. e. dom { <. <. a , b >. , c >. | ( ( a e. V /\ b e. V ) /\ c = { <. f , p >. | ps } ) } -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) )
43 df-mpt2 6655 . . . . . . 7 |- ( a e. V , b e. V |-> { <. f , p >. | ps } ) = { <. <. a , b >. , c >. | ( ( a e. V /\ b e. V ) /\ c = { <. f , p >. | ps } ) }
4443dmeqi 5325 . . . . . 6 |- dom ( a e. V , b e. V |-> { <. f , p >. | ps } ) = dom { <. <. a , b >. , c >. | ( ( a e. V /\ b e. V ) /\ c = { <. f , p >. | ps } ) }
4542, 44eleq2s 2719 . . . . 5 |- ( <. A , B >. e. dom ( a e. V , b e. V |-> { <. f , p >. | ps } ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) )
469, 45syl6bi 243 . . . 4 |- ( ( V e. _V /\ E e. _V /\ ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V ) -> ( <. A , B >. e. dom ( V O E ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) ) )
47 3ianor 1055 . . . . 5 |- ( -. ( V e. _V /\ E e. _V /\ ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V ) <-> ( -. V e. _V \/ -. E e. _V \/ -. ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V ) )
48 df-3or 1038 . . . . . 6 |- ( ( -. V e. _V \/ -. E e. _V \/ -. ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V ) <-> ( ( -. V e. _V \/ -. E e. _V ) \/ -. ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V ) )
49 ianor 509 . . . . . . . 8 |- ( -. ( V e. _V /\ E e. _V ) <-> ( -. V e. _V \/ -. E e. _V ) )
5025dmeqd 5326 . . . . . . . . . . 11 |- ( -. ( V e. _V /\ E e. _V ) -> dom ( V O E ) = dom (/) )
5150eleq2d 2687 . . . . . . . . . 10 |- ( -. ( V e. _V /\ E e. _V ) -> ( <. A , B >. e. dom ( V O E ) <-> <. A , B >. e. dom (/) ) )
52 dm0 5339 . . . . . . . . . . 11 |- dom (/) = (/)
5352eleq2i 2693 . . . . . . . . . 10 |- ( <. A , B >. e. dom (/) <-> <. A , B >. e. (/) )
5451, 53syl6bb 276 . . . . . . . . 9 |- ( -. ( V e. _V /\ E e. _V ) -> ( <. A , B >. e. dom ( V O E ) <-> <. A , B >. e. (/) ) )
55 noel 3919 . . . . . . . . . 10 |- -. <. A , B >. e. (/)
5655pm2.21i 116 . . . . . . . . 9 |- ( <. A , B >. e. (/) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) )
5754, 56syl6bi 243 . . . . . . . 8 |- ( -. ( V e. _V /\ E e. _V ) -> ( <. A , B >. e. dom ( V O E ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) ) )
5849, 57sylbir 225 . . . . . . 7 |- ( ( -. V e. _V \/ -. E e. _V ) -> ( <. A , B >. e. dom ( V O E ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) ) )
59 anor 510 . . . . . . . . 9 |- ( ( V e. _V /\ E e. _V ) <-> -. ( -. V e. _V \/ -. E e. _V ) )
60 id 22 . . . . . . . . . . . . 13 |- ( V e. _V -> V e. _V )
6160ancri 575 . . . . . . . . . . . 12 |- ( V e. _V -> ( V e. _V /\ V e. _V ) )
6261adantr 481 . . . . . . . . . . 11 |- ( ( V e. _V /\ E e. _V ) -> ( V e. _V /\ V e. _V ) )
63 mpt2exga 7246 . . . . . . . . . . 11 |- ( ( V e. _V /\ V e. _V ) -> ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V )
6462, 63syl 17 . . . . . . . . . 10 |- ( ( V e. _V /\ E e. _V ) -> ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V )
6564pm2.24d 147 . . . . . . . . 9 |- ( ( V e. _V /\ E e. _V ) -> ( -. ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V -> ( <. A , B >. e. dom ( V O E ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) ) ) )
6659, 65sylbir 225 . . . . . . . 8 |- ( -. ( -. V e. _V \/ -. E e. _V ) -> ( -. ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V -> ( <. A , B >. e. dom ( V O E ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) ) ) )
6766imp 445 . . . . . . 7 |- ( ( -. ( -. V e. _V \/ -. E e. _V ) /\ -. ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V ) -> ( <. A , B >. e. dom ( V O E ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) ) )
6858, 67jaoi3 1011 . . . . . 6 |- ( ( ( -. V e. _V \/ -. E e. _V ) \/ -. ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V ) -> ( <. A , B >. e. dom ( V O E ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) ) )
6948, 68sylbi 207 . . . . 5 |- ( ( -. V e. _V \/ -. E e. _V \/ -. ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V ) -> ( <. A , B >. e. dom ( V O E ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) ) )
7047, 69sylbi 207 . . . 4 |- ( -. ( V e. _V /\ E e. _V /\ ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V ) -> ( <. A , B >. e. dom ( V O E ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) ) )
7146, 70pm2.61i 176 . . 3 |- ( <. A , B >. e. dom ( V O E ) -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) )
721, 71syl 17 . 2 |- ( F ( A ( V O E ) B ) P -> ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) ) )
7372pm2.43i 52 1 |- ( F ( A ( V O E ) B ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) /\ ( A e. V /\ B e. V ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   \/ w3o 1036   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   _Vcvv 3200   (/)c0 3915   <.cop 4183   class class class wbr 4653   {copab 4712   X. cxp 5112   dom cdm 5114   ` cfv 5888  (class class class)co 6650   {coprab 6651   |-> cmpt2 6652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator