Metamath Proof Explorer

Theorem sprsymrelfo

Description: The mapping F is a function from the subsets of the set of pairs over a fixed set V onto the symmetric relations R on the fixed set V . (Contributed by AV, 23-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 sprsymrelfo ⊢ V ∈ W → F : P ⟶ onto 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 1 2 3 sprsymrelf ⊢ F : P ⟶ R
5 4 a1i ⊢ V ∈ W → F : P ⟶ R
6 breq ⊢ r = t → x r y ↔ x t y
7 breq ⊢ r = t → y r x ↔ y t x
8 6 7 bibi12d ⊢ r = t → x r y ↔ y r x ↔ x t y ↔ y t x
9 8 2ralbidv ⊢ r = t → ∀ x ∈ V ∀ y ∈ V x r y ↔ y r x ↔ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x
10 9 2 elrab2 ⊢ t ∈ R ↔ t ∈ 𝒫 V × V ∧ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x
11 eqid ⊢ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b = q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b
12 11 sprsymrelfolem1 ⊢ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b ∈ 𝒫 Pairs ⁡ V
13 12 1 eleqtrri ⊢ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b ∈ P
14 13 a1i ⊢ t ∈ 𝒫 V × V ∧ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x ∧ V ∈ W → q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b ∈ P
15 rexeq ⊢ f = q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b → ∃ c ∈ f c = x y ↔ ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
16 15 opabbidv ⊢ f = q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b → x y | ∃ c ∈ f c = x y = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
17 16 eqeq2d ⊢ f = q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b → t = x y | ∃ c ∈ f c = x y ↔ t = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
18 17 adantl ⊢ t ∈ 𝒫 V × V ∧ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x ∧ V ∈ W ∧ f = q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b → t = x y | ∃ c ∈ f c = x y ↔ t = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
19 velpw ⊢ t ∈ 𝒫 V × V ↔ t ⊆ V × V
20 xpss ⊢ V × V ⊆ V × V
21 sstr2 ⊢ t ⊆ V × V → V × V ⊆ V × V → t ⊆ V × V
22 20 21 mpi ⊢ t ⊆ V × V → t ⊆ V × V
23 df-rel ⊢ Rel ⁡ t ↔ t ⊆ V × V
24 22 23 sylibr ⊢ t ⊆ V × V → Rel ⁡ t
25 24 adantl ⊢ V ∈ W ∧ t ⊆ V × V → Rel ⁡ t
26 dfrel4v ⊢ Rel ⁡ t ↔ t = x y | x t y
27 nfv ⊢ Ⅎ x V ∈ W ∧ t ⊆ V × V
28 nfra1 ⊢ Ⅎ x ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x
29 27 28 nfan ⊢ Ⅎ x V ∈ W ∧ t ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x
30 nfv ⊢ Ⅎ y V ∈ W ∧ t ⊆ V × V
31 nfra2w ⊢ Ⅎ y ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x
32 30 31 nfan ⊢ Ⅎ y V ∈ W ∧ t ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x
33 11 sprsymrelfolem2 ⊢ V ∈ W ∧ t ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x → x t y ↔ ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
34 33 3expa ⊢ V ∈ W ∧ t ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x → x t y ↔ ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
35 29 32 34 opabbid ⊢ V ∈ W ∧ t ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x → x y | x t y = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
36 35 eqeq2d ⊢ V ∈ W ∧ t ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x → t = x y | x t y ↔ t = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
37 36 biimpd ⊢ V ∈ W ∧ t ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x → t = x y | x t y → t = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
38 37 ex ⊢ V ∈ W ∧ t ⊆ V × V → ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x → t = x y | x t y → t = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
39 38 com23 ⊢ V ∈ W ∧ t ⊆ V × V → t = x y | x t y → ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x → t = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
40 26 39 biimtrid ⊢ V ∈ W ∧ t ⊆ V × V → Rel ⁡ t → ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x → t = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
41 25 40 mpd ⊢ V ∈ W ∧ t ⊆ V × V → ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x → t = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
42 41 expcom ⊢ t ⊆ V × V → V ∈ W → ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x → t = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
43 42 com23 ⊢ t ⊆ V × V → ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x → V ∈ W → t = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
44 19 43 sylbi ⊢ t ∈ 𝒫 V × V → ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x → V ∈ W → t = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
45 44 imp31 ⊢ t ∈ 𝒫 V × V ∧ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x ∧ V ∈ W → t = x y | ∃ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a t b c = x y
46 14 18 45 rspcedvd ⊢ t ∈ 𝒫 V × V ∧ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x ∧ V ∈ W → ∃ f ∈ P t = x y | ∃ c ∈ f c = x y
47 46 ex ⊢ t ∈ 𝒫 V × V ∧ ∀ x ∈ V ∀ y ∈ V x t y ↔ y t x → V ∈ W → ∃ f ∈ P t = x y | ∃ c ∈ f c = x y
48 10 47 sylbi ⊢ t ∈ R → V ∈ W → ∃ f ∈ P t = x y | ∃ c ∈ f c = x y
49 48 impcom ⊢ V ∈ W ∧ t ∈ R → ∃ f ∈ P t = x y | ∃ c ∈ f c = x y
50 1 2 3 sprsymrelfv ⊢ f ∈ P → F ⁡ f = x y | ∃ c ∈ f c = x y
51 50 adantl ⊢ V ∈ W ∧ t ∈ R ∧ f ∈ P → F ⁡ f = x y | ∃ c ∈ f c = x y
52 51 eqeq2d ⊢ V ∈ W ∧ t ∈ R ∧ f ∈ P → t = F ⁡ f ↔ t = x y | ∃ c ∈ f c = x y
53 52 rexbidva ⊢ V ∈ W ∧ t ∈ R → ∃ f ∈ P t = F ⁡ f ↔ ∃ f ∈ P t = x y | ∃ c ∈ f c = x y
54 49 53 mpbird ⊢ V ∈ W ∧ t ∈ R → ∃ f ∈ P t = F ⁡ f
55 54 ralrimiva ⊢ V ∈ W → ∀ t ∈ R ∃ f ∈ P t = F ⁡ f
56 dffo3 ⊢ F : P ⟶ onto R ↔ F : P ⟶ R ∧ ∀ t ∈ R ∃ f ∈ P t = F ⁡ f
57 5 55 56 sylanbrc ⊢ V ∈ W → F : P ⟶ onto R