Metamath Proof Explorer

Theorem bropopvvv

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)

Ref Expression
Hypotheses 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 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 ) ) )

Proof

Step Hyp Ref Expression
1 bropopvvv.o 
 |-  O = ( v e. _V , e e. _V |-> ( a e. v , b e. v |-> { <. f , p >. | ph } ) )
2 bropopvvv.p 
 |-  ( ( v = V /\ e = E ) -> ( ph <-> ps ) )
3 bropopvvv.oo 
 |-  ( ( ( V e. _V /\ E e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( A ( V O E ) B ) = { <. f , p >. | th } )
4 brovpreldm 
 |-  ( F ( A ( V O E ) B ) P -> <. A , B >. e. dom ( V O E ) )
5 simpl 
 |-  ( ( v = V /\ e = E ) -> v = V )
6 2 opabbidv 
 |-  ( ( v = V /\ e = E ) -> { <. f , p >. | ph } = { <. f , p >. | ps } )
7 5 5 6 mpoeq123dv 
 |-  ( ( v = V /\ e = E ) -> ( a e. v , b e. v |-> { <. f , p >. | ph } ) = ( a e. V , b e. V |-> { <. f , p >. | ps } ) )
8 7 1 ovmpoga 
 |-  ( ( 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 } ) )
9 8 dmeqd 
 |-  ( ( 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 } ) )
10 9 eleq2d 
 |-  ( ( 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 } ) ) )
11 dmoprabss 
 |-  dom { <. <. a , b >. , c >. | ( ( a e. V /\ b e. V ) /\ c = { <. f , p >. | ps } ) } C_ ( V X. V )
12 11 sseli 
 |-  ( <. A , B >. e. dom { <. <. a , b >. , c >. | ( ( a e. V /\ b e. V ) /\ c = { <. f , p >. | ps } ) } -> <. A , B >. e. ( V X. V ) )
13 opelxp 
 |-  ( <. A , B >. e. ( V X. V ) <-> ( A e. V /\ B e. V ) )
14 df-br 
 |-  ( F ( A ( V O E ) B ) P <-> <. F , P >. e. ( A ( V O E ) B ) )
15 ne0i 
 |-  ( <. F , P >. e. ( A ( V O E ) B ) -> ( A ( V O E ) B ) =/= (/) )
16 3 breqd 
 |-  ( ( ( 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 
 |-  ( F { <. f , p >. | th } P -> ( F e. _V /\ P e. _V ) )
18 17 anim2i 
 |-  ( ( ( V e. _V /\ E e. _V ) /\ F { <. f , p >. | th } P ) -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) )
19 18 ex 
 |-  ( ( V e. _V /\ E e. _V ) -> ( F { <. f , p >. | th } P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) ) )
20 19 adantr 
 |-  ( ( ( 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 ) ) ) )
21 16 20 sylbid 
 |-  ( ( ( 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 ) ) ) )
22 21 ex 
 |-  ( ( 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 ) ) ) ) )
23 22 com23 
 |-  ( ( 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 ) ) ) ) )
24 23 a1d 
 |-  ( ( 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 ) ) ) ) ) )
25 1 mpondm0 
 |-  ( -. ( V e. _V /\ E e. _V ) -> ( V O E ) = (/) )
26 df-ov 
 |-  ( A ( V O E ) B ) = ( ( V O E ) ` <. A , B >. )
27 fveq1 
 |-  ( ( V O E ) = (/) -> ( ( V O E ) ` <. A , B >. ) = ( (/) ` <. A , B >. ) )
28 26 27 eqtrid 
 |-  ( ( V O E ) = (/) -> ( A ( V O E ) B ) = ( (/) ` <. A , B >. ) )
