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^{-1}}^{-1} \land Fun A^{-1}) \leftrightarrow \forall x \forall y \forall z \forall w ((x A y \land z A w) \to (x = z \leftrightarrow y = w))$

Proof

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

Metamath Proof Explorer

Theorem fun11

Proof