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	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
	sprsymrelf.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
	sprsymrelf.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } )
Assertion	sprsymrelf	⊢ 𝐹 : 𝑃 ⟶ 𝑅

Proof

Step	Hyp	Ref	Expression
1		sprsymrelf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2		sprsymrelf.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
3		sprsymrelf.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } )
4		sprsymrelfvlem	⊢ ( 𝑝 ⊆ ( Pairs ‘ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) )
5		prcom	⊢ { 𝑥 , 𝑦 } = { 𝑦 , 𝑥 }
6	5	a1i	⊢ ( ( ( 𝑝 ⊆ ( Pairs ‘ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑝 ) → { 𝑥 , 𝑦 } = { 𝑦 , 𝑥 } )
7	6	eqeq2d	⊢ ( ( ( 𝑝 ⊆ ( Pairs ‘ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑝 ) → ( 𝑐 = { 𝑥 , 𝑦 } ↔ 𝑐 = { 𝑦 , 𝑥 } ) )
8	7	rexbidva	⊢ ( ( 𝑝 ⊆ ( Pairs ‘ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } ↔ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑦 , 𝑥 } ) )
9		df-br	⊢ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } )
10		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ↔ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } )
11	9 10	bitri	⊢ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑦 ↔ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } )
12		vex	⊢ 𝑦 ∈ V
13		vex	⊢ 𝑥 ∈ V
14		preq12	⊢ ( ( 𝑎 = 𝑦 ∧ 𝑏 = 𝑥 ) → { 𝑎 , 𝑏 } = { 𝑦 , 𝑥 } )
15	14	eqeq2d	⊢ ( ( 𝑎 = 𝑦 ∧ 𝑏 = 𝑥 ) → ( 𝑐 = { 𝑎 , 𝑏 } ↔ 𝑐 = { 𝑦 , 𝑥 } ) )
16	15	rexbidv	⊢ ( ( 𝑎 = 𝑦 ∧ 𝑏 = 𝑥 ) → ( ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑎 , 𝑏 } ↔ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑦 , 𝑥 } ) )
17		preq12	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } )
18	17	eqeq2d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑐 = { 𝑥 , 𝑦 } ↔ 𝑐 = { 𝑎 , 𝑏 } ) )
19	18	rexbidv	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } ↔ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑎 , 𝑏 } ) )
20	19	cbvopabv	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑎 , 𝑏 } }
21	12 13 16 20	braba	⊢ ( 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑥 ↔ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑦 , 𝑥 } )
22	8 11 21	3bitr4g	⊢ ( ( 𝑝 ⊆ ( Pairs ‘ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑦 ↔ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑥 ) )
23	22	ralrimivva	⊢ ( 𝑝 ⊆ ( Pairs ‘ 𝑉 ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑦 ↔ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑥 ) )
24	4 23	jca	⊢ ( 𝑝 ⊆ ( Pairs ‘ 𝑉 ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑦 ↔ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑥 ) ) )
25	1	eleq2i	⊢ ( 𝑝 ∈ 𝑃 ↔ 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) )
26		vex	⊢ 𝑝 ∈ V
27	26	elpw	⊢ ( 𝑝 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↔ 𝑝 ⊆ ( Pairs ‘ 𝑉 ) )
28	25 27	bitri	⊢ ( 𝑝 ∈ 𝑃 ↔ 𝑝 ⊆ ( Pairs ‘ 𝑉 ) )
29		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } }
30	29	nfeq2	⊢ Ⅎ 𝑥 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } }
31		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } }
32	31	nfeq2	⊢ Ⅎ 𝑦 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } }
33		breq	⊢ ( 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } → ( 𝑥 𝑟 𝑦 ↔ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑦 ) )
34		breq	⊢ ( 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } → ( 𝑦 𝑟 𝑥 ↔ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑥 ) )
35	33 34	bibi12d	⊢ ( 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } → ( ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) ↔ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑦 ↔ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑥 ) ) )
36	32 35	ralbid	⊢ ( 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } → ( ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑉 ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑦 ↔ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑥 ) ) )
37	30 36	ralbid	⊢ ( 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑦 ↔ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑥 ) ) )
38	37	elrab	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ∈ { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) } ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑦 ↔ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } 𝑥 ) ) )
39	24 28 38	3imtr4i	⊢ ( 𝑝 ∈ 𝑃 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ∈ { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) } )
40	39 2	eleqtrrdi	⊢ ( 𝑝 ∈ 𝑃 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝑅 )
41	3 40	fmpti	⊢ 𝐹 : 𝑃 ⟶ 𝑅