Metamath Proof Explorer

Theorem fun11

Description: Two ways of stating that A is one-to-one (but not necessarily a function). Each side is equivalent to Definition 6.4(3) of TakeutiZaring p. 24, who use the notation "Un_2 (A)" for one-to-one (but not necessarily a function). (Contributed by NM, 17-Jan-2006)

Ref Expression
Assertion fun11 
|- ( ( Fun `' `' A /\ Fun `' A ) <-> A. x A. y A. z A. w ( ( x A y /\ z A w ) -> ( x = z <-> y = w ) ) )

Proof

Step Hyp Ref Expression
1 dfbi2 
 |-  ( ( x = z <-> y = w ) <-> ( ( x = z -> y = w ) /\ ( y = w -> x = z ) ) )
2 1 imbi2i 
 |-  ( ( ( x A y /\ z A w ) -> ( x = z <-> y = w ) ) <-> ( ( x A y /\ z A w ) -> ( ( x = z -> y = w ) /\ ( y = w -> x = z ) ) ) )
3 pm4.76 
 |-  ( ( ( ( x A y /\ z A w ) -> ( x = z -> y = w ) ) /\ ( ( x A y /\ z A w ) -> ( y = w -> x = z ) ) ) <-> ( ( x A y /\ z A w ) -> ( ( x = z -> y = w ) /\ ( y = w -> x = z ) ) ) )
4 bi2.04 
 |-  ( ( ( x A y /\ z A w ) -> ( x = z -> y = w ) ) <-> ( x = z -> ( ( x A y /\ z A w ) -> y = w ) ) )
5 bi2.04 
 |-  ( ( ( x A y /\ z A w ) -> ( y = w -> x = z ) ) <-> ( y = w -> ( ( x A y /\ z A w ) -> x = z ) ) )
6 4 5 anbi12i 
 |-  ( ( ( ( x A y /\ z A w ) -> ( x = z -> y = w ) ) /\ ( ( x A y /\ z A w ) -> ( y = w -> x = z ) ) ) <-> ( ( x = z -> ( ( x A y /\ z A w ) -> y = w ) ) /\ ( y = w -> ( ( x A y /\ z A w ) -> x = z ) ) ) )
7 2 3 6 3bitr2i 
 |-  ( ( ( x A y /\ z A w ) -> ( x = z <-> y = w ) ) <-> ( ( x = z -> ( ( x A y /\ z A w ) -> y = w ) ) /\ ( y = w -> ( ( x A y /\ z A w ) -> x = z ) ) ) )
8 7 2albii 
 |-  ( A. x A. y ( ( x A y /\ z A w ) -> ( x = z <-> y = w ) ) <-> A. x A. y ( ( x = z -> ( ( x A y /\ z A w ) -> y = w ) ) /\ ( y = w -> ( ( x A y /\ z A w ) -> x = z ) ) ) )
9 19.26-2 
 |-  ( A. x A. y ( ( x = z -> ( ( x A y /\ z A w ) -> y = w ) ) /\ ( y = w -> ( ( x A y /\ z A w ) -> x = z ) ) ) <-> ( A. x A. y ( x = z -> ( ( x A y /\ z A w ) -> y = w ) ) /\ A. x A. y ( y = w -> ( ( x A y /\ z A w ) -> x = z ) ) ) )
10 alcom 
 |-  ( A. x A. y ( x = z -> ( ( x A y /\ z A w ) -> y = w ) ) <-> A. y A. x ( x = z -> ( ( x A y /\ z A w ) -> y = w ) ) )
11 breq1 
 |-  ( x = z -> ( x A y <-> z A y ) )
12 11 anbi1d 
 |-  ( x = z -> ( ( x A y /\ z A w ) <-> ( z A y /\ z A w ) ) )
13 12 imbi1d 
 |-  ( x = z -> ( ( ( x A y /\ z A w ) -> y = w ) <-> ( ( z A y /\ z A w ) -> y = w ) ) )
14 13 equsalvw 
 |-  ( A. x ( x = z -> ( ( x A y /\ z A w ) -> y = w ) ) <-> ( ( z A y /\ z A w ) -> y = w ) )
15 14 albii 
 |-  ( A. y A. x ( x = z -> ( ( x A y /\ z A w ) -> y = w ) ) <-> A. y ( ( z A y /\ z A w ) -> y = w ) )
16 10 15 bitri 
 |-  ( A. x A. y ( x = z -> ( ( x A y /\ z A w ) -> y = w ) ) <-> A. y ( ( z A y /\ z A w ) -> y = w ) )
17 breq2 
 |-  ( y = w -> ( x A y <-> x A w ) )
18 17 anbi1d 
 |-  ( y = w -> ( ( x A y /\ z A w ) <-> ( x A w /\ z A w ) ) )
19 18 imbi1d 
 |-  ( y = w -> ( ( ( x A y /\ z A w ) -> x = z ) <-> ( ( x A w /\ z A w ) -> x = z ) ) )
20 19 equsalvw 
 |-  ( A. y ( y = w -> ( ( x A y /\ z A w ) -> x = z ) ) <-> ( ( x A w /\ z A w ) -> x = z ) )
