Theorem sprsymrelf1

Description: The mapping F is a one-to-one 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	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
	sprsymrelf.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
	sprsymrelf.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } )
Assertion	sprsymrelf1	⊢ 𝐹 : 𝑃 –1-1→ 𝑅

Proof

Step	Hyp	Ref	Expression
1		sprsymrelf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2		sprsymrelf.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
3		sprsymrelf.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } )
4	1 2 3	sprsymrelf	⊢ 𝐹 : 𝑃 ⟶ 𝑅
5	1 2 3	sprsymrelfv	⊢ ( 𝑎 ∈ 𝑃 → ( 𝐹 ‘ 𝑎 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } )
6	1 2 3	sprsymrelfv	⊢ ( 𝑏 ∈ 𝑃 → ( 𝐹 ‘ 𝑏 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } )
7	5 6	eqeqan12d	⊢ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) )
8	1	eleq2i	⊢ ( 𝑎 ∈ 𝑃 ↔ 𝑎 ∈ 𝒫 ( Pairs ‘ 𝑉 ) )
9		vex	⊢ 𝑎 ∈ V
10	9	elpw	⊢ ( 𝑎 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↔ 𝑎 ⊆ ( Pairs ‘ 𝑉 ) )
11	8 10	bitri	⊢ ( 𝑎 ∈ 𝑃 ↔ 𝑎 ⊆ ( Pairs ‘ 𝑉 ) )
12	1	eleq2i	⊢ ( 𝑏 ∈ 𝑃 ↔ 𝑏 ∈ 𝒫 ( Pairs ‘ 𝑉 ) )
13		vex	⊢ 𝑏 ∈ V
14	13	elpw	⊢ ( 𝑏 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↔ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) )
15	12 14	bitri	⊢ ( 𝑏 ∈ 𝑃 ↔ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) )
16		sprsymrelf1lem	⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } → 𝑎 ⊆ 𝑏 ) )
17	16	imp	⊢ ( ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) → 𝑎 ⊆ 𝑏 )
18		eqcom	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } )
19		sprsymrelf1lem	⊢ ( ( 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } → 𝑏 ⊆ 𝑎 ) )
20	18 19	syl5bi	⊢ ( ( 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } → 𝑏 ⊆ 𝑎 ) )
21	20	ancoms	⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } → 𝑏 ⊆ 𝑎 ) )
22	21	imp	⊢ ( ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) → 𝑏 ⊆ 𝑎 )
23	17 22	eqssd	⊢ ( ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) → 𝑎 = 𝑏 )
24	23	ex	⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } → 𝑎 = 𝑏 ) )
25	11 15 24	syl2anb	⊢ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } → 𝑎 = 𝑏 ) )
26	7 25	sylbid	⊢ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
27	26	rgen2	⊢ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 )
28		dff13	⊢ ( 𝐹 : 𝑃 –1-1→ 𝑅 ↔ ( 𝐹 : 𝑃 ⟶ 𝑅 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
29	4 27 28	mpbir2an	⊢ 𝐹 : 𝑃 –1-1→ 𝑅