Metamath Proof Explorer

Theorem sprsymrelf

Description: The mapping F is a function from the subsets of the set of pairs over a fixed set V into the symmetric relations R on the fixed set V . (Contributed by AV, 19-Nov-2021)

Ref Expression
Hypotheses sprsymrelf.p ⊢ P = 𝒫 Pairs ⁡ V
sprsymrelf.r ⊢ R = r ∈ 𝒫 V × V | ∀ x ∈ V ∀ y ∈ V x r y ↔ y r x
sprsymrelf.f ⊢ F = p ∈ P ⟼ x y | ∃ c ∈ p c = x y
Assertion sprsymrelf ⊢ F : P ⟶ R

Proof

Step Hyp Ref Expression
1 sprsymrelf.p ⊢ P = 𝒫 Pairs ⁡ V
2 sprsymrelf.r ⊢ R = r ∈ 𝒫 V × V | ∀ x ∈ V ∀ y ∈ V x r y ↔ y r x
3 sprsymrelf.f ⊢ F = p ∈ P ⟼ x y | ∃ c ∈ p c = x y
4 sprsymrelfvlem ⊢ p ⊆ Pairs ⁡ V → x y | ∃ c ∈ p c = x y ∈ 𝒫 V × V
5 prcom ⊢ x y = y x
6 5 a1i ⊢ p ⊆ Pairs ⁡ V ∧ x ∈ V ∧ y ∈ V ∧ c ∈ p → x y = y x
7 6 eqeq2d ⊢ p ⊆ Pairs ⁡ V ∧ x ∈ V ∧ y ∈ V ∧ c ∈ p → c = x y ↔ c = y x
8 7 rexbidva ⊢ p ⊆ Pairs ⁡ V ∧ x ∈ V ∧ y ∈ V → ∃ c ∈ p c = x y ↔ ∃ c ∈ p c = y x
9 df-br ⊢ x x y | ∃ c ∈ p c = x y y ↔ x y ∈ x y | ∃ c ∈ p c = x y
10 opabidw ⊢ x y ∈ x y | ∃ c ∈ p c = x y ↔ ∃ c ∈ p c = x y
11 9 10 bitri ⊢ x x y | ∃ c ∈ p c = x y y ↔ ∃ c ∈ p c = x y
12 vex ⊢ y ∈ V
13 vex ⊢ x ∈ V
14 preq12 ⊢ a = y ∧ b = x → a b = y x
15 14 eqeq2d ⊢ a = y ∧ b = x → c = a b ↔ c = y x
16 15 rexbidv ⊢ a = y ∧ b = x → ∃ c ∈ p c = a b ↔ ∃ c ∈ p c = y x
17 preq12 ⊢ x = a ∧ y = b → x y = a b
18 17 eqeq2d ⊢ x = a ∧ y = b → c = x y ↔ c = a b
19 18 rexbidv ⊢ x = a ∧ y = b → ∃ c ∈ p c = x y ↔ ∃ c ∈ p c = a b
20 19 cbvopabv ⊢ x y | ∃ c ∈ p c = x y = a b | ∃ c ∈ p c = a b
21 12 13 16 20 braba ⊢ y x y | ∃ c ∈ p c = x y x ↔ ∃ c ∈ p c = y x
22 8 11 21 3bitr4g ⊢ p ⊆ Pairs ⁡ V ∧ x ∈ V ∧ y ∈ V → x x y | ∃ c ∈ p c = x y y ↔ y x y | ∃ c ∈ p c = x y x
23 22 ralrimivva ⊢ p ⊆ Pairs ⁡ V → ∀ x ∈ V ∀ y ∈ V x x y | ∃ c ∈ p c = x y y ↔ y x y | ∃ c ∈ p c = x y x
24 4 23 jca ⊢ p ⊆ Pairs ⁡ V → x y | ∃ c ∈ p c = x y ∈ 𝒫 V × V ∧ ∀ x ∈ V ∀ y ∈ V x x y | ∃ c ∈ p c = x y y ↔ y x y | ∃ c ∈ p c = x y x
25 1 eleq2i ⊢ p ∈ P ↔ p ∈ 𝒫 Pairs ⁡ V
26 vex ⊢ p ∈ V
27 26 elpw ⊢ p ∈ 𝒫 Pairs ⁡ V ↔ p ⊆ Pairs ⁡ V
28 25 27 bitri ⊢ p ∈ P ↔ p ⊆ Pairs ⁡ V
29 nfopab1 ⊢ Ⅎ _ x x y | ∃ c ∈ p c = x y
30 29 nfeq2 ⊢ Ⅎ x r = x y | ∃ c ∈ p c = x y
31 nfopab2 ⊢ Ⅎ _ y x y | ∃ c ∈ p c = x y
32 31 nfeq2 ⊢ Ⅎ y r = x y | ∃ c ∈ p c = x y
33 breq ⊢ r = x y | ∃ c ∈ p c = x y → x r y ↔ x x y | ∃ c ∈ p c = x y y
34 breq ⊢ r = x y | ∃ c ∈ p c = x y → y r x ↔ y x y | ∃ c ∈ p c = x y x
35 33 34 bibi12d ⊢ r = x y | ∃ c ∈ p c = x y → x r y ↔ y r x ↔ x x y | ∃ c ∈ p c = x y y ↔ y x y | ∃ c ∈ p c = x y x
36 32 35 ralbid ⊢ r = x y | ∃ c ∈ p c = x y → ∀ y ∈ V x r y ↔ y r x ↔ ∀ y ∈ V x x y | ∃ c ∈ p c = x y y ↔ y x y | ∃ c ∈ p c = x y x
37 30 36 ralbid ⊢ r = x y | ∃ c ∈ p c = x y → ∀ x ∈ V ∀ y ∈ V x r y ↔ y r x ↔ ∀ x ∈ V ∀ y ∈ V x x y | ∃ c ∈ p c = x y y ↔ y x y | ∃ c ∈ p c = x y x
38 37 elrab ⊢ x y | ∃ c ∈ p c = x y ∈ r ∈ 𝒫 V × V | ∀ x ∈ V ∀ y ∈ V x r y ↔ y r x ↔ x y | ∃ c ∈ p c = x y ∈ 𝒫 V × V ∧ ∀ x ∈ V ∀ y ∈ V x x y | ∃ c ∈ p c = x y y ↔ y x y | ∃ c ∈ p c = x y x
39 24 28 38 3imtr4i ⊢ p ∈ P → x y | ∃ c ∈ p c = x y ∈ r ∈ 𝒫 V × V | ∀ x ∈ V ∀ y ∈ V x r y ↔ y r x
40 39 2 eleqtrrdi ⊢ p ∈ P → x y | ∃ c ∈ p c = x y ∈ R
41 3 40 fmpti ⊢ F : P ⟶ R