funcnv - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > funcnv		GIF version

Theorem funcnv 5184

Description: The converse of a class is a function iff the class is single-rooted, which means that for any 𝑦 in the range of 𝐴 there is at most one 𝑥 such that 𝑥𝐴𝑦. Definition of single-rooted in [Enderton] p. 43. See funcnv2 5183 for a simpler version. (Contributed by NM, 13-Aug-2004.)

**Assertion**
Ref	Expression
funcnv	⊢ (Fun ^◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃*𝑥 𝑥𝐴𝑦)

Distinct variable group: 𝑥,𝑦,𝐴

**Proof of Theorem funcnv**
Step	Hyp	Ref	Expression
1		vex 2689	. . . . . . 7 ⊢ 𝑥 ∈ V
2		vex 2689	. . . . . . 7 ⊢ 𝑦 ∈ V
3	1, 2	brelrn 4772	. . . . . 6 ⊢ (𝑥𝐴𝑦 → 𝑦 ∈ ran 𝐴)
4	3	pm4.71ri 389	. . . . 5 ⊢ (𝑥𝐴𝑦 ↔ (𝑦 ∈ ran 𝐴 ∧ 𝑥𝐴𝑦))
5	4	mobii 2036	. . . 4 ⊢ (∃𝑥 𝑥𝐴𝑦 ↔ ∃𝑥(𝑦 ∈ ran 𝐴 ∧ 𝑥𝐴𝑦))
6		moanimv 2074	. . . 4 ⊢ (∃𝑥(𝑦 ∈ ran 𝐴 ∧ 𝑥𝐴𝑦) ↔ (𝑦 ∈ ran 𝐴 → ∃𝑥 𝑥𝐴𝑦))
7	5, 6	bitri 183	. . 3 ⊢ (∃𝑥 𝑥𝐴𝑦 ↔ (𝑦 ∈ ran 𝐴 → ∃𝑥 𝑥𝐴𝑦))
8	7	albii 1446	. 2 ⊢ (∀𝑦∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(𝑦 ∈ ran 𝐴 → ∃𝑥 𝑥𝐴𝑦))
9		funcnv2 5183	. 2 ⊢ (Fun ^◡𝐴 ↔ ∀𝑦∃*𝑥 𝑥𝐴𝑦)
10		df-ral 2421	. 2 ⊢ (∀𝑦 ∈ ran 𝐴∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(𝑦 ∈ ran 𝐴 → ∃𝑥 𝑥𝐴𝑦))
11	8, 9, 10	3bitr4i 211	1 ⊢ (Fun ^◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃*𝑥 𝑥𝐴𝑦)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∀wal 1329 ∈ wcel 1480 ∃*wmo 2000 ∀wral 2416 class class class wbr 3929 ^◡ccnv 4538 ran crn 4540 Fun wfun 5117

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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-pow 4098 ax-pr 4131

This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ral 2421 df-rex 2422 df-v 2688 df-un 3075 df-in 3077 df-ss 3084 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-br 3930 df-opab 3990 df-id 4215 df-xp 4545 df-rel 4546 df-cnv 4547 df-co 4548 df-dm 4549 df-rn 4550 df-fun 5125

This theorem is referenced by: funcnv3 5185 fncnv 5189

W3C validator