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∈V,e∈V⟼a∈v,b∈v⟼fp|φ
bropopvvv.p ⊢v=V∧e=E→φ↔ψ
bropopvvv.oo ⊢V∈V∧E∈V∧A∈V∧B∈V→AVOEB=fp|θ
Assertion bropopvvv ⊢FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V

Proof

Step Hyp Ref Expression
1 bropopvvv.o ⊢O=v∈V,e∈V⟼a∈v,b∈v⟼fp|φ
2 bropopvvv.p ⊢v=V∧e=E→φ↔ψ
3 bropopvvv.oo ⊢V∈V∧E∈V∧A∈V∧B∈V→AVOEB=fp|θ
4 brovpreldm ⊢FAVOEBP→AB∈dom⁡VOE
5 simpl ⊢v=V∧e=E→v=V
6 2 opabbidv ⊢v=V∧e=E→fp|φ=fp|ψ
7 5 5 6 mpoeq123dv ⊢v=V∧e=E→a∈v,b∈v⟼fp|φ=a∈V,b∈V⟼fp|ψ
8 7 1 ovmpoga ⊢V∈V∧E∈V∧a∈V,b∈V⟼fp|ψ∈V→VOE=a∈V,b∈V⟼fp|ψ
9 8 dmeqd ⊢V∈V∧E∈V∧a∈V,b∈V⟼fp|ψ∈V→dom⁡VOE=dom⁡a∈V,b∈V⟼fp|ψ
10 9 eleq2d ⊢V∈V∧E∈V∧a∈V,b∈V⟼fp|ψ∈V→AB∈dom⁡VOE↔AB∈dom⁡a∈V,b∈V⟼fp|ψ
11 dmoprabss ⊢dom⁡abc|a∈V∧b∈V∧c=fp|ψ⊆V×V
12 11 sseli ⊢AB∈dom⁡abc|a∈V∧b∈V∧c=fp|ψ→AB∈V×V
13 opelxp ⊢AB∈V×V↔A∈V∧B∈V
14 df-br ⊢FAVOEBP↔FP∈AVOEB
15 ne0i ⊢FP∈AVOEB→AVOEB≠∅
16 3 breqd ⊢V∈V∧E∈V∧A∈V∧B∈V→FAVOEBP↔Ffp|θP
17 brabv ⊢Ffp|θP→F∈V∧P∈V
18 17 anim2i ⊢V∈V∧E∈V∧Ffp|θP→V∈V∧E∈V∧F∈V∧P∈V
19 18 ex ⊢V∈V∧E∈V→Ffp|θP→V∈V∧E∈V∧F∈V∧P∈V
20 19 adantr ⊢V∈V∧E∈V∧A∈V∧B∈V→Ffp|θP→V∈V∧E∈V∧F∈V∧P∈V
21 16 20 sylbid ⊢V∈V∧E∈V∧A∈V∧B∈V→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V
22 21 ex ⊢V∈V∧E∈V→A∈V∧B∈V→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V
23 22 com23 ⊢V∈V∧E∈V→FAVOEBP→A∈V∧B∈V→V∈V∧E∈V∧F∈V∧P∈V
24 23 a1d ⊢V∈V∧E∈V→AVOEB≠∅→FAVOEBP→A∈V∧B∈V→V∈V∧E∈V∧F∈V∧P∈V
25 1 mpondm0 ⊢¬V∈V∧E∈V→VOE=∅
26 df-ov ⊢AVOEB=VOE⁡AB
27 fveq1 ⊢VOE=∅→VOE⁡AB=∅⁡AB
28 26 27 eqtrid ⊢VOE=∅→AVOEB=∅⁡AB
29 0fv ⊢∅⁡AB=∅
30 28 29 eqtrdi ⊢VOE=∅→AVOEB=∅
31 eqneqall ⊢AVOEB=∅→AVOEB≠∅→FAVOEBP→A∈V∧B∈V→V∈V∧E∈V∧F∈V∧P∈V
32 25 30 31 3syl ⊢¬V∈V∧E∈V→AVOEB≠∅→FAVOEBP→A∈V∧B∈V→V∈V∧E∈V∧F∈V∧P∈V
33 24 32 pm2.61i ⊢AVOEB≠∅→FAVOEBP→A∈V∧B∈V→V∈V∧E∈V∧F∈V∧P∈V
34 15 33 syl ⊢FP∈AVOEB→FAVOEBP→A∈V∧B∈V→V∈V∧E∈V∧F∈V∧P∈V
35 14 34 sylbi ⊢FAVOEBP→FAVOEBP→A∈V∧B∈V→V∈V∧E∈V∧F∈V∧P∈V
36 35 pm2.43i ⊢FAVOEBP→A∈V∧B∈V→V∈V∧E∈V∧F∈V∧P∈V
37 36 com12 ⊢A∈V∧B∈V→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V
38 37 anc2ri ⊢A∈V∧B∈V→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
39 df-3an ⊢V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V↔V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
40 38 39 imbitrrdi ⊢A∈V∧B∈V→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
41 13 40 sylbi ⊢AB∈V×V→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
42 12 41 syl ⊢AB∈dom⁡abc|a∈V∧b∈V∧c=fp|ψ→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
43 df-mpo ⊢a∈V,b∈V⟼fp|ψ=abc|a∈V∧b∈V∧c=fp|ψ
44 43 dmeqi ⊢dom⁡a∈V,b∈V⟼fp|ψ=dom⁡abc|a∈V∧b∈V∧c=fp|ψ
45 42 44 eleq2s ⊢AB∈dom⁡a∈V,b∈V⟼fp|ψ→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
46 10 45 syl6bi ⊢V∈V∧E∈V∧a∈V,b∈V⟼fp|ψ∈V→AB∈dom⁡VOE→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
47 3ianor ⊢¬V∈V∧E∈V∧a∈V,b∈V⟼fp|ψ∈V↔¬V∈V∨¬E∈V∨¬a∈V,b∈V⟼fp|ψ∈V
48 df-3or ⊢¬V∈V∨¬E∈V∨¬a∈V,b∈V⟼fp|ψ∈V↔¬V∈V∨¬E∈V∨¬a∈V,b∈V⟼fp|ψ∈V
49 ianor ⊢¬V∈V∧E∈V↔¬V∈V∨¬E∈V
50 25 dmeqd ⊢¬V∈V∧E∈V→dom⁡VOE=dom⁡∅
51 50 eleq2d ⊢¬V∈V∧E∈V→AB∈dom⁡VOE↔AB∈dom⁡∅
52 dm0 ⊢dom⁡∅=∅
53 52 eleq2i ⊢AB∈dom⁡∅↔AB∈∅
54 51 53 bitrdi ⊢¬V∈V∧E∈V→AB∈dom⁡VOE↔AB∈∅
55 noel ⊢¬AB∈∅
56 55 pm2.21i ⊢AB∈∅→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
57 54 56 syl6bi ⊢¬V∈V∧E∈V→AB∈dom⁡VOE→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
58 49 57 sylbir ⊢¬V∈V∨¬E∈V→AB∈dom⁡VOE→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
59 anor ⊢V∈V∧E∈V↔¬¬V∈V∨¬E∈V
60 id ⊢V∈V→V∈V
61 60 ancri ⊢V∈V→V∈V∧V∈V
62 61 adantr ⊢V∈V∧E∈V→V∈V∧V∈V
63 mpoexga ⊢V∈V∧V∈V→a∈V,b∈V⟼fp|ψ∈V
64 62 63 syl ⊢V∈V∧E∈V→a∈V,b∈V⟼fp|ψ∈V
65 64 pm2.24d ⊢V∈V∧E∈V→¬a∈V,b∈V⟼fp|ψ∈V→AB∈dom⁡VOE→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
66 59 65 sylbir ⊢¬¬V∈V∨¬E∈V→¬a∈V,b∈V⟼fp|ψ∈V→AB∈dom⁡VOE→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
67 66 imp ⊢¬¬V∈V∨¬E∈V∧¬a∈V,b∈V⟼fp|ψ∈V→AB∈dom⁡VOE→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
68 58 67 jaoi3 ⊢¬V∈V∨¬E∈V∨¬a∈V,b∈V⟼fp|ψ∈V→AB∈dom⁡VOE→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
69 48 68 sylbi ⊢¬V∈V∨¬E∈V∨¬a∈V,b∈V⟼fp|ψ∈V→AB∈dom⁡VOE→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
70 47 69 sylbi ⊢¬V∈V∧E∈V∧a∈V,b∈V⟼fp|ψ∈V→AB∈dom⁡VOE→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
71 46 70 pm2.61i ⊢AB∈dom⁡VOE→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
72 4 71 syl ⊢FAVOEBP→FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V
73 72 pm2.43i ⊢FAVOEBP→V∈V∧E∈V∧F∈V∧P∈V∧A∈V∧B∈V