Metamath Proof Explorer

Theorem uspgrbisymrelALT

Description: Alternate proof of uspgrbisymrel not using the definition of equinumerosity. (Contributed by AV, 26-Nov-2021) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses uspgrbisymrel.g ⊢ G = v e | v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e
uspgrbisymrel.r ⊢ R = r ∈ 𝒫 V × V | ∀ x ∈ V ∀ y ∈ V x r y ↔ y r x
Assertion uspgrbisymrelALT ⊢ V ∈ W → ∃ f f : G ⟶ 1-1 onto R

Proof

Step Hyp Ref Expression
1 uspgrbisymrel.g ⊢ G = v e | v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e
2 uspgrbisymrel.r ⊢ R = r ∈ 𝒫 V × V | ∀ x ∈ V ∀ y ∈ V x r y ↔ y r x
3 fvex ⊢ Pairs ⁡ V ∈ V
4 3 pwex ⊢ 𝒫 Pairs ⁡ V ∈ V
5 mptexg ⊢ 𝒫 Pairs ⁡ V ∈ V → p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y ∈ V
6 4 5 mp1i ⊢ V ∈ W → p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y ∈ V
7 eqid ⊢ 𝒫 Pairs ⁡ V = 𝒫 Pairs ⁡ V
8 7 1 uspgrex ⊢ V ∈ W → G ∈ V
9 mptexg ⊢ G ∈ V → g ∈ G ⟼ 2 nd ⁡ g ∈ V
10 8 9 syl ⊢ V ∈ W → g ∈ G ⟼ 2 nd ⁡ g ∈ V
11 coexg ⊢ p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y ∈ V ∧ g ∈ G ⟼ 2 nd ⁡ g ∈ V → p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y ∘ g ∈ G ⟼ 2 nd ⁡ g ∈ V
12 6 10 11 syl2anc ⊢ V ∈ W → p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y ∘ g ∈ G ⟼ 2 nd ⁡ g ∈ V
13 eqid ⊢ p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y = p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y
14 7 2 13 sprsymrelf1o ⊢ V ∈ W → p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y : 𝒫 Pairs ⁡ V ⟶ 1-1 onto R
15 eqid ⊢ g ∈ G ⟼ 2 nd ⁡ g = g ∈ G ⟼ 2 nd ⁡ g
16 7 1 15 uspgrsprf1o ⊢ V ∈ W → g ∈ G ⟼ 2 nd ⁡ g : G ⟶ 1-1 onto 𝒫 Pairs ⁡ V
17 f1oco ⊢ p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y : 𝒫 Pairs ⁡ V ⟶ 1-1 onto R ∧ g ∈ G ⟼ 2 nd ⁡ g : G ⟶ 1-1 onto 𝒫 Pairs ⁡ V → p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y ∘ g ∈ G ⟼ 2 nd ⁡ g : G ⟶ 1-1 onto R
18 14 16 17 syl2anc ⊢ V ∈ W → p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y ∘ g ∈ G ⟼ 2 nd ⁡ g : G ⟶ 1-1 onto R
19 f1oeq1 ⊢ f = p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y ∘ g ∈ G ⟼ 2 nd ⁡ g → f : G ⟶ 1-1 onto R ↔ p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y ∘ g ∈ G ⟼ 2 nd ⁡ g : G ⟶ 1-1 onto R
20 19 spcegv ⊢ p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y ∘ g ∈ G ⟼ 2 nd ⁡ g ∈ V → p ∈ 𝒫 Pairs ⁡ V ⟼ x y | ∃ c ∈ p c = x y ∘ g ∈ G ⟼ 2 nd ⁡ g : G ⟶ 1-1 onto R → ∃ f f : G ⟶ 1-1 onto R
21 12 18 20 sylc ⊢ V ∈ W → ∃ f f : G ⟶ 1-1 onto R