Theorem dffun2 5141

Description: Alternate definition of a function. (Contributed by NM, 29-Dec-1996.)

Assertion

Ref	Expression
dffun2	⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)))

Distinct variable group:   𝑥,𝑦,𝑧,𝐴

Proof of Theorem dffun2

Step	Hyp	Ref	Expression
1		df-fun 5133	. 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
2		df-id 4223	. . . . . 6 ⊢ I = {⟨𝑦, 𝑧⟩ ∣ 𝑦 = 𝑧}
3	2	sseq2i 3129	. . . . 5 ⊢ ((𝐴 ∘ ◡𝐴) ⊆ I ↔ (𝐴 ∘ ◡𝐴) ⊆ {⟨𝑦, 𝑧⟩ ∣ 𝑦 = 𝑧})
4		df-co 4556	. . . . . 6 ⊢ (𝐴 ∘ ◡𝐴) = {⟨𝑦, 𝑧⟩ ∣ ∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧)}
5	4	sseq1i 3128	. . . . 5 ⊢ ((𝐴 ∘ ◡𝐴) ⊆ {⟨𝑦, 𝑧⟩ ∣ 𝑦 = 𝑧} ↔ {⟨𝑦, 𝑧⟩ ∣ ∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧)} ⊆ {⟨𝑦, 𝑧⟩ ∣ 𝑦 = 𝑧})
6		ssopab2b 4206	. . . . 5 ⊢ ({⟨𝑦, 𝑧⟩ ∣ ∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧)} ⊆ {⟨𝑦, 𝑧⟩ ∣ 𝑦 = 𝑧} ↔ ∀𝑦∀𝑧(∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
7	3, 5, 6	3bitri 205	. . . 4 ⊢ ((𝐴 ∘ ◡𝐴) ⊆ I ↔ ∀𝑦∀𝑧(∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
8		vex 2692	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
9		vex 2692	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
10	8, 9	brcnv 4730	. . . . . . . . . . 11 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
11	10	anbi1i 454	. . . . . . . . . 10 ⊢ ((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) ↔ (𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧))
12	11	exbii 1585	. . . . . . . . 9 ⊢ (∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) ↔ ∃𝑥(𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧))
13	12	imbi1i 237	. . . . . . . 8 ⊢ ((∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ (∃𝑥(𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
14		19.23v 1856	. . . . . . . 8 ⊢ (∀𝑥((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ (∃𝑥(𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
15	13, 14	bitr4i 186	. . . . . . 7 ⊢ ((∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ ∀𝑥((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
16	15	albii 1447	. . . . . 6 ⊢ (∀𝑧(∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ ∀𝑧∀𝑥((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
17		alcom 1455	. . . . . 6 ⊢ (∀𝑧∀𝑥((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ ∀𝑥∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
18	16, 17	bitri 183	. . . . 5 ⊢ (∀𝑧(∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ ∀𝑥∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
19	18	albii 1447	. . . 4 ⊢ (∀𝑦∀𝑧(∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ ∀𝑦∀𝑥∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
20		alcom 1455	. . . 4 ⊢ (∀𝑦∀𝑥∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
21	7, 19, 20	3bitri 205	. . 3 ⊢ ((𝐴 ∘ ◡𝐴) ⊆ I ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
22	21	anbi2i 453	. 2 ⊢ ((Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ) ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)))
23	1, 22	bitri 183	1 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1330  ∃wex 1469   ⊆ wss 3076   class class class wbr 3937  {copab 3996   I cid 4218  ^◡ccnv 4546   ∘ ccom 4551  Rel wrel 4552  Fun wfun 5125

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106  ax-pr 4139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-br 3938  df-opab 3998  df-id 4223  df-cnv 4555  df-co 4556  df-fun 5133

This theorem is referenced by:  dffun4  5142  dffun6f  5144  sbcfung  5155  funcnveq  5194  fliftfun  5705  fclim  11095