This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funcnv5mpt

Description: Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 1-Mar-2017)

Ref Expression
Hypotheses funcnvmpt.0 
|- F/ x ph
funcnvmpt.1 
|- F/_ x A
funcnvmpt.2 
|- F/_ x F
funcnvmpt.3 
|- F = ( x e. A |-> B )
funcnvmpt.4 
|- ( ( ph /\ x e. A ) -> B e. V )
funcnv5mpt.1 
|- ( x = z -> B = C )
Assertion funcnv5mpt 
|- ( ph -> ( Fun `' F <-> A. x e. A A. z e. A ( x = z \/ B =/= C ) ) )

Proof

Step Hyp Ref Expression
1 funcnvmpt.0 
 |-  F/ x ph
2 funcnvmpt.1 
 |-  F/_ x A
3 funcnvmpt.2 
 |-  F/_ x F
4 funcnvmpt.3 
 |-  F = ( x e. A |-> B )
5 funcnvmpt.4 
 |-  ( ( ph /\ x e. A ) -> B e. V )
6 funcnv5mpt.1 
 |-  ( x = z -> B = C )
7 1 2 3 4 5 funcnvmpt 
 |-  ( ph -> ( Fun `' F <-> A. y E* x e. A y = B ) )
8 nne 
 |-  ( -. B =/= C <-> B = C )
9 eqvincg 
 |-  ( B e. V -> ( B = C <-> E. y ( y = B /\ y = C ) ) )
10 5 9 syl 
 |-  ( ( ph /\ x e. A ) -> ( B = C <-> E. y ( y = B /\ y = C ) ) )
11 8 10 bitrid 
 |-  ( ( ph /\ x e. A ) -> ( -. B =/= C <-> E. y ( y = B /\ y = C ) ) )
12 11 imbi1d 
 |-  ( ( ph /\ x e. A ) -> ( ( -. B =/= C -> x = z ) <-> ( E. y ( y = B /\ y = C ) -> x = z ) ) )
13 orcom 
 |-  ( ( x = z \/ B =/= C ) <-> ( B =/= C \/ x = z ) )
14 df-or 
 |-  ( ( B =/= C \/ x = z ) <-> ( -. B =/= C -> x = z ) )
15 13 14 bitri 
 |-  ( ( x = z \/ B =/= C ) <-> ( -. B =/= C -> x = z ) )
16 19.23v 
 |-  ( A. y ( ( y = B /\ y = C ) -> x = z ) <-> ( E. y ( y = B /\ y = C ) -> x = z ) )
17 12 15 16 3bitr4g 
 |-  ( ( ph /\ x e. A ) -> ( ( x = z \/ B =/= C ) <-> A. y ( ( y = B /\ y = C ) -> x = z ) ) )
18 17 ralbidv 
 |-  ( ( ph /\ x e. A ) -> ( A. z e. A ( x = z \/ B =/= C ) <-> A. z e. A A. y ( ( y = B /\ y = C ) -> x = z ) ) )
19 ralcom4 
 |-  ( A. z e. A A. y ( ( y = B /\ y = C ) -> x = z ) <-> A. y A. z e. A ( ( y = B /\ y = C ) -> x = z ) )
20 18 19 bitrdi 
 |-  ( ( ph /\ x e. A ) -> ( A. z e. A ( x = z \/ B =/= C ) <-> A. y A. z e. A ( ( y = B /\ y = C ) -> x = z ) ) )
21 1 20 ralbida 
 |-  ( ph -> ( A. x e. A A. z e. A ( x = z \/ B =/= C ) <-> A. x e. A A. y A. z e. A ( ( y = B /\ y = C ) -> x = z ) ) )
22 nfcv 
 |-  F/_ z A
23 nfv 
 |-  F/ x y = C
24 6 eqeq2d 
 |-  ( x = z -> ( y = B <-> y = C ) )
25 2 22 23 24 rmo4f 
 |-  ( E* x e. A y = B <-> A. x e. A A. z e. A ( ( y = B /\ y = C ) -> x = z ) )
26 25 albii 
 |-  ( A. y E* x e. A y = B <-> A. y A. x e. A A. z e. A ( ( y = B /\ y = C ) -> x = z ) )
27 ralcom4 
 |-  ( A. x e. A A. y A. z e. A ( ( y = B /\ y = C ) -> x = z ) <-> A. y A. x e. A A. z e. A ( ( y = B /\ y = C ) -> x = z ) )
28 26 27 bitr4i 
 |-  ( A. y E* x e. A y = B <-> A. x e. A A. y A. z e. A ( ( y = B /\ y = C ) -> x = z ) )
29 21 28 bitr4di 
 |-  ( ph -> ( A. x e. A A. z e. A ( x = z \/ B =/= C ) <-> A. y E* x e. A y = B ) )
30 7 29 bitr4d 
 |-  ( ph -> ( Fun `' F <-> A. x e. A A. z e. A ( x = z \/ B =/= C ) ) )