21 20 albii 
 |-  ( A. x A. y ( y = w -> ( ( x A y /\ z A w ) -> x = z ) ) <-> A. x ( ( x A w /\ z A w ) -> x = z ) )
22 16 21 anbi12i 
 |-  ( ( A. x A. y ( x = z -> ( ( x A y /\ z A w ) -> y = w ) ) /\ A. x A. y ( y = w -> ( ( x A y /\ z A w ) -> x = z ) ) ) <-> ( A. y ( ( z A y /\ z A w ) -> y = w ) /\ A. x ( ( x A w /\ z A w ) -> x = z ) ) )
23 8 9 22 3bitri 
 |-  ( A. x A. y ( ( x A y /\ z A w ) -> ( x = z <-> y = w ) ) <-> ( A. y ( ( z A y /\ z A w ) -> y = w ) /\ A. x ( ( x A w /\ z A w ) -> x = z ) ) )
24 23 2albii 
 |-  ( A. z A. w A. x A. y ( ( x A y /\ z A w ) -> ( x = z <-> y = w ) ) <-> A. z A. w ( A. y ( ( z A y /\ z A w ) -> y = w ) /\ A. x ( ( x A w /\ z A w ) -> x = z ) ) )
25 19.26-2 
 |-  ( A. z A. w ( A. y ( ( z A y /\ z A w ) -> y = w ) /\ A. x ( ( x A w /\ z A w ) -> x = z ) ) <-> ( A. z A. w A. y ( ( z A y /\ z A w ) -> y = w ) /\ A. z A. w A. x ( ( x A w /\ z A w ) -> x = z ) ) )
26 24 25 bitr2i 
 |-  ( ( A. z A. w A. y ( ( z A y /\ z A w ) -> y = w ) /\ A. z A. w A. x ( ( x A w /\ z A w ) -> x = z ) ) <-> A. z A. w A. x A. y ( ( x A y /\ z A w ) -> ( x = z <-> y = w ) ) )
27 fun2cnv 
 |-  ( Fun `' `' A <-> A. z E* y z A y )
28 breq2 
 |-  ( y = w -> ( z A y <-> z A w ) )
29 28 mo4 
 |-  ( E* y z A y <-> A. y A. w ( ( z A y /\ z A w ) -> y = w ) )
30 29 albii 
 |-  ( A. z E* y z A y <-> A. z A. y A. w ( ( z A y /\ z A w ) -> y = w ) )
31 alcom 
 |-  ( A. y A. w ( ( z A y /\ z A w ) -> y = w ) <-> A. w A. y ( ( z A y /\ z A w ) -> y = w ) )
32 31 albii 
 |-  ( A. z A. y A. w ( ( z A y /\ z A w ) -> y = w ) <-> A. z A. w A. y ( ( z A y /\ z A w ) -> y = w ) )
33 27 30 32 3bitri 
 |-  ( Fun `' `' A <-> A. z A. w A. y ( ( z A y /\ z A w ) -> y = w ) )
34 funcnv2 
 |-  ( Fun `' A <-> A. w E* x x A w )
35 breq1 
 |-  ( x = z -> ( x A w <-> z A w ) )
36 35 mo4 
 |-  ( E* x x A w <-> A. x A. z ( ( x A w /\ z A w ) -> x = z ) )
37 36 albii 
 |-  ( A. w E* x x A w <-> A. w A. x A. z ( ( x A w /\ z A w ) -> x = z ) )
38 alcom 
 |-  ( A. x A. z ( ( x A w /\ z A w ) -> x = z ) <-> A. z A. x ( ( x A w /\ z A w ) -> x = z ) )
39 38 albii 
 |-  ( A. w A. x A. z ( ( x A w /\ z A w ) -> x = z ) <-> A. w A. z A. x ( ( x A w /\ z A w ) -> x = z ) )
40 alcom 
 |-  ( A. w A. z A. x ( ( x A w /\ z A w ) -> x = z ) <-> A. z A. w A. x ( ( x A w /\ z A w ) -> x = z ) )
41 39 40 bitri 
 |-  ( A. w A. x A. z ( ( x A w /\ z A w ) -> x = z ) <-> A. z A. w A. x ( ( x A w /\ z A w ) -> x = z ) )
42 34 37 41 3bitri 
 |-  ( Fun `' A <-> A. z A. w A. x ( ( x A w /\ z A w ) -> x = z ) )
43 33 42 anbi12i 
 |-  ( ( Fun `' `' A /\ Fun `' A ) <-> ( A. z A. w A. y ( ( z A y /\ z A w ) -> y = w ) /\ A. z A. w A. x ( ( x A w /\ z A w ) -> x = z ) ) )
44 alrot4 
 |-  ( A. x A. y A. z A. w ( ( x A y /\ z A w ) -> ( x = z <-> y = w ) ) <-> A. z A. w A. x A. y ( ( x A y /\ z A w ) -> ( x = z <-> y = w ) ) )
45 26 43 44 3bitr4i 
 |-  ( ( Fun `' `' A /\ Fun `' A ) <-> A. x A. y A. z A. w ( ( x A y /\ z A w ) -> ( x = z <-> y = w ) ) )