Metamath Proof Explorer

Theorem fsovd

Description: Value of the operator, ( A O B ) , which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, A and B . (Contributed by RP, 25-Apr-2021)

Ref Expression
Hypotheses fsovd.fs ⊢ O = a ∈ V , b ∈ V ⟼ f ∈ 𝒫 b a ⟼ y ∈ b ⟼ x ∈ a | y ∈ f ⁡ x
fsovd.a ⊢ φ → A ∈ V
fsovd.b ⊢ φ → B ∈ W
Assertion fsovd ⊢ φ → A O B = f ∈ 𝒫 B A ⟼ y ∈ B ⟼ x ∈ A | y ∈ f ⁡ x

Proof

Step Hyp Ref Expression
1 fsovd.fs ⊢ O = a ∈ V , b ∈ V ⟼ f ∈ 𝒫 b a ⟼ y ∈ b ⟼ x ∈ a | y ∈ f ⁡ x
2 fsovd.a ⊢ φ → A ∈ V
3 fsovd.b ⊢ φ → B ∈ W
4 1 a1i ⊢ φ → O = a ∈ V , b ∈ V ⟼ f ∈ 𝒫 b a ⟼ y ∈ b ⟼ x ∈ a | y ∈ f ⁡ x
5 pweq ⊢ b = B → 𝒫 b = 𝒫 B
6 5 adantl ⊢ a = A ∧ b = B → 𝒫 b = 𝒫 B
7 simpl ⊢ a = A ∧ b = B → a = A
8 6 7 oveq12d ⊢ a = A ∧ b = B → 𝒫 b a = 𝒫 B A
9 simpr ⊢ a = A ∧ b = B → b = B
10 rabeq ⊢ a = A → x ∈ a | y ∈ f ⁡ x = x ∈ A | y ∈ f ⁡ x
11 10 adantr ⊢ a = A ∧ b = B → x ∈ a | y ∈ f ⁡ x = x ∈ A | y ∈ f ⁡ x
12 9 11 mpteq12dv ⊢ a = A ∧ b = B → y ∈ b ⟼ x ∈ a | y ∈ f ⁡ x = y ∈ B ⟼ x ∈ A | y ∈ f ⁡ x
13 8 12 mpteq12dv ⊢ a = A ∧ b = B → f ∈ 𝒫 b a ⟼ y ∈ b ⟼ x ∈ a | y ∈ f ⁡ x = f ∈ 𝒫 B A ⟼ y ∈ B ⟼ x ∈ A | y ∈ f ⁡ x
14 13 adantl ⊢ φ ∧ a = A ∧ b = B → f ∈ 𝒫 b a ⟼ y ∈ b ⟼ x ∈ a | y ∈ f ⁡ x = f ∈ 𝒫 B A ⟼ y ∈ B ⟼ x ∈ A | y ∈ f ⁡ x
15 2 elexd ⊢ φ → A ∈ V
16 3 elexd ⊢ φ → B ∈ V
17 ovex ⊢ 𝒫 B A ∈ V
18 17 mptex ⊢ f ∈ 𝒫 B A ⟼ y ∈ B ⟼ x ∈ A | y ∈ f ⁡ x ∈ V
19 18 a1i ⊢ φ → f ∈ 𝒫 B A ⟼ y ∈ B ⟼ x ∈ A | y ∈ f ⁡ x ∈ V
20 4 14 15 16 19 ovmpod ⊢ φ → A O B = f ∈ 𝒫 B A ⟼ y ∈ B ⟼ x ∈ A | y ∈ f ⁡ x