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

Proof

Step Hyp Ref Expression
1 sprsymrelf.p ⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2 sprsymrelf.r ⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
3 sprsymrelf.f ⊢ 𝐹 = ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } )
4 1 2 3 sprsymrelf ⊢ 𝐹 : 𝑃 ⟶ 𝑅
5 4 a1i ⊢ ( 𝑉 ∈ 𝑊 → 𝐹 : 𝑃 ⟶ 𝑅 )
6 breq ⊢ ( 𝑟 = 𝑡 → ( 𝑥 𝑟 𝑦 ↔ 𝑥 𝑡 𝑦 ) )
7 breq ⊢ ( 𝑟 = 𝑡 → ( 𝑦 𝑟 𝑥 ↔ 𝑦 𝑡 𝑥 ) )
8 6 7 bibi12d ⊢ ( 𝑟 = 𝑡 → ( ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) ↔ ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) ) )
9 8 2ralbidv ⊢ ( 𝑟 = 𝑡 → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) ) )
10 9 2 elrab2 ⊢ ( 𝑡 ∈ 𝑅 ↔ ( 𝑡 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) ) )
11 eqid ⊢ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } = { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) }
12 11 sprsymrelfolem1 ⊢ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } ∈ 𝒫 ( Pairs ‘ 𝑉 )
13 12 1 eleqtrri ⊢ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } ∈ 𝑃
14 13 a1i ⊢ ( ( ( 𝑡 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) ) ∧ 𝑉 ∈ 𝑊 ) → { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } ∈ 𝑃 )
15 rexeq ⊢ ( 𝑓 = { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } → ( ∃ 𝑐 ∈ 𝑓 𝑐 = { 𝑥 , 𝑦 } ↔ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } ) )
16 15 opabbidv ⊢ ( 𝑓 = { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑓 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } )
17 16 eqeq2d ⊢ ( 𝑓 = { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } → ( 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑓 𝑐 = { 𝑥 , 𝑦 } } ↔ 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } ) )
18 17 adantl ⊢ ( ( ( ( 𝑡 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) ) ∧ 𝑉 ∈ 𝑊 ) ∧ 𝑓 = { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } ) → ( 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑓 𝑐 = { 𝑥 , 𝑦 } } ↔ 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } ) )
19 velpw ⊢ ( 𝑡 ∈ 𝒫 ( 𝑉 × 𝑉 ) ↔ 𝑡 ⊆ ( 𝑉 × 𝑉 ) )
20 xpss ⊢ ( 𝑉 × 𝑉 ) ⊆ ( V × V )
21 sstr2 ⊢ ( 𝑡 ⊆ ( 𝑉 × 𝑉 ) → ( ( 𝑉 × 𝑉 ) ⊆ ( V × V ) → 𝑡 ⊆ ( V × V ) ) )
22 20 21 mpi ⊢ ( 𝑡 ⊆ ( 𝑉 × 𝑉 ) → 𝑡 ⊆ ( V × V ) )
23 df-rel ⊢ ( Rel 𝑡 ↔ 𝑡 ⊆ ( V × V ) )
24 22 23 sylibr ⊢ ( 𝑡 ⊆ ( 𝑉 × 𝑉 ) → Rel 𝑡 )
25 24 adantl ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) ) → Rel 𝑡 )
26 dfrel4v ⊢ ( Rel 𝑡 ↔ 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑡 𝑦 } )
27 nfv ⊢ Ⅎ 𝑥 ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) )
28 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 )
29 27 28 nfan ⊢ Ⅎ 𝑥 ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) )
30 nfv ⊢ Ⅎ 𝑦 ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) )
31 nfra2w ⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 )
32 30 31 nfan ⊢ Ⅎ 𝑦 ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) )
33 11 sprsymrelfolem2 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) ) → ( 𝑥 𝑡 𝑦 ↔ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } ) )
34 33 3expa ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) ) → ( 𝑥 𝑡 𝑦 ↔ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } ) )
35 29 32 34 opabbid ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑡 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } )
36 35 eqeq2d ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) ) → ( 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑡 𝑦 } ↔ 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } ) )
37 36 biimpd ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) ) → ( 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑡 𝑦 } → 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } ) )
38 37 ex ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) → ( 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑡 𝑦 } → 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } ) ) )
39 38 com23 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) ) → ( 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑡 𝑦 } → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) → 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } ) ) )
40 26 39 syl5bi ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) ) → ( Rel 𝑡 → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) → 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } ) ) )
41 25 40 mpd ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ ( 𝑉 × 𝑉 ) ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) → 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } ) )
42 41 expcom ⊢ ( 𝑡 ⊆ ( 𝑉 × 𝑉 ) → ( 𝑉 ∈ 𝑊 → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) → 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } ) ) )
43 42 com23 ⊢ ( 𝑡 ⊆ ( 𝑉 × 𝑉 ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) → ( 𝑉 ∈ 𝑊 → 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } ) ) )
44 19 43 sylbi ⊢ ( 𝑡 ∈ 𝒫 ( 𝑉 × 𝑉 ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) → ( 𝑉 ∈ 𝑊 → 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } ) ) )
45 44 imp31 ⊢ ( ( ( 𝑡 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) ) ∧ 𝑉 ∈ 𝑊 ) → 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑡 𝑏 ) } 𝑐 = { 𝑥 , 𝑦 } } )
46 14 18 45 rspcedvd ⊢ ( ( ( 𝑡 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) ) ∧ 𝑉 ∈ 𝑊 ) → ∃ 𝑓 ∈ 𝑃 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑓 𝑐 = { 𝑥 , 𝑦 } } )
47 46 ex ⊢ ( ( 𝑡 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑡 𝑦 ↔ 𝑦 𝑡 𝑥 ) ) → ( 𝑉 ∈ 𝑊 → ∃ 𝑓 ∈ 𝑃 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑓 𝑐 = { 𝑥 , 𝑦 } } ) )
48 10 47 sylbi ⊢ ( 𝑡 ∈ 𝑅 → ( 𝑉 ∈ 𝑊 → ∃ 𝑓 ∈ 𝑃 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑓 𝑐 = { 𝑥 , 𝑦 } } ) )
49 48 impcom ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ∈ 𝑅 ) → ∃ 𝑓 ∈ 𝑃 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑓 𝑐 = { 𝑥 , 𝑦 } } )
50 1 2 3 sprsymrelfv ⊢ ( 𝑓 ∈ 𝑃 → ( 𝐹 ‘ 𝑓 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑓 𝑐 = { 𝑥 , 𝑦 } } )
51 50 adantl ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ∈ 𝑅 ) ∧ 𝑓 ∈ 𝑃 ) → ( 𝐹 ‘ 𝑓 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑓 𝑐 = { 𝑥 , 𝑦 } } )
52 51 eqeq2d ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ∈ 𝑅 ) ∧ 𝑓 ∈ 𝑃 ) → ( 𝑡 = ( 𝐹 ‘ 𝑓 ) ↔ 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑓 𝑐 = { 𝑥 , 𝑦 } } ) )
53 52 rexbidva ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ∈ 𝑅 ) → ( ∃ 𝑓 ∈ 𝑃 𝑡 = ( 𝐹 ‘ 𝑓 ) ↔ ∃ 𝑓 ∈ 𝑃 𝑡 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑓 𝑐 = { 𝑥 , 𝑦 } } ) )
54 49 53 mpbird ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑡 ∈ 𝑅 ) → ∃ 𝑓 ∈ 𝑃 𝑡 = ( 𝐹 ‘ 𝑓 ) )
55 54 ralrimiva ⊢ ( 𝑉 ∈ 𝑊 → ∀ 𝑡 ∈ 𝑅 ∃ 𝑓 ∈ 𝑃 𝑡 = ( 𝐹 ‘ 𝑓 ) )
56 dffo3 ⊢ ( 𝐹 : 𝑃 –onto→ 𝑅 ↔ ( 𝐹 : 𝑃 ⟶ 𝑅 ∧ ∀ 𝑡 ∈ 𝑅 ∃ 𝑓 ∈ 𝑃 𝑡 = ( 𝐹 ‘ 𝑓 ) ) )
57 5 55 56 sylanbrc ⊢ ( 𝑉 ∈ 𝑊 → 𝐹 : 𝑃 –onto→ 𝑅 )