Metamath Proof Explorer

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 eqabrd ⊢ ( 𝐹 Fn 𝐴 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑝 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑝 ) ) )
6 5 adantr ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑝 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑝 ) ) )
7 nfv ⊢ Ⅎ 𝑝 𝐹 Fn 𝐴
8 nfra1 ⊢ Ⅎ 𝑝 ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 }
9 7 8 nfan ⊢ Ⅎ 𝑝 ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } )
10 nfv ⊢ Ⅎ 𝑝 ∀ 𝑜 ∈ 𝐴 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) )
11 eleq2w2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ( 𝑜 ∈ 𝑦 ↔ 𝑜 ∈ ( 𝐹 ‘ 𝑝 ) ) )
12 elin ⊢ ( 𝑜 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ ( 𝑜 ∈ ( 𝐹 ‘ 𝑝 ) ∧ 𝑜 ∈ 𝐴 ) )
13 12 rbaib ⊢ ( 𝑜 ∈ 𝐴 → ( 𝑜 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ 𝑜 ∈ ( 𝐹 ‘ 𝑝 ) ) )
14 13 ad2antll ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) → ( 𝑜 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ 𝑜 ∈ ( 𝐹 ‘ 𝑝 ) ) )
15 rsp ⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( 𝑝 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) )
16 eleq2w2 ⊢ ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( 𝑜 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ 𝑜 ∈ { 𝑝 } ) )
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 rsp ⊢ ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑜 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) → ( 𝑝 ∈ 𝐴 → ∀ 𝑜 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) ) )
38 36 37 simpl2im ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑝 ∈ 𝐴 → ∀ 𝑜 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) ) )
39 rsp ⊢ ( ∀ 𝑜 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) → ( 𝑜 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) ) )
40 38 39 syl6 ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑝 ∈ 𝐴 → ( 𝑜 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) ) ) )
41 40 imp32 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) → 𝑝 = 𝑜 ) )
42 fveq2 ⊢ ( 𝑝 = 𝑜 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) )
43 41 42 impbid1 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑜 ) ↔ 𝑝 = 𝑜 ) )
44 31 43 sylan9bbr ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) → ( 𝑦 = ( 𝐹 ‘ 𝑜 ) ↔ 𝑝 = 𝑜 ) )
45 44 ex ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑜 ∈ 𝐴 ) ) → ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ( 𝑦 = ( 𝐹 ‘ 𝑜 ) ↔ 𝑝 = 𝑜 ) ) )
46 45 anass1rs ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑜 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ( 𝑦 = ( 𝐹 ‘ 𝑜 ) ↔ 𝑝 = 𝑜 ) ) )
47 46 impr ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑜 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) ) → ( 𝑦 = ( 𝐹 ‘ 𝑜 ) ↔ 𝑝 = 𝑜 ) )
48 47 an32s ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) ) ∧ 𝑜 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑜 ) ↔ 𝑝 = 𝑜 ) )
49 30 48 bitr4d ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) ) ∧ 𝑜 ∈ 𝐴 ) → ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) )
50 49 ex ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) ) → ( 𝑜 ∈ 𝐴 → ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) )
51 50 ralrimiv ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑝 ) ) ) → ∀ 𝑜 ∈ 𝐴 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) )
52 51 exp32 ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑝 ∈ 𝐴 → ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ∀ 𝑜 ∈ 𝐴 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) ) )
53 9 10 52 rexlimd ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( ∃ 𝑝 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑝 ) → ∀ 𝑜 ∈ 𝐴 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) )
54 6 53 sylbid ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑦 ∈ ran 𝐹 → ∀ 𝑜 ∈ 𝐴 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) )
55 rsp ⊢ ( ∀ 𝑜 ∈ 𝐴 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) → ( 𝑜 ∈ 𝐴 → ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) )
56 54 55 syl6 ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑦 ∈ ran 𝐹 → ( 𝑜 ∈ 𝐴 → ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) ) )
57 56 com23 ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑜 ∈ 𝐴 → ( 𝑦 ∈ ran 𝐹 → ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) ) )
58 57 ralrimdv ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑜 ∈ 𝐴 → ∀ 𝑦 ∈ ran 𝐹 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) )
59 reu6i ⊢ ( ( ( 𝐹 ‘ 𝑜 ) ∈ ran 𝐹 ∧ ∀ 𝑦 ∈ ran 𝐹 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) ) → ∃! 𝑦 ∈ ran 𝐹 𝑜 ∈ 𝑦 )
60 59 ex ⊢ ( ( 𝐹 ‘ 𝑜 ) ∈ ran 𝐹 → ( ∀ 𝑦 ∈ ran 𝐹 ( 𝑜 ∈ 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑜 ) ) → ∃! 𝑦 ∈ ran 𝐹 𝑜 ∈ 𝑦 ) )
61 3 58 60 syl6c ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑜 ∈ 𝐴 → ∃! 𝑦 ∈ ran 𝐹 𝑜 ∈ 𝑦 ) )
62 61 ralrimiv ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ∀ 𝑜 ∈ 𝐴 ∃! 𝑦 ∈ ran 𝐹 𝑜 ∈ 𝑦 )
63 nfv ⊢ Ⅎ 𝑥 𝑞 = 𝑜
64 nfv ⊢ Ⅎ 𝑦 𝑞 = 𝑜
65 nfvd ⊢ ( 𝑞 = 𝑜 → Ⅎ 𝑦 𝑞 ∈ 𝑥 )
66 nfvd ⊢ ( 𝑞 = 𝑜 → Ⅎ 𝑥 𝑜 ∈ 𝑦 )
67 elequ12 ⊢ ( ( 𝑞 = 𝑜 ∧ 𝑥 = 𝑦 ) → ( 𝑞 ∈ 𝑥 ↔ 𝑜 ∈ 𝑦 ) )
68 67 ex ⊢ ( 𝑞 = 𝑜 → ( 𝑥 = 𝑦 → ( 𝑞 ∈ 𝑥 ↔ 𝑜 ∈ 𝑦 ) ) )
69 63 64 65 66 68 cbvreud ⊢ ( 𝑞 = 𝑜 → ( ∃! 𝑥 ∈ ran 𝐹 𝑞 ∈ 𝑥 ↔ ∃! 𝑦 ∈ ran 𝐹 𝑜 ∈ 𝑦 ) )
70 69 cbvralvw ⊢ ( ∀ 𝑞 ∈ 𝐴 ∃! 𝑥 ∈ ran 𝐹 𝑞 ∈ 𝑥 ↔ ∀ 𝑜 ∈ 𝐴 ∃! 𝑦 ∈ ran 𝐹 𝑜 ∈ 𝑦 )
71 62 70 sylibr ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ∀ 𝑞 ∈ 𝐴 ∃! 𝑥 ∈ ran 𝐹 𝑞 ∈ 𝑥 )