Metamath Proof Explorer


Theorem bropfvvvv

Description: If a binary relation holds for the result of an operation which is a function value, the involved classes are sets. (Contributed by AV, 31-Dec-2020) (Revised by AV, 16-Jan-2021)

Ref Expression
Hypotheses bropfvvvv.o O = a U b V , c W d e | φ
bropfvvvv.oo A U B S C T B O A C = d e | θ
bropfvvvv.s a = A V = S
bropfvvvv.t a = A W = T
bropfvvvv.p a = A φ ψ
Assertion bropfvvvv S X T Y D B O A C E A U B S C T D V E V

Proof

Step Hyp Ref Expression
1 bropfvvvv.o O = a U b V , c W d e | φ
2 bropfvvvv.oo A U B S C T B O A C = d e | θ
3 bropfvvvv.s a = A V = S
4 bropfvvvv.t a = A W = T
5 bropfvvvv.p a = A φ ψ
6 brovpreldm D B O A C E B C dom O A
7 5 opabbidv a = A d e | φ = d e | ψ
8 3 4 7 mpoeq123dv a = A b V , c W d e | φ = b S , c T d e | ψ
9 8 1 fvmptg A U b S , c T d e | ψ V O A = b S , c T d e | ψ
10 9 dmeqd A U b S , c T d e | ψ V dom O A = dom b S , c T d e | ψ
11 10 eleq2d A U b S , c T d e | ψ V B C dom O A B C dom b S , c T d e | ψ
12 dmoprabss dom b c z | b S c T z = d e | ψ S × T
13 12 sseli B C dom b c z | b S c T z = d e | ψ B C S × T
14 1 2 bropfvvvvlem B C S × T D B O A C E A U B S C T D V E V
15 14 ex B C S × T D B O A C E A U B S C T D V E V
16 13 15 syl B C dom b c z | b S c T z = d e | ψ D B O A C E A U B S C T D V E V
17 df-mpo b S , c T d e | ψ = b c z | b S c T z = d e | ψ
18 17 dmeqi dom b S , c T d e | ψ = dom b c z | b S c T z = d e | ψ
19 16 18 eleq2s B C dom b S , c T d e | ψ D B O A C E A U B S C T D V E V
20 11 19 syl6bi A U b S , c T d e | ψ V B C dom O A D B O A C E A U B S C T D V E V
21 20 com23 A U b S , c T d e | ψ V D B O A C E B C dom O A A U B S C T D V E V
22 21 a1d A U b S , c T d e | ψ V S X T Y D B O A C E B C dom O A A U B S C T D V E V
23 ianor ¬ A U b S , c T d e | ψ V ¬ A U ¬ b S , c T d e | ψ V
24 1 fvmptndm ¬ A U O A =
25 24 dmeqd ¬ A U dom O A = dom
26 25 eleq2d ¬ A U B C dom O A B C dom
27 dm0 dom =
28 27 eleq2i B C dom B C
29 26 28 bitrdi ¬ A U B C dom O A B C
30 noel ¬ B C
31 30 pm2.21i B C D B O A C E A U B S C T D V E V
32 29 31 syl6bi ¬ A U B C dom O A D B O A C E A U B S C T D V E V
33 32 a1d ¬ A U S X T Y B C dom O A D B O A C E A U B S C T D V E V
34 notnotb A U ¬ ¬ A U
35 elex S X S V
36 elex T Y T V
37 35 36 anim12i S X T Y S V T V
38 37 adantl A U S X T Y S V T V
39 mpoexga S V T V b S , c T d e | ψ V
40 38 39 syl A U S X T Y b S , c T d e | ψ V
41 40 pm2.24d A U S X T Y ¬ b S , c T d e | ψ V B C dom O A D B O A C E A U B S C T D V E V
42 41 ex A U S X T Y ¬ b S , c T d e | ψ V B C dom O A D B O A C E A U B S C T D V E V
43 42 com23 A U ¬ b S , c T d e | ψ V S X T Y B C dom O A D B O A C E A U B S C T D V E V
44 34 43 sylbir ¬ ¬ A U ¬ b S , c T d e | ψ V S X T Y B C dom O A D B O A C E A U B S C T D V E V
45 44 imp ¬ ¬ A U ¬ b S , c T d e | ψ V S X T Y B C dom O A D B O A C E A U B S C T D V E V
46 33 45 jaoi3 ¬ A U ¬ b S , c T d e | ψ V S X T Y B C dom O A D B O A C E A U B S C T D V E V
47 23 46 sylbi ¬ A U b S , c T d e | ψ V S X T Y B C dom O A D B O A C E A U B S C T D V E V
48 47 com34 ¬ A U b S , c T d e | ψ V S X T Y D B O A C E B C dom O A A U B S C T D V E V
49 22 48 pm2.61i S X T Y D B O A C E B C dom O A A U B S C T D V E V
50 6 49 mpdi S X T Y D B O A C E A U B S C T D V E V