Theorem fsetsnf1

Description: The mapping of an element of a class to a singleton function is an injection. (Contributed by AV, 13-Sep-2024)

	Ref	Expression
Hypotheses	fsetsnf.a	⊢ 𝐴 = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } }
	fsetsnf.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ { ⟨ 𝑆 , 𝑥 ⟩ } )
Assertion	fsetsnf1	⊢ ( 𝑆 ∈ 𝑉 → 𝐹 : 𝐵 –1-1→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fsetsnf.a	⊢ 𝐴 = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } }
2		fsetsnf.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ { ⟨ 𝑆 , 𝑥 ⟩ } )
3	1 2	fsetsnf	⊢ ( 𝑆 ∈ 𝑉 → 𝐹 : 𝐵 ⟶ 𝐴 )
4	2	a1i	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ { ⟨ 𝑆 , 𝑥 ⟩ } ) )
5		opeq2	⊢ ( 𝑥 = 𝑚 → ⟨ 𝑆 , 𝑥 ⟩ = ⟨ 𝑆 , 𝑚 ⟩ )
6	5	sneqd	⊢ ( 𝑥 = 𝑚 → { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑚 ⟩ } )
7	6	adantl	⊢ ( ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑥 = 𝑚 ) → { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑚 ⟩ } )
8		simpl	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → 𝑚 ∈ 𝐵 )
9		snex	⊢ { ⟨ 𝑆 , 𝑚 ⟩ } ∈ V
10	9	a1i	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → { ⟨ 𝑆 , 𝑚 ⟩ } ∈ V )
11	4 7 8 10	fvmptd	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑚 ) = { ⟨ 𝑆 , 𝑚 ⟩ } )
12		opeq2	⊢ ( 𝑥 = 𝑛 → ⟨ 𝑆 , 𝑥 ⟩ = ⟨ 𝑆 , 𝑛 ⟩ )
13	12	sneqd	⊢ ( 𝑥 = 𝑛 → { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑛 ⟩ } )
14	13	adantl	⊢ ( ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑥 = 𝑛 ) → { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑛 ⟩ } )
15		simpr	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → 𝑛 ∈ 𝐵 )
16		snex	⊢ { ⟨ 𝑆 , 𝑛 ⟩ } ∈ V
17	16	a1i	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → { ⟨ 𝑆 , 𝑛 ⟩ } ∈ V )
18	4 14 15 17	fvmptd	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑛 ) = { ⟨ 𝑆 , 𝑛 ⟩ } )
19	11 18	eqeq12d	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) ↔ { ⟨ 𝑆 , 𝑚 ⟩ } = { ⟨ 𝑆 , 𝑛 ⟩ } ) )
20	19	adantl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) ↔ { ⟨ 𝑆 , 𝑚 ⟩ } = { ⟨ 𝑆 , 𝑛 ⟩ } ) )
21		opex	⊢ ⟨ 𝑆 , 𝑚 ⟩ ∈ V
22	21	sneqr	⊢ ( { ⟨ 𝑆 , 𝑚 ⟩ } = { ⟨ 𝑆 , 𝑛 ⟩ } → ⟨ 𝑆 , 𝑚 ⟩ = ⟨ 𝑆 , 𝑛 ⟩ )
23		opthg	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑚 ∈ 𝐵 ) → ( ⟨ 𝑆 , 𝑚 ⟩ = ⟨ 𝑆 , 𝑛 ⟩ ↔ ( 𝑆 = 𝑆 ∧ 𝑚 = 𝑛 ) ) )
24	23	adantrr	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) ) → ( ⟨ 𝑆 , 𝑚 ⟩ = ⟨ 𝑆 , 𝑛 ⟩ ↔ ( 𝑆 = 𝑆 ∧ 𝑚 = 𝑛 ) ) )
25		simpr	⊢ ( ( 𝑆 = 𝑆 ∧ 𝑚 = 𝑛 ) → 𝑚 = 𝑛 )
26	24 25	syl6bi	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) ) → ( ⟨ 𝑆 , 𝑚 ⟩ = ⟨ 𝑆 , 𝑛 ⟩ → 𝑚 = 𝑛 ) )
27	22 26	syl5	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) ) → ( { ⟨ 𝑆 , 𝑚 ⟩ } = { ⟨ 𝑆 , 𝑛 ⟩ } → 𝑚 = 𝑛 ) )
28	20 27	sylbid	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) → 𝑚 = 𝑛 ) )
29	28	ralrimivva	⊢ ( 𝑆 ∈ 𝑉 → ∀ 𝑚 ∈ 𝐵 ∀ 𝑛 ∈ 𝐵 ( ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) → 𝑚 = 𝑛 ) )
30		dff13	⊢ ( 𝐹 : 𝐵 –1-1→ 𝐴 ↔ ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑚 ∈ 𝐵 ∀ 𝑛 ∈ 𝐵 ( ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) → 𝑚 = 𝑛 ) ) )
31	3 29 30	sylanbrc	⊢ ( 𝑆 ∈ 𝑉 → 𝐹 : 𝐵 –1-1→ 𝐴 )