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 𝑂 = ( 𝑎𝑈 ↦ ( 𝑏𝑉 , 𝑐𝑊 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜑 } ) )
bropfvvvv.oo ( ( 𝐴𝑈𝐵𝑆𝐶𝑇 ) → ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜃 } )
bropfvvvv.s ( 𝑎 = 𝐴𝑉 = 𝑆 )
bropfvvvv.t ( 𝑎 = 𝐴𝑊 = 𝑇 )
bropfvvvv.p ( 𝑎 = 𝐴 → ( 𝜑𝜓 ) )
Assertion bropfvvvv ( ( 𝑆𝑋𝑇𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )

Proof

Step Hyp Ref Expression
1 bropfvvvv.o 𝑂 = ( 𝑎𝑈 ↦ ( 𝑏𝑉 , 𝑐𝑊 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜑 } ) )
2 bropfvvvv.oo ( ( 𝐴𝑈𝐵𝑆𝐶𝑇 ) → ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜃 } )
3 bropfvvvv.s ( 𝑎 = 𝐴𝑉 = 𝑆 )
4 bropfvvvv.t ( 𝑎 = 𝐴𝑊 = 𝑇 )
5 bropfvvvv.p ( 𝑎 = 𝐴 → ( 𝜑𝜓 ) )
6 brovpreldm ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) )
7 5 opabbidv ( 𝑎 = 𝐴 → { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜑 } = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } )
8 3 4 7 mpoeq123dv ( 𝑎 = 𝐴 → ( 𝑏𝑉 , 𝑐𝑊 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜑 } ) = ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) )
9 8 1 fvmptg ( ( 𝐴𝑈 ∧ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( 𝑂𝐴 ) = ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) )
10 9 dmeqd ( ( 𝐴𝑈 ∧ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → dom ( 𝑂𝐴 ) = dom ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) )
11 10 eleq2d ( ( 𝐴𝑈 ∧ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ) )
12 dmoprabss dom { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑏𝑆𝑐𝑇 ) ∧ 𝑧 = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) } ⊆ ( 𝑆 × 𝑇 )
13 12 sseli ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑏𝑆𝑐𝑇 ) ∧ 𝑧 = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) } → ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑆 × 𝑇 ) )
14 1 2 bropfvvvvlem ( ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑆 × 𝑇 ) ∧ 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 ) → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) )
15 14 ex ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑆 × 𝑇 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
16 13 15 syl ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑏𝑆𝑐𝑇 ) ∧ 𝑧 = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) } → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
17 df-mpo ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) = { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑏𝑆𝑐𝑇 ) ∧ 𝑧 = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) }
18 17 dmeqi dom ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) = dom { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑏𝑆𝑐𝑇 ) ∧ 𝑧 = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) }
19 16 18 eleq2s ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
20 11 19 syl6bi ( ( 𝐴𝑈 ∧ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) )
21 20 com23 ( ( 𝐴𝑈 ∧ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) )
22 21 a1d ( ( 𝐴𝑈 ∧ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆𝑋𝑇𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
23 ianor ( ¬ ( 𝐴𝑈 ∧ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) ↔ ( ¬ 𝐴𝑈 ∨ ¬ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) )
24 1 fvmptndm ( ¬ 𝐴𝑈 → ( 𝑂𝐴 ) = ∅ )
25 24 dmeqd ( ¬ 𝐴𝑈 → dom ( 𝑂𝐴 ) = dom ∅ )
26 25 eleq2d ( ¬ 𝐴𝑈 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ∅ ) )
27 dm0 dom ∅ = ∅
28 27 eleq2i ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ∅ ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ ∅ )
29 26 28 bitrdi ( ¬ 𝐴𝑈 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ ∅ ) )
30 noel ¬ ⟨ 𝐵 , 𝐶 ⟩ ∈ ∅
31 30 pm2.21i ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ∅ → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
32 29 31 syl6bi ( ¬ 𝐴𝑈 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) )
33 32 a1d ( ¬ 𝐴𝑈 → ( ( 𝑆𝑋𝑇𝑌 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
34 notnotb ( 𝐴𝑈 ↔ ¬ ¬ 𝐴𝑈 )
35 elex ( 𝑆𝑋𝑆 ∈ V )
36 elex ( 𝑇𝑌𝑇 ∈ V )
37 35 36 anim12i ( ( 𝑆𝑋𝑇𝑌 ) → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) )
38 37 adantl ( ( 𝐴𝑈 ∧ ( 𝑆𝑋𝑇𝑌 ) ) → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) )
39 mpoexga ( ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) → ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V )
40 38 39 syl ( ( 𝐴𝑈 ∧ ( 𝑆𝑋𝑇𝑌 ) ) → ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V )
41 40 pm2.24d ( ( 𝐴𝑈 ∧ ( 𝑆𝑋𝑇𝑌 ) ) → ( ¬ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
42 41 ex ( 𝐴𝑈 → ( ( 𝑆𝑋𝑇𝑌 ) → ( ¬ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) )
43 42 com23 ( 𝐴𝑈 → ( ¬ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V → ( ( 𝑆𝑋𝑇𝑌 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) )
44 34 43 sylbir ( ¬ ¬ 𝐴𝑈 → ( ¬ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V → ( ( 𝑆𝑋𝑇𝑌 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) )
45 44 imp ( ( ¬ ¬ 𝐴𝑈 ∧ ¬ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆𝑋𝑇𝑌 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
46 33 45 jaoi3 ( ( ¬ 𝐴𝑈 ∨ ¬ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆𝑋𝑇𝑌 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
47 23 46 sylbi ( ¬ ( 𝐴𝑈 ∧ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆𝑋𝑇𝑌 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
48 47 com34 ( ¬ ( 𝐴𝑈 ∧ ( 𝑏𝑆 , 𝑐𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆𝑋𝑇𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
49 22 48 pm2.61i ( ( 𝑆𝑋𝑇𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂𝐴 ) → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) )
50 6 49 mpdi ( ( 𝑆𝑋𝑇𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂𝐴 ) 𝐶 ) 𝐸 → ( 𝐴𝑈 ∧ ( 𝐵𝑆𝐶𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )