Metamath Proof Explorer

Theorem dff1o6

Description: A one-to-one onto function in terms of function values. (Contributed by NM, 29-Mar-2008)

Ref Expression
Assertion dff1o6 ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)$

Proof

Step Hyp Ref Expression
1 df-f1o ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {F}:{A}\underset{onto}{⟶}{B}\right)$
2 dff13 ${⊢}{F}:{A}\underset{1-1}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)$
3 df-fo ${⊢}{F}:{A}\underset{onto}{⟶}{B}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)$
4 2 3 anbi12i ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {F}:{A}\underset{onto}{⟶}{B}\right)↔\left(\left({F}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)\wedge \left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)\right)$
5 df-3an ${⊢}\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)↔\left(\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)$
6 eqimss ${⊢}\mathrm{ran}{F}={B}\to \mathrm{ran}{F}\subseteq {B}$
7 6 anim2i ${⊢}\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)\to \left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {B}\right)$
8 df-f ${⊢}{F}:{A}⟶{B}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {B}\right)$
9 7 8 sylibr ${⊢}\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)\to {F}:{A}⟶{B}$
10 9 pm4.71ri ${⊢}\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)↔\left({F}:{A}⟶{B}\wedge \left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)\right)$
11 10 anbi1i ${⊢}\left(\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)↔\left(\left({F}:{A}⟶{B}\wedge \left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)$
12 an32 ${⊢}\left(\left({F}:{A}⟶{B}\wedge \left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)↔\left(\left({F}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)\wedge \left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)\right)$
13 5 11 12 3bitrri ${⊢}\left(\left({F}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)\wedge \left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)\right)↔\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)$
14 1 4 13 3bitri ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)$