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 ⟼ f p | φ
bropopvvv.p ⊢ v = V ∧ e = E → φ ↔ ψ
bropopvvv.oo ⊢ V ∈ V ∧ E ∈ V ∧ A ∈ V ∧ B ∈ V → A V O E B = f p | θ
Assertion bropopvvv ⊢ F A V O E B P → 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 ⟼ f p | φ
2 bropopvvv.p ⊢ v = V ∧ e = E → φ ↔ ψ
3 bropopvvv.oo ⊢ V ∈ V ∧ E ∈ V ∧ A ∈ V ∧ B ∈ V → A V O E B = f p | θ
4 brovpreldm ⊢ F A V O E B P → A B ∈ dom ⁡ V O E
5 simpl ⊢ v = V ∧ e = E → v = V
6 2 opabbidv ⊢ v = V ∧ e = E → f p | φ = f p | ψ
7 5 5 6 mpoeq123dv ⊢ v = V ∧ e = E → a ∈ v , b ∈ v ⟼ f p | φ = a ∈ V , b ∈ V ⟼ f p | ψ
8 7 1 ovmpoga ⊢ V ∈ V ∧ E ∈ V ∧ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V → V O E = a ∈ V , b ∈ V ⟼ f p | ψ
9 8 dmeqd ⊢ V ∈ V ∧ E ∈ V ∧ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V → dom ⁡ V O E = dom ⁡ a ∈ V , b ∈ V ⟼ f p | ψ
10 9 eleq2d ⊢ V ∈ V ∧ E ∈ V ∧ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V → A B ∈ dom ⁡ V O E ↔ A B ∈ dom ⁡ a ∈ V , b ∈ V ⟼ f p | ψ
11 dmoprabss ⊢ dom ⁡ a b c | a ∈ V ∧ b ∈ V ∧ c = f p | ψ ⊆ V × V
12 11 sseli ⊢ A B ∈ dom ⁡ a b c | a ∈ V ∧ b ∈ V ∧ c = f p | ψ → A B ∈ V × V
13 opelxp ⊢ A B ∈ V × V ↔ A ∈ V ∧ B ∈ V
14 df-br ⊢ F A V O E B P ↔ F P ∈ A V O E B
15 ne0i ⊢ F P ∈ A V O E B → A V O E B ≠ ∅
16 3 breqd ⊢ V ∈ V ∧ E ∈ V ∧ A ∈ V ∧ B ∈ V → F A V O E B P ↔ F f p | θ P
17 brabv ⊢ F f p | θ P → F ∈ V ∧ P ∈ V
18 17 anim2i ⊢ V ∈ V ∧ E ∈ V ∧ F f p | θ P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
19 18 ex ⊢ V ∈ V ∧ E ∈ V → F f p | θ P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
20 19 adantr ⊢ V ∈ V ∧ E ∈ V ∧ A ∈ V ∧ B ∈ V → F f p | θ P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
21 16 20 sylbid ⊢ V ∈ V ∧ E ∈ V ∧ A ∈ V ∧ B ∈ V → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
22 21 ex ⊢ V ∈ V ∧ E ∈ V → A ∈ V ∧ B ∈ V → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
23 22 com23 ⊢ V ∈ V ∧ E ∈ V → F A V O E B P → A ∈ V ∧ B ∈ V → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
24 23 a1d ⊢ V ∈ V ∧ E ∈ V → A V O E B ≠ ∅ → F A V O E B P → A ∈ V ∧ B ∈ V → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
25 1 mpondm0 ⊢ ¬ V ∈ V ∧ 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 ∈ V ∧ B ∈ V → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
32 25 30 31 3syl ⊢ ¬ V ∈ V ∧ E ∈ V → A V O E B ≠ ∅ → F A V O E B P → A ∈ V ∧ B ∈ V → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
33 24 32 pm2.61i ⊢ A V O E B ≠ ∅ → F A V O E B P → A ∈ V ∧ B ∈ V → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
34 15 33 syl ⊢ F P ∈ A V O E B → F A V O E B P → A ∈ V ∧ B ∈ V → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
35 14 34 sylbi ⊢ F A V O E B P → F A V O E B P → A ∈ V ∧ B ∈ V → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
36 35 pm2.43i ⊢ F A V O E B P → A ∈ V ∧ B ∈ V → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
37 36 com12 ⊢ A ∈ V ∧ B ∈ V → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V
38 37 anc2ri ⊢ A ∈ V ∧ B ∈ V → F A V O E B P → 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 → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
41 13 40 sylbi ⊢ A B ∈ V × V → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
42 12 41 syl ⊢ A B ∈ dom ⁡ a b c | a ∈ V ∧ b ∈ V ∧ c = f p | ψ → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
43 df-mpo ⊢ a ∈ V , b ∈ V ⟼ f p | ψ = a b c | a ∈ V ∧ b ∈ V ∧ c = f p | ψ
44 43 dmeqi ⊢ dom ⁡ a ∈ V , b ∈ V ⟼ f p | ψ = dom ⁡ a b c | a ∈ V ∧ b ∈ V ∧ c = f p | ψ
45 42 44 eleq2s ⊢ A B ∈ dom ⁡ a ∈ V , b ∈ V ⟼ f p | ψ → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
46 10 45 biimtrdi ⊢ V ∈ V ∧ E ∈ V ∧ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V → A B ∈ dom ⁡ V O E → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
47 3ianor ⊢ ¬ V ∈ V ∧ E ∈ V ∧ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V ↔ ¬ V ∈ V ∨ ¬ E ∈ V ∨ ¬ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V
48 df-3or ⊢ ¬ V ∈ V ∨ ¬ E ∈ V ∨ ¬ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V ↔ ¬ V ∈ V ∨ ¬ E ∈ V ∨ ¬ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V
49 ianor ⊢ ¬ V ∈ V ∧ E ∈ V ↔ ¬ V ∈ V ∨ ¬ E ∈ V
50 25 dmeqd ⊢ ¬ V ∈ V ∧ E ∈ V → dom ⁡ V O E = dom ⁡ ∅
51 50 eleq2d ⊢ ¬ V ∈ V ∧ E ∈ V → A B ∈ dom ⁡ V O E ↔ A B ∈ dom ⁡ ∅
52 dm0 ⊢ dom ⁡ ∅ = ∅
53 52 eleq2i ⊢ A B ∈ dom ⁡ ∅ ↔ A B ∈ ∅
54 51 53 bitrdi ⊢ ¬ V ∈ V ∧ E ∈ V → A B ∈ dom ⁡ V O E ↔ A B ∈ ∅
55 noel ⊢ ¬ A B ∈ ∅
56 55 pm2.21i ⊢ A B ∈ ∅ → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
57 54 56 biimtrdi ⊢ ¬ V ∈ V ∧ E ∈ V → A B ∈ dom ⁡ V O E → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
58 49 57 sylbir ⊢ ¬ V ∈ V ∨ ¬ E ∈ V → A B ∈ dom ⁡ V O E → F A V O E B P → 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 ⟼ f p | ψ ∈ V
64 62 63 syl ⊢ V ∈ V ∧ E ∈ V → a ∈ V , b ∈ V ⟼ f p | ψ ∈ V
65 64 pm2.24d ⊢ V ∈ V ∧ E ∈ V → ¬ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V → A B ∈ dom ⁡ V O E → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
66 59 65 sylbir ⊢ ¬ ¬ V ∈ V ∨ ¬ E ∈ V → ¬ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V → A B ∈ dom ⁡ V O E → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
67 66 imp ⊢ ¬ ¬ V ∈ V ∨ ¬ E ∈ V ∧ ¬ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V → A B ∈ dom ⁡ V O E → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
68 58 67 jaoi3 ⊢ ¬ V ∈ V ∨ ¬ E ∈ V ∨ ¬ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V → A B ∈ dom ⁡ V O E → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
69 48 68 sylbi ⊢ ¬ V ∈ V ∨ ¬ E ∈ V ∨ ¬ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V → A B ∈ dom ⁡ V O E → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
70 47 69 sylbi ⊢ ¬ V ∈ V ∧ E ∈ V ∧ a ∈ V , b ∈ V ⟼ f p | ψ ∈ V → A B ∈ dom ⁡ V O E → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
71 46 70 pm2.61i ⊢ A B ∈ dom ⁡ V O E → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
72 4 71 syl ⊢ F A V O E B P → F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V
73 72 pm2.43i ⊢ F A V O E B P → V ∈ V ∧ E ∈ V ∧ F ∈ V ∧ P ∈ V ∧ A ∈ V ∧ B ∈ V