Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Exploring Topology via Seifert and Threlfall
Equinumerosity of sets of relations and maps
fsovcnvfvd
Metamath Proof Explorer
Description: The value of the converse of ( A O B ) , where O is the
operator 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, evaluated at function F . (Contributed by RP , 27-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
fsovfvd.g
⊢ G = A O B
fsovcnvfvd.f
⊢ φ → F ∈ 𝒫 A B
Assertion
fsovcnvfvd
⊢ φ → G -1 ⁡ F = y ∈ A ⟼ x ∈ B | 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
fsovfvd.g
⊢ G = A O B
5
fsovcnvfvd.f
⊢ φ → F ∈ 𝒫 A B
6
eqid
⊢ B O A = B O A
7
1 2 3 4 6
fsovcnvd
⊢ φ → G -1 = B O A
8
7
fveq1d
⊢ φ → G -1 ⁡ F = B O A ⁡ F
9
1 3 2 6 5
fsovfvd
⊢ φ → B O A ⁡ F = y ∈ A ⟼ x ∈ B | y ∈ F ⁡ x
10
8 9
eqtrd
⊢ φ → G -1 ⁡ F = y ∈ A ⟼ x ∈ B | y ∈ F ⁡ x