Theorem fvineqsneu

Description: A theorem about functions where the image of every point intersects the domain only at that point. (Contributed by ML, 27-Mar-2021)

	Ref	Expression
Assertion	fvineqsneu	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ∀ 𝑞 ∈ 𝐴 ∃! 𝑥 ∈ ran 𝐹 𝑞 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		fnfvelrn	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑜 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑜 ) ∈ ran 𝐹 )
2	1	ex	⊢ ( 𝐹 Fn 𝐴 → ( 𝑜 ∈ 𝐴 → ( 𝐹 ‘ 𝑜 ) ∈ ran 𝐹 ) )
3	2	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑜 ∈ 𝐴 → ( 𝐹 ‘ 𝑜 ) ∈ ran 𝐹 ) )
4		fnrnfv	⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑝 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑝 ) } )
5	4	abeq2d	⊢ ( 𝐹 Fn 𝐴 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑝 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑝 ) ) )
6	5	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑝 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑝 ) ) )
7		nfv	⊢ Ⅎ 𝑝 𝐹 Fn 𝐴
8		nfra1	⊢ Ⅎ 𝑝 ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 }
9	7 8	nfan	⊢ Ⅎ 𝑝 ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } )
10		nfv	⊢ Ⅎ 𝑝 ∀ 𝑜 ∈ 𝐴 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) )
11		eleq2	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ( 𝑜 ∈ 𝑦 ↔ 𝑜 ∈ ( 𝐹 ‘ 𝑝 ) ) )
12		elin	⊢ ( 𝑜 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ ( 𝑜 ∈ ( 𝐹 ‘ 𝑝 ) ∧ 𝑜 ∈ 𝐴 ) )
13	12	rbaib	⊢ ( 𝑜 ∈ 𝐴 → ( 𝑜 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ 𝑜 ∈ ( 𝐹 ‘ 𝑝 ) ) )
14	13	ad2antll	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) → ( 𝑜 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ 𝑜 ∈ ( 𝐹 ‘ 𝑝 ) ) )
15		rsp	⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( 𝑝 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) )
16		eleq2	⊢ ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( 𝑜 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ 𝑜 ∈ { 𝑝 } ) )
17		velsn	⊢ ( 𝑜 ∈ { 𝑝 } ↔ 𝑜 = 𝑝 )
18		equcom	⊢ ( 𝑜 = 𝑝 ↔ 𝑝 = 𝑜 )
19	17 18	bitri	⊢ ( 𝑜 ∈ { 𝑝 } ↔ 𝑝 = 𝑜 )
20	16 19	bitrdi	⊢ ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( 𝑜 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ 𝑝 = 𝑜 ) )
21	15 20	syl6	⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( 𝑝 ∈ 𝐴 → ( 𝑜 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ 𝑝 = 𝑜 ) ) )
22	21	adantl	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑝 ∈ 𝐴 → ( 𝑜 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ 𝑝 = 𝑜 ) ) )
23	22	adantrd	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) → ( 𝑜 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ 𝑝 = 𝑜 ) ) )
24	23	imp	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) → ( 𝑜 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ 𝑝 = 𝑜 ) )
25	14 24	bitr3d	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) → ( 𝑜 ∈ ( 𝐹 ‘ 𝑝 ) ↔ 𝑝 = 𝑜 ) )
26	11 25	sylan9bbr	⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) → ( 𝑜 ∈ 𝑦 ↔ 𝑝 = 𝑜 ) )
27	26	ex	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) → ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ( 𝑜 ∈ 𝑦 ↔ 𝑝 = 𝑜 ) ) )
28	27	anass1rs	⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑜 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ( 𝑜 ∈ 𝑦 ↔ 𝑝 = 𝑜 ) ) )
29	28	impr	⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑜 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) ) → ( 𝑜 ∈ 𝑦 ↔ 𝑝 = 𝑜 ) )
30	29	an32s	⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) ) ∧ 𝑜 ∈ 𝐴 ) → ( 𝑜 ∈ 𝑦 ↔ 𝑝 = 𝑜 ) )
31		eqeq1	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ( 𝑦 = ( 𝐹 ‘ 𝑜 ) ↔ ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) ) )
32		dffn3	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 )
33		fvineqsnf1	⊢ ( ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → 𝐹 : 𝐴 –1-1→ ran 𝐹 )
34	32 33	sylanb	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → 𝐹 : 𝐴 –1-1→ ran 𝐹 )
35		dff13	⊢ ( 𝐹 : 𝐴 –1-1→ ran 𝐹 ↔ ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑜 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) ) )
36	34 35	sylib	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑜 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) ) )
37	36	simprd	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ∀ 𝑝 ∈ 𝐴 ∀ 𝑜 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) )
38		rsp	⊢ ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑜 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) → ( 𝑝 ∈ 𝐴 → ∀ 𝑜 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) ) )
39	37 38	syl	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑝 ∈ 𝐴 → ∀ 𝑜 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) ) )
40		rsp	⊢ ( ∀ 𝑜 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) → ( 𝑜 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) ) )
41	39 40	syl6	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑝 ∈ 𝐴 → ( 𝑜 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) ) ) )
42	41	imp32	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) )
43		fveq2	⊢ ( 𝑝 = 𝑜 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) )
44	42 43	impbid1	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) ↔ 𝑝 = 𝑜 ) )
45	31 44	sylan9bbr	⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) → ( 𝑦 = ( 𝐹 ‘ 𝑜 ) ↔ 𝑝 = 𝑜 ) )
46	45	ex	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) → ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ( 𝑦 = ( 𝐹 ‘ 𝑜 ) ↔ 𝑝 = 𝑜 ) ) )
47	46	anass1rs	⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑜 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ( 𝑦 = ( 𝐹 ‘ 𝑜 ) ↔ 𝑝 = 𝑜 ) ) )
48	47	impr	⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑜 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) ) → ( 𝑦 = ( 𝐹 ‘ 𝑜 ) ↔ 𝑝 = 𝑜 ) )
49	48	an32s	⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) ) ∧ 𝑜 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑜 ) ↔ 𝑝 = 𝑜 ) )
50	30 49	bitr4d	⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) ) ∧ 𝑜 ∈ 𝐴 ) → ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) )
51	50	ex	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) ) → ( 𝑜 ∈ 𝐴 → ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) )
52	51	ralrimiv	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) ) → ∀ 𝑜 ∈ 𝐴 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) )
53	52	exp32	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑝 ∈ 𝐴 → ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ∀ 𝑜 ∈ 𝐴 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) ) )
54	9 10 53	rexlimd	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( ∃ 𝑝 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑝 ) → ∀ 𝑜 ∈ 𝐴 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) )
55	6 54	sylbid	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑦 ∈ ran 𝐹 → ∀ 𝑜 ∈ 𝐴 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) )
56		rsp	⊢ ( ∀ 𝑜 ∈ 𝐴 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) → ( 𝑜 ∈ 𝐴 → ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) )
57	55 56	syl6	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑦 ∈ ran 𝐹 → ( 𝑜 ∈ 𝐴 → ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) ) )
58	57	com23	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑜 ∈ 𝐴 → ( 𝑦 ∈ ran 𝐹 → ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) ) )
59	58	ralrimdv	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑜 ∈ 𝐴 → ∀ 𝑦 ∈ ran 𝐹 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) )
60		reu6i	⊢ ( ( ( 𝐹 ‘ 𝑜 ) ∈ ran 𝐹 ∧ ∀ 𝑦 ∈ ran 𝐹 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) → ∃! 𝑦 ∈ ran 𝐹 𝑜 ∈ 𝑦 )
61	60	ex	⊢ ( ( 𝐹 ‘ 𝑜 ) ∈ ran 𝐹 → ( ∀ 𝑦 ∈ ran 𝐹 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) → ∃! 𝑦 ∈ ran 𝐹 𝑜 ∈ 𝑦 ) )
62	3 59 61	syl6c	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑜 ∈ 𝐴 → ∃! 𝑦 ∈ ran 𝐹 𝑜 ∈ 𝑦 ) )
63	62	ralrimiv	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ∀ 𝑜 ∈ 𝐴 ∃! 𝑦 ∈ ran 𝐹 𝑜 ∈ 𝑦 )
64		nfv	⊢ Ⅎ 𝑥 𝑞 = 𝑜
65		nfv	⊢ Ⅎ 𝑦 𝑞 = 𝑜
66		nfvd	⊢ ( 𝑞 = 𝑜 → Ⅎ 𝑦 𝑞 ∈ 𝑥 )
67		nfvd	⊢ ( 𝑞 = 𝑜 → Ⅎ 𝑥 𝑜 ∈ 𝑦 )
68		eleq12	⊢ ( ( 𝑞 = 𝑜 ∧ 𝑥 = 𝑦 ) → ( 𝑞 ∈ 𝑥 ↔ 𝑜 ∈ 𝑦 ) )
69	68	ex	⊢ ( 𝑞 = 𝑜 → ( 𝑥 = 𝑦 → ( 𝑞 ∈ 𝑥 ↔ 𝑜 ∈ 𝑦 ) ) )
70	64 65 66 67 69	cbvreud	⊢ ( 𝑞 = 𝑜 → ( ∃! 𝑥 ∈ ran 𝐹 𝑞 ∈ 𝑥 ↔ ∃! 𝑦 ∈ ran 𝐹 𝑜 ∈ 𝑦 ) )
71	70	cbvralvw	⊢ ( ∀ 𝑞 ∈ 𝐴 ∃! 𝑥 ∈ ran 𝐹 𝑞 ∈ 𝑥 ↔ ∀ 𝑜 ∈ 𝐴 ∃! 𝑦 ∈ ran 𝐹 𝑜 ∈ 𝑦 )
72	63 71	sylibr	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ∀ 𝑞 ∈ 𝐴 ∃! 𝑥 ∈ ran 𝐹 𝑞 ∈ 𝑥 )