Metamath Proof Explorer

Theorem dff3

Description: Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007)

Ref Expression
Assertion dff3 ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) )

Proof

Step Hyp Ref Expression
1 fssxp ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 ⊆ ( 𝐴 × 𝐵 ) )
2 ffun ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Fun 𝐹 )
3 fdm ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
4 3 eleq2d ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴 ) )
5 4 biimpar ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝐹 )
6 funfvop ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 )
7 2 5 6 syl2an2r ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 )
8 df-br ⊢ ( 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) ↔ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 )
9 7 8 sylibr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) )
10 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
11 breq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑥 𝐹 𝑦 ↔ 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) ) )
12 10 11 spcev ⊢ ( 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) → ∃ 𝑦 𝑥 𝐹 𝑦 )
13 9 12 syl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 𝑥 𝐹 𝑦 )
14 funmo ⊢ ( Fun 𝐹 → ∃* 𝑦 𝑥 𝐹 𝑦 )
15 2 14 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ∃* 𝑦 𝑥 𝐹 𝑦 )
16 15 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ∃* 𝑦 𝑥 𝐹 𝑦 )
17 df-eu ⊢ ( ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ( ∃ 𝑦 𝑥 𝐹 𝑦 ∧ ∃* 𝑦 𝑥 𝐹 𝑦 ) )
18 13 16 17 sylanbrc ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑦 𝑥 𝐹 𝑦 )
19 18 ralrimiva ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 )
20 1 19 jca ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) )
21 xpss ⊢ ( 𝐴 × 𝐵 ) ⊆ ( V × V )
22 sstr ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝐴 × 𝐵 ) ⊆ ( V × V ) ) → 𝐹 ⊆ ( V × V ) )
23 21 22 mpan2 ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → 𝐹 ⊆ ( V × V ) )
24 df-rel ⊢ ( Rel 𝐹 ↔ 𝐹 ⊆ ( V × V ) )
25 23 24 sylibr ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → Rel 𝐹 )
26 25 adantr ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) → Rel 𝐹 )
27 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃! 𝑦 𝑥 𝐹 𝑦 ) )
28 eumo ⊢ ( ∃! 𝑦 𝑥 𝐹 𝑦 → ∃* 𝑦 𝑥 𝐹 𝑦 )
29 28 imim2i ⊢ ( ( 𝑥 ∈ 𝐴 → ∃! 𝑦 𝑥 𝐹 𝑦 ) → ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑥 𝐹 𝑦 ) )
30 29 adantl ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 → ∃! 𝑦 𝑥 𝐹 𝑦 ) ) → ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑥 𝐹 𝑦 ) )
31 df-br ⊢ ( 𝑥 𝐹 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
32 ssel ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
33 31 32 biimtrid ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑥 𝐹 𝑦 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
34 opelxp1 ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → 𝑥 ∈ 𝐴 )
35 33 34 syl6 ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑥 𝐹 𝑦 → 𝑥 ∈ 𝐴 ) )
36 35 exlimdv ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ∃ 𝑦 𝑥 𝐹 𝑦 → 𝑥 ∈ 𝐴 ) )
37 36 con3d ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ¬ 𝑥 ∈ 𝐴 → ¬ ∃ 𝑦 𝑥 𝐹 𝑦 ) )
38 nexmo ⊢ ( ¬ ∃ 𝑦 𝑥 𝐹 𝑦 → ∃* 𝑦 𝑥 𝐹 𝑦 )
39 37 38 syl6 ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ¬ 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑥 𝐹 𝑦 ) )
40 39 adantr ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 → ∃! 𝑦 𝑥 𝐹 𝑦 ) ) → ( ¬ 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑥 𝐹 𝑦 ) )
41 30 40 pm2.61d ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 → ∃! 𝑦 𝑥 𝐹 𝑦 ) ) → ∃* 𝑦 𝑥 𝐹 𝑦 )
42 41 ex ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ( 𝑥 ∈ 𝐴 → ∃! 𝑦 𝑥 𝐹 𝑦 ) → ∃* 𝑦 𝑥 𝐹 𝑦 ) )
43 42 alimdv ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃! 𝑦 𝑥 𝐹 𝑦 ) → ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 ) )
44 27 43 biimtrid ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 → ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 ) )
45 44 imp ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) → ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 )
46 dffun6 ⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 ) )
47 26 45 46 sylanbrc ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) → Fun 𝐹 )
48 dmss ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → dom 𝐹 ⊆ dom ( 𝐴 × 𝐵 ) )
49 dmxpss ⊢ dom ( 𝐴 × 𝐵 ) ⊆ 𝐴
50 48 49 sstrdi ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → dom 𝐹 ⊆ 𝐴 )
51 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝐹 𝑦 ↔ 𝑧 𝐹 𝑦 ) )
52 51 eubidv ⊢ ( 𝑥 = 𝑧 → ( ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ∃! 𝑦 𝑧 𝐹 𝑦 ) )
53 52 rspccv ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 → ( 𝑧 ∈ 𝐴 → ∃! 𝑦 𝑧 𝐹 𝑦 ) )
54 euex ⊢ ( ∃! 𝑦 𝑧 𝐹 𝑦 → ∃ 𝑦 𝑧 𝐹 𝑦 )
55 vex ⊢ 𝑧 ∈ V
56 55 eldm ⊢ ( 𝑧 ∈ dom 𝐹 ↔ ∃ 𝑦 𝑧 𝐹 𝑦 )
57 54 56 sylibr ⊢ ( ∃! 𝑦 𝑧 𝐹 𝑦 → 𝑧 ∈ dom 𝐹 )
58 53 57 syl6 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ dom 𝐹 ) )
59 58 ssrdv ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 → 𝐴 ⊆ dom 𝐹 )
60 50 59 anim12i ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) → ( dom 𝐹 ⊆ 𝐴 ∧ 𝐴 ⊆ dom 𝐹 ) )
61 eqss ⊢ ( dom 𝐹 = 𝐴 ↔ ( dom 𝐹 ⊆ 𝐴 ∧ 𝐴 ⊆ dom 𝐹 ) )
62 60 61 sylibr ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) → dom 𝐹 = 𝐴 )
63 df-fn ⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) )
64 47 62 63 sylanbrc ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) → 𝐹 Fn 𝐴 )
65 rnss ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ran 𝐹 ⊆ ran ( 𝐴 × 𝐵 ) )
66 rnxpss ⊢ ran ( 𝐴 × 𝐵 ) ⊆ 𝐵
67 65 66 sstrdi ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ran 𝐹 ⊆ 𝐵 )
68 67 adantr ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) → ran 𝐹 ⊆ 𝐵 )
69 df-f ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
70 64 68 69 sylanbrc ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
71 20 70 impbii ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) )