Theorem fun11 5265

Description: Two ways of stating that 𝐴 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₂ (A)" for one-to-one (but not necessarily a function). (Contributed by NM, 17-Jan-2006.)

Assertion

Ref	Expression
fun11	⊢ ((Fun ◡◡𝐴 ∧ Fun ◡𝐴) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)))

Distinct variable group:   𝑥,𝑦,𝑧,𝑤,𝐴

Proof of Theorem fun11

Step	Hyp	Ref	Expression
1		dfbi2 386	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ↔ 𝑦 = 𝑤) ↔ ((𝑥 = 𝑧 → 𝑦 = 𝑤) ∧ (𝑦 = 𝑤 → 𝑥 = 𝑧)))
2	1	imbi2i 225	. . . . . . 7 ⊢ (((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)) ↔ ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → ((𝑥 = 𝑧 → 𝑦 = 𝑤) ∧ (𝑦 = 𝑤 → 𝑥 = 𝑧))))
3		pm4.76 599	. . . . . . 7 ⊢ ((((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 → 𝑦 = 𝑤)) ∧ ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑦 = 𝑤 → 𝑥 = 𝑧))) ↔ ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → ((𝑥 = 𝑧 → 𝑦 = 𝑤) ∧ (𝑦 = 𝑤 → 𝑥 = 𝑧))))
4		bi2.04 247	. . . . . . . 8 ⊢ (((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 → 𝑦 = 𝑤)) ↔ (𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)))
5		bi2.04 247	. . . . . . . 8 ⊢ (((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑦 = 𝑤 → 𝑥 = 𝑧)) ↔ (𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
6	4, 5	anbi12i 457	. . . . . . 7 ⊢ ((((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 → 𝑦 = 𝑤)) ∧ ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑦 = 𝑤 → 𝑥 = 𝑧))) ↔ ((𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ∧ (𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))))
7	2, 3, 6	3bitr2i 207	. . . . . 6 ⊢ (((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)) ↔ ((𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ∧ (𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))))
8	7	2albii 1464	. . . . 5 ⊢ (∀𝑥∀𝑦((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ∧ (𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))))
9		19.26-2 1475	. . . . 5 ⊢ (∀𝑥∀𝑦((𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ∧ (𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))) ↔ (∀𝑥∀𝑦(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ∧ ∀𝑥∀𝑦(𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))))
10		alcom 1471	. . . . . . 7 ⊢ (∀𝑥∀𝑦(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ↔ ∀𝑦∀𝑥(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)))
11		nfv 1521	. . . . . . . . 9 ⊢ Ⅎ𝑥((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)
12		breq1 3992	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑥𝐴𝑦 ↔ 𝑧𝐴𝑦))
13	12	anbi1d 462	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) ↔ (𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤)))
14	13	imbi1d 230	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ↔ ((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)))
15	11, 14	equsal 1720	. . . . . . . 8 ⊢ (∀𝑥(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ↔ ((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
16	15	albii 1463	. . . . . . 7 ⊢ (∀𝑦∀𝑥(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ↔ ∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
17	10, 16	bitri 183	. . . . . 6 ⊢ (∀𝑥∀𝑦(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ↔ ∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
18		nfv 1521	. . . . . . . 8 ⊢ Ⅎ𝑦((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)
19		breq2 3993	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑥𝐴𝑦 ↔ 𝑥𝐴𝑤))
20	19	anbi1d 462	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) ↔ (𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤)))
21	20	imbi1d 230	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧) ↔ ((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
22	18, 21	equsal 1720	. . . . . . 7 ⊢ (∀𝑦(𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)) ↔ ((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
23	22	albii 1463	. . . . . 6 ⊢ (∀𝑥∀𝑦(𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)) ↔ ∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
24	17, 23	anbi12i 457	. . . . 5 ⊢ ((∀𝑥∀𝑦(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ∧ ∀𝑥∀𝑦(𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))) ↔ (∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
25	8, 9, 24	3bitri 205	. . . 4 ⊢ (∀𝑥∀𝑦((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)) ↔ (∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
26	25	2albii 1464	. . 3 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)) ↔ ∀𝑧∀𝑤(∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
27		19.26-2 1475	. . 3 ⊢ (∀𝑧∀𝑤(∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)) ↔ (∀𝑧∀𝑤∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑧∀𝑤∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
28	26, 27	bitr2i 184	. 2 ⊢ ((∀𝑧∀𝑤∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑧∀𝑤∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)) ↔ ∀𝑧∀𝑤∀𝑥∀𝑦((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)))
29		fun2cnv 5262	. . . 4 ⊢ (Fun ◡◡𝐴 ↔ ∀𝑧∃*𝑦 𝑧𝐴𝑦)
30		breq2 3993	. . . . . 6 ⊢ (𝑦 = 𝑤 → (𝑧𝐴𝑦 ↔ 𝑧𝐴𝑤))
31	30	mo4 2080	. . . . 5 ⊢ (∃*𝑦 𝑧𝐴𝑦 ↔ ∀𝑦∀𝑤((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
32	31	albii 1463	. . . 4 ⊢ (∀𝑧∃*𝑦 𝑧𝐴𝑦 ↔ ∀𝑧∀𝑦∀𝑤((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
33		alcom 1471	. . . . 5 ⊢ (∀𝑦∀𝑤((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ↔ ∀𝑤∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
34	33	albii 1463	. . . 4 ⊢ (∀𝑧∀𝑦∀𝑤((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ↔ ∀𝑧∀𝑤∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
35	29, 32, 34	3bitri 205	. . 3 ⊢ (Fun ◡◡𝐴 ↔ ∀𝑧∀𝑤∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
36		funcnv2 5258	. . . 4 ⊢ (Fun ◡𝐴 ↔ ∀𝑤∃*𝑥 𝑥𝐴𝑤)
37		breq1 3992	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑥𝐴𝑤 ↔ 𝑧𝐴𝑤))
38	37	mo4 2080	. . . . 5 ⊢ (∃*𝑥 𝑥𝐴𝑤 ↔ ∀𝑥∀𝑧((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
39	38	albii 1463	. . . 4 ⊢ (∀𝑤∃*𝑥 𝑥𝐴𝑤 ↔ ∀𝑤∀𝑥∀𝑧((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
40		alcom 1471	. . . . . 6 ⊢ (∀𝑥∀𝑧((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧) ↔ ∀𝑧∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
41	40	albii 1463	. . . . 5 ⊢ (∀𝑤∀𝑥∀𝑧((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧) ↔ ∀𝑤∀𝑧∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
42		alcom 1471	. . . . 5 ⊢ (∀𝑤∀𝑧∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧) ↔ ∀𝑧∀𝑤∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
43	41, 42	bitri 183	. . . 4 ⊢ (∀𝑤∀𝑥∀𝑧((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧) ↔ ∀𝑧∀𝑤∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
44	36, 39, 43	3bitri 205	. . 3 ⊢ (Fun ◡𝐴 ↔ ∀𝑧∀𝑤∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
45	35, 44	anbi12i 457	. 2 ⊢ ((Fun ◡◡𝐴 ∧ Fun ◡𝐴) ↔ (∀𝑧∀𝑤∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑧∀𝑤∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
46		alrot4 1479	. 2 ⊢ (∀𝑥∀𝑦∀𝑧∀𝑤((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)) ↔ ∀𝑧∀𝑤∀𝑥∀𝑦((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)))
47	28, 45, 46	3bitr4i 211	1 ⊢ ((Fun ◡◡𝐴 ∧ Fun ◡𝐴) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1346  ∃*wmo 2020   class class class wbr 3989  ^◡ccnv 4610  Fun wfun 5192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990  df-opab 4051  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-fun 5200

This theorem is referenced by: (None)