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	⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
	uspgrbisymrel.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
Assertion	uspgrbisymrelALT	⊢ ( 𝑉 ∈ 𝑊 → ∃ 𝑓 𝑓 : 𝐺 –1-1-onto→ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		uspgrbisymrel.g	⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
2		uspgrbisymrel.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
3		fvex	⊢ ( Pairs ‘ 𝑉 ) ∈ V
4	3	pwex	⊢ 𝒫 ( Pairs ‘ 𝑉 ) ∈ V
5		mptexg	⊢ ( 𝒫 ( Pairs ‘ 𝑉 ) ∈ V → ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∈ V )
6	4 5	mp1i	⊢ ( 𝑉 ∈ 𝑊 → ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∈ V )
7		eqid	⊢ 𝒫 ( Pairs ‘ 𝑉 ) = 𝒫 ( Pairs ‘ 𝑉 )
8	7 1	uspgrex	⊢ ( 𝑉 ∈ 𝑊 → 𝐺 ∈ V )
9		mptexg	⊢ ( 𝐺 ∈ V → ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) ∈ V )
10	8 9	syl	⊢ ( 𝑉 ∈ 𝑊 → ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) ∈ V )
11		coexg	⊢ ( ( ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∈ V ∧ ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) ∈ V ) → ( ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∘ ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) ) ∈ V )
12	6 10 11	syl2anc	⊢ ( 𝑉 ∈ 𝑊 → ( ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∘ ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) ) ∈ V )
13		eqid	⊢ ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) = ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } )
14	7 2 13	sprsymrelf1o	⊢ ( 𝑉 ∈ 𝑊 → ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) : 𝒫 ( Pairs ‘ 𝑉 ) –1-1-onto→ 𝑅 )
15		eqid	⊢ ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) = ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) )
16	7 1 15	uspgrsprf1o	⊢ ( 𝑉 ∈ 𝑊 → ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) : 𝐺 –1-1-onto→ 𝒫 ( Pairs ‘ 𝑉 ) )
17		f1oco	⊢ ( ( ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) : 𝒫 ( Pairs ‘ 𝑉 ) –1-1-onto→ 𝑅 ∧ ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) : 𝐺 –1-1-onto→ 𝒫 ( Pairs ‘ 𝑉 ) ) → ( ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∘ ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) ) : 𝐺 –1-1-onto→ 𝑅 )
18	14 16 17	syl2anc	⊢ ( 𝑉 ∈ 𝑊 → ( ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∘ ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) ) : 𝐺 –1-1-onto→ 𝑅 )
19		f1oeq1	⊢ ( 𝑓 = ( ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∘ ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) ) → ( 𝑓 : 𝐺 –1-1-onto→ 𝑅 ↔ ( ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∘ ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) ) : 𝐺 –1-1-onto→ 𝑅 ) )
20	19	spcegv	⊢ ( ( ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∘ ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) ) ∈ V → ( ( ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∘ ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) ) : 𝐺 –1-1-onto→ 𝑅 → ∃ 𝑓 𝑓 : 𝐺 –1-1-onto→ 𝑅 ) )
21	12 18 20	sylc	⊢ ( 𝑉 ∈ 𝑊 → ∃ 𝑓 𝑓 : 𝐺 –1-1-onto→ 𝑅 )