Metamath Proof Explorer

Theorem mptmpoopabbrd

Description: The operation value of a function value of a collection of ordered pairs of elements related in two ways. (Contributed by Alexander van Vekens, 8-Nov-2017) (Revised by AV, 15-Jan-2021) Add disjoint variable condition on D , f , h to remove hypotheses; avoid ax-rep . (Revised by SN, 7-Apr-2025)

Ref Expression
Hypotheses mptmpoopabbrd.g ⊢ φ → G ∈ W
mptmpoopabbrd.x ⊢ φ → X ∈ A ⁡ G
mptmpoopabbrd.y ⊢ φ → Y ∈ B ⁡ G
mptmpoopabbrd.1 ⊢ a = X ∧ b = Y → τ ↔ θ
mptmpoopabbrd.2 ⊢ g = G → χ ↔ τ
mptmpoopabbrd.m ⊢ M = g ∈ V ⟼ a ∈ A ⁡ g , b ∈ B ⁡ g ⟼ f h | χ ∧ f D ⁡ g h
Assertion mptmpoopabbrd ⊢ φ → X M ⁡ G Y = f h | θ ∧ f D ⁡ G h

Proof

Step Hyp Ref Expression
1 mptmpoopabbrd.g ⊢ φ → G ∈ W
2 mptmpoopabbrd.x ⊢ φ → X ∈ A ⁡ G
3 mptmpoopabbrd.y ⊢ φ → Y ∈ B ⁡ G
4 mptmpoopabbrd.1 ⊢ a = X ∧ b = Y → τ ↔ θ
5 mptmpoopabbrd.2 ⊢ g = G → χ ↔ τ
6 mptmpoopabbrd.m ⊢ M = g ∈ V ⟼ a ∈ A ⁡ g , b ∈ B ⁡ g ⟼ f h | χ ∧ f D ⁡ g h
7 fveq2 ⊢ g = G → A ⁡ g = A ⁡ G
8 fveq2 ⊢ g = G → B ⁡ g = B ⁡ G
9 fveq2 ⊢ g = G → D ⁡ g = D ⁡ G
10 9 breqd ⊢ g = G → f D ⁡ g h ↔ f D ⁡ G h
11 5 10 anbi12d ⊢ g = G → χ ∧ f D ⁡ g h ↔ τ ∧ f D ⁡ G h
12 11 opabbidv ⊢ g = G → f h | χ ∧ f D ⁡ g h = f h | τ ∧ f D ⁡ G h
13 7 8 12 mpoeq123dv ⊢ g = G → a ∈ A ⁡ g , b ∈ B ⁡ g ⟼ f h | χ ∧ f D ⁡ g h = a ∈ A ⁡ G , b ∈ B ⁡ G ⟼ f h | τ ∧ f D ⁡ G h
14 1 elexd ⊢ φ → G ∈ V
15 fvex ⊢ A ⁡ G ∈ V
16 fvex ⊢ B ⁡ G ∈ V
17 fvex ⊢ D ⁡ G ∈ V
18 17 pwex ⊢ 𝒫 D ⁡ G ∈ V
19 simpr ⊢ τ ∧ f D ⁡ G h → f D ⁡ G h
20 19 ssopab2i ⊢ f h | τ ∧ f D ⁡ G h ⊆ f h | f D ⁡ G h
21 opabss ⊢ f h | f D ⁡ G h ⊆ D ⁡ G
22 20 21 sstri ⊢ f h | τ ∧ f D ⁡ G h ⊆ D ⁡ G
23 17 22 elpwi2 ⊢ f h | τ ∧ f D ⁡ G h ∈ 𝒫 D ⁡ G
24 23 rgen2w ⊢ ∀ a ∈ A ⁡ G ∀ b ∈ B ⁡ G f h | τ ∧ f D ⁡ G h ∈ 𝒫 D ⁡ G
25 15 16 18 24 mpoexw ⊢ a ∈ A ⁡ G , b ∈ B ⁡ G ⟼ f h | τ ∧ f D ⁡ G h ∈ V
26 25 a1i ⊢ φ → a ∈ A ⁡ G , b ∈ B ⁡ G ⟼ f h | τ ∧ f D ⁡ G h ∈ V
27 6 13 14 26 fvmptd3 ⊢ φ → M ⁡ G = a ∈ A ⁡ G , b ∈ B ⁡ G ⟼ f h | τ ∧ f D ⁡ G h
28 27 oveqd ⊢ φ → X M ⁡ G Y = X a ∈ A ⁡ G , b ∈ B ⁡ G ⟼ f h | τ ∧ f D ⁡ G h Y
29 4 anbi1d ⊢ a = X ∧ b = Y → τ ∧ f D ⁡ G h ↔ θ ∧ f D ⁡ G h
30 29 opabbidv ⊢ a = X ∧ b = Y → f h | τ ∧ f D ⁡ G h = f h | θ ∧ f D ⁡ G h
31 eqid ⊢ a ∈ A ⁡ G , b ∈ B ⁡ G ⟼ f h | τ ∧ f D ⁡ G h = a ∈ A ⁡ G , b ∈ B ⁡ G ⟼ f h | τ ∧ f D ⁡ G h
32 ancom ⊢ θ ∧ f D ⁡ G h ↔ f D ⁡ G h ∧ θ
33 32 opabbii ⊢ f h | θ ∧ f D ⁡ G h = f h | f D ⁡ G h ∧ θ
34 opabresex2 ⊢ f h | f D ⁡ G h ∧ θ ∈ V
35 33 34 eqeltri ⊢ f h | θ ∧ f D ⁡ G h ∈ V
36 30 31 35 ovmpoa ⊢ X ∈ A ⁡ G ∧ Y ∈ B ⁡ G → X a ∈ A ⁡ G , b ∈ B ⁡ G ⟼ f h | τ ∧ f D ⁡ G h Y = f h | θ ∧ f D ⁡ G h
37 2 3 36 syl2anc ⊢ φ → X a ∈ A ⁡ G , b ∈ B ⁡ G ⟼ f h | τ ∧ f D ⁡ G h Y = f h | θ ∧ f D ⁡ G h
38 28 37 eqtrd ⊢ φ → X M ⁡ G Y = f h | θ ∧ f D ⁡ G h