Theorem fun11 4966

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 368	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ↔ 𝑦 = 𝑤) ↔ ((𝑥 = 𝑧 → 𝑦 = 𝑤) ∧ (𝑦 = 𝑤 → 𝑥 = 𝑧)))
2	1	imbi2i 215	. . . . . . 7 ⊢ (((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)) ↔ ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → ((𝑥 = 𝑧 → 𝑦 = 𝑤) ∧ (𝑦 = 𝑤 → 𝑥 = 𝑧))))
3		pm4.76 536	. . . . . . 7 ⊢ ((((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 → 𝑦 = 𝑤)) ∧ ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑦 = 𝑤 → 𝑥 = 𝑧))) ↔ ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → ((𝑥 = 𝑧 → 𝑦 = 𝑤) ∧ (𝑦 = 𝑤 → 𝑥 = 𝑧))))
4		bi2.04 237	. . . . . . . 8 ⊢ (((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 → 𝑦 = 𝑤)) ↔ (𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)))
5		bi2.04 237	. . . . . . . 8 ⊢ (((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑦 = 𝑤 → 𝑥 = 𝑧)) ↔ (𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
6	4, 5	anbi12i 433	. . . . . . 7 ⊢ ((((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 → 𝑦 = 𝑤)) ∧ ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑦 = 𝑤 → 𝑥 = 𝑧))) ↔ ((𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ∧ (𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))))
7	2, 3, 6	3bitr2i 197	. . . . . 6 ⊢ (((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)) ↔ ((𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ∧ (𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))))
8	7	2albii 1360	. . . . 5 ⊢ (∀𝑥∀𝑦((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ∧ (𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))))
9		19.26-2 1371	. . . . 5 ⊢ (∀𝑥∀𝑦((𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ∧ (𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))) ↔ (∀𝑥∀𝑦(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ∧ ∀𝑥∀𝑦(𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))))
10		alcom 1367	. . . . . . 7 ⊢ (∀𝑥∀𝑦(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ↔ ∀𝑦∀𝑥(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)))
11		nfv 1421	. . . . . . . . 9 ⊢ Ⅎ𝑥((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)
12		breq1 3767	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑥𝐴𝑦 ↔ 𝑧𝐴𝑦))
13	12	anbi1d 438	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) ↔ (𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤)))
14	13	imbi1d 220	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ↔ ((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)))
15	11, 14	equsal 1615	. . . . . . . 8 ⊢ (∀𝑥(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ↔ ((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
16	15	albii 1359	. . . . . . 7 ⊢ (∀𝑦∀𝑥(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ↔ ∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
17	10, 16	bitri 173	. . . . . 6 ⊢ (∀𝑥∀𝑦(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ↔ ∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
18		nfv 1421	. . . . . . . 8 ⊢ Ⅎ𝑦((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)
19		breq2 3768	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑥𝐴𝑦 ↔ 𝑥𝐴𝑤))
20	19	anbi1d 438	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) ↔ (𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤)))
21	20	imbi1d 220	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧) ↔ ((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
22	18, 21	equsal 1615	. . . . . . 7 ⊢ (∀𝑦(𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)) ↔ ((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
23	22	albii 1359	. . . . . 6 ⊢ (∀𝑥∀𝑦(𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)) ↔ ∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
24	17, 23	anbi12i 433	. . . . 5 ⊢ ((∀𝑥∀𝑦(𝑥 = 𝑧 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤)) ∧ ∀𝑥∀𝑦(𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))) ↔ (∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
25	8, 9, 24	3bitri 195	. . . 4 ⊢ (∀𝑥∀𝑦((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)) ↔ (∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
26	25	2albii 1360	. . 3 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)) ↔ ∀𝑧∀𝑤(∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
27		19.26-2 1371	. . 3 ⊢ (∀𝑧∀𝑤(∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)) ↔ (∀𝑧∀𝑤∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑧∀𝑤∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
28	26, 27	bitr2i 174	. 2 ⊢ ((∀𝑧∀𝑤∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑧∀𝑤∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)) ↔ ∀𝑧∀𝑤∀𝑥∀𝑦((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)))
29		fun2cnv 4963	. . . 4 ⊢ (Fun ◡◡𝐴 ↔ ∀𝑧∃*𝑦 𝑧𝐴𝑦)
30		breq2 3768	. . . . . 6 ⊢ (𝑦 = 𝑤 → (𝑧𝐴𝑦 ↔ 𝑧𝐴𝑤))
31	30	mo4 1961	. . . . 5 ⊢ (∃*𝑦 𝑧𝐴𝑦 ↔ ∀𝑦∀𝑤((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
32	31	albii 1359	. . . 4 ⊢ (∀𝑧∃*𝑦 𝑧𝐴𝑦 ↔ ∀𝑧∀𝑦∀𝑤((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
33		alcom 1367	. . . . 5 ⊢ (∀𝑦∀𝑤((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ↔ ∀𝑤∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
34	33	albii 1359	. . . 4 ⊢ (∀𝑧∀𝑦∀𝑤((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ↔ ∀𝑧∀𝑤∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
35	29, 32, 34	3bitri 195	. . 3 ⊢ (Fun ◡◡𝐴 ↔ ∀𝑧∀𝑤∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤))
36		funcnv2 4959	. . . 4 ⊢ (Fun ◡𝐴 ↔ ∀𝑤∃*𝑥 𝑥𝐴𝑤)
37		breq1 3767	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑥𝐴𝑤 ↔ 𝑧𝐴𝑤))
38	37	mo4 1961	. . . . 5 ⊢ (∃*𝑥 𝑥𝐴𝑤 ↔ ∀𝑥∀𝑧((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
39	38	albii 1359	. . . 4 ⊢ (∀𝑤∃*𝑥 𝑥𝐴𝑤 ↔ ∀𝑤∀𝑥∀𝑧((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
40		alcom 1367	. . . . . 6 ⊢ (∀𝑥∀𝑧((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧) ↔ ∀𝑧∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
41	40	albii 1359	. . . . 5 ⊢ (∀𝑤∀𝑥∀𝑧((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧) ↔ ∀𝑤∀𝑧∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
42		alcom 1367	. . . . 5 ⊢ (∀𝑤∀𝑧∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧) ↔ ∀𝑧∀𝑤∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
43	41, 42	bitri 173	. . . 4 ⊢ (∀𝑤∀𝑥∀𝑧((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧) ↔ ∀𝑧∀𝑤∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
44	36, 39, 43	3bitri 195	. . 3 ⊢ (Fun ◡𝐴 ↔ ∀𝑧∀𝑤∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧))
45	35, 44	anbi12i 433	. 2 ⊢ ((Fun ◡◡𝐴 ∧ Fun ◡𝐴) ↔ (∀𝑧∀𝑤∀𝑦((𝑧𝐴𝑦 ∧ 𝑧𝐴𝑤) → 𝑦 = 𝑤) ∧ ∀𝑧∀𝑤∀𝑥((𝑥𝐴𝑤 ∧ 𝑧𝐴𝑤) → 𝑥 = 𝑧)))
46		alrot4 1375	. 2 ⊢ (∀𝑥∀𝑦∀𝑧∀𝑤((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)) ↔ ∀𝑧∀𝑤∀𝑥∀𝑦((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)))
47	28, 45, 46	3bitr4i 201	1 ⊢ ((Fun ◡◡𝐴 ∧ Fun ◡𝐴) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98  ∀wal 1241  ∃*wmo 1901   class class class wbr 3764  ^◡ccnv 4344  Fun wfun 4896

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-br 3765  df-opab 3819  df-id 4030  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-fun 4904

This theorem is referenced by: (None)