29 0fv 
 |-  ( (/) ` <. A , B >. ) = (/)
30 28 29 eqtrdi 
 |-  ( ( V O E ) = (/) -> ( A ( V O E ) B ) = (/) )
31 eqneqall 
 |-  ( ( 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 ) ) ) ) ) )
32 25 30 31 3syl 
 |-  ( -. ( 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 ) ) ) ) ) )
33 24 32 pm2.61i 
 |-  ( ( 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 ) ) ) ) )
34 15 33 syl 
 |-  ( <. 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 ) ) ) ) )
35 14 34 sylbi 
 |-  ( 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 ) ) ) ) )
36 35 pm2.43i 
 |-  ( 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 ) ) ) )
37 36 com12 
 |-  ( ( 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 ) ) ) )
38 37 anc2ri 
 |-  ( ( 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 
 |-  ( ( ( 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 ) ) )
40 38 39 imbitrrdi 
 |-  ( ( 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 ) ) ) )
41 13 40 sylbi 
 |-  ( <. 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 ) ) ) )
42 12 41 syl 
 |-  ( <. 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-mpo 
 |-  ( a e. V , b e. V |-> { <. f , p >. | ps } ) = { <. <. a , b >. , c >. | ( ( a e. V /\ b e. V ) /\ c = { <. f , p >. | ps } ) }
44 43 dmeqi 
 |-  dom ( a e. V , b e. V |-> { <. f , p >. | ps } ) = dom { <. <. a , b >. , c >. | ( ( a e. V /\ b e. V ) /\ c = { <. f , p >. | ps } ) }
45 42 44 eleq2s 
 |-  ( <. 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 ) ) ) )
46 10 45 biimtrdi 
 |-  ( ( 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 
 |-  ( -. ( 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 
 |-  ( ( -. 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 
 |-  ( -. ( V e. _V /\ E e. _V ) <-> ( -. V e. _V \/ -. E e. _V ) )
50 25 dmeqd 
 |-  ( -. ( V e. _V /\ E e. _V ) -> dom ( V O E ) = dom (/) )
51 50 eleq2d 
 |-  ( -. ( V e. _V /\ E e. _V ) -> ( <. A , B >. e. dom ( V O E ) <-> <. A , B >. e. dom (/) ) )
52 dm0 
 |-  dom (/) = (/)
53 52 eleq2i 
 |-  ( <. A , B >. e. dom (/) <-> <. A , B >. e. (/) )
54 51 53 bitrdi 
 |-  ( -. ( V e. _V /\ E e. _V ) -> ( <. A , B >. e. dom ( V O E ) <-> <. A , B >. e. (/) ) )
55 noel 
 |-  -. <. A , B >. e. (/)
56 55 pm2.21i 
 |-  ( <. 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 ) ) ) )
57 54 56 biimtrdi 
 |-  ( -. ( 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 ) ) ) ) )
58 49 57 sylbir 
 |-  ( ( -. 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 
 |-  ( ( V e. _V /\ E e. _V ) <-> -. ( -. V e. _V \/ -. E e. _V ) )
60 id 
 |-  ( V e. _V -> V e. _V )
61 60 ancri 
 |-  ( V e. _V -> ( V e. _V /\ V e. _V ) )
62 61 adantr 
 |-  ( ( V e. _V /\ E e. _V ) -> ( V e. _V /\ V e. _V ) )
63 mpoexga 
 |-  ( ( V e. _V /\ V e. _V ) -> ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V )
64 62 63 syl 
 |-  ( ( V e. _V /\ E e. _V ) -> ( a e. V , b e. V |-> { <. f , p >. | ps } ) e. _V )
65 64 pm2.24d 
 |-  ( ( 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 ) ) ) ) ) )
66 59 65 sylbir 
 |-  ( -. ( -. 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 ) ) ) ) ) )
67 66 imp 
 |-  ( ( -. ( -. 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 ) ) ) ) )
68 58 67 jaoi3 
 |-  ( ( ( -. 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 ) ) ) ) )
69 48 68 sylbi 
 |-  ( ( -. 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 ) ) ) ) )
70 47 69 sylbi 
 |-  ( -. ( 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 ) ) ) ) )
71 46 70 pm2.61i 
 |-  ( <. 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 ) ) ) )
72 4 71 syl 
 |-  ( 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 ) ) ) )
73 72 pm2.43i 
 |-  ( 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 ) ) )