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

Theorem fncnv 4993
 Description: Single-rootedness (see funcnv 4988) of a class cut down by a cross product. (Contributed by NM, 5-Mar-2007.)
Assertion
Ref Expression
fncnv ((𝑅 ∩ (𝐴 × 𝐵)) Fn 𝐵 ↔ ∀𝑦𝐵 ∃!𝑥𝐴 𝑥𝑅𝑦)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦

Proof of Theorem fncnv
StepHypRef Expression
1 df-fn 4933 . 2 ((𝑅 ∩ (𝐴 × 𝐵)) Fn 𝐵 ↔ (Fun (𝑅 ∩ (𝐴 × 𝐵)) ∧ dom (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵))
2 df-rn 4384 . . . 4 ran (𝑅 ∩ (𝐴 × 𝐵)) = dom (𝑅 ∩ (𝐴 × 𝐵))
32eqeq1i 2063 . . 3 (ran (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ dom (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵)
43anbi2i 438 . 2 ((Fun (𝑅 ∩ (𝐴 × 𝐵)) ∧ ran (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵) ↔ (Fun (𝑅 ∩ (𝐴 × 𝐵)) ∧ dom (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵))
5 rninxp 4792 . . . . 5 (ran (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ ∀𝑦𝐵𝑥𝐴 𝑥𝑅𝑦)
65anbi1i 439 . . . 4 ((ran (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵 ∧ ∀𝑦𝐵 ∃*𝑥𝐴 𝑥𝑅𝑦) ↔ (∀𝑦𝐵𝑥𝐴 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 ∃*𝑥𝐴 𝑥𝑅𝑦))
7 funcnv 4988 . . . . . 6 (Fun (𝑅 ∩ (𝐴 × 𝐵)) ↔ ∀𝑦 ∈ ran (𝑅 ∩ (𝐴 × 𝐵))∃*𝑥 𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦)
8 raleq 2522 . . . . . . 7 (ran (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵 → (∀𝑦 ∈ ran (𝑅 ∩ (𝐴 × 𝐵))∃*𝑥 𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦 ↔ ∀𝑦𝐵 ∃*𝑥 𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦))
9 biimt 234 . . . . . . . . 9 (𝑦𝐵 → (∃*𝑥𝐴 𝑥𝑅𝑦 ↔ (𝑦𝐵 → ∃*𝑥𝐴 𝑥𝑅𝑦)))
10 moanimv 1991 . . . . . . . . . 10 (∃*𝑥(𝑦𝐵 ∧ (𝑥𝐴𝑥𝑅𝑦)) ↔ (𝑦𝐵 → ∃*𝑥(𝑥𝐴𝑥𝑅𝑦)))
11 brinxp2 4435 . . . . . . . . . . . 12 (𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦 ↔ (𝑥𝐴𝑦𝐵𝑥𝑅𝑦))
12 3anan12 908 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐵𝑥𝑅𝑦) ↔ (𝑦𝐵 ∧ (𝑥𝐴𝑥𝑅𝑦)))
1311, 12bitri 177 . . . . . . . . . . 11 (𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦 ↔ (𝑦𝐵 ∧ (𝑥𝐴𝑥𝑅𝑦)))
1413mobii 1953 . . . . . . . . . 10 (∃*𝑥 𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦 ↔ ∃*𝑥(𝑦𝐵 ∧ (𝑥𝐴𝑥𝑅𝑦)))
15 df-rmo 2331 . . . . . . . . . . 11 (∃*𝑥𝐴 𝑥𝑅𝑦 ↔ ∃*𝑥(𝑥𝐴𝑥𝑅𝑦))
1615imbi2i 219 . . . . . . . . . 10 ((𝑦𝐵 → ∃*𝑥𝐴 𝑥𝑅𝑦) ↔ (𝑦𝐵 → ∃*𝑥(𝑥𝐴𝑥𝑅𝑦)))
1710, 14, 163bitr4i 205 . . . . . . . . 9 (∃*𝑥 𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦 ↔ (𝑦𝐵 → ∃*𝑥𝐴 𝑥𝑅𝑦))
189, 17syl6rbbr 192 . . . . . . . 8 (𝑦𝐵 → (∃*𝑥 𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦 ↔ ∃*𝑥𝐴 𝑥𝑅𝑦))
1918ralbiia 2355 . . . . . . 7 (∀𝑦𝐵 ∃*𝑥 𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦 ↔ ∀𝑦𝐵 ∃*𝑥𝐴 𝑥𝑅𝑦)
208, 19syl6bb 189 . . . . . 6 (ran (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵 → (∀𝑦 ∈ ran (𝑅 ∩ (𝐴 × 𝐵))∃*𝑥 𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦 ↔ ∀𝑦𝐵 ∃*𝑥𝐴 𝑥𝑅𝑦))
217, 20syl5bb 185 . . . . 5 (ran (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵 → (Fun (𝑅 ∩ (𝐴 × 𝐵)) ↔ ∀𝑦𝐵 ∃*𝑥𝐴 𝑥𝑅𝑦))
2221pm5.32i 435 . . . 4 ((ran (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵 ∧ Fun (𝑅 ∩ (𝐴 × 𝐵))) ↔ (ran (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵 ∧ ∀𝑦𝐵 ∃*𝑥𝐴 𝑥𝑅𝑦))
23 r19.26 2458 . . . 4 (∀𝑦𝐵 (∃𝑥𝐴 𝑥𝑅𝑦 ∧ ∃*𝑥𝐴 𝑥𝑅𝑦) ↔ (∀𝑦𝐵𝑥𝐴 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 ∃*𝑥𝐴 𝑥𝑅𝑦))
246, 22, 233bitr4i 205 . . 3 ((ran (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵 ∧ Fun (𝑅 ∩ (𝐴 × 𝐵))) ↔ ∀𝑦𝐵 (∃𝑥𝐴 𝑥𝑅𝑦 ∧ ∃*𝑥𝐴 𝑥𝑅𝑦))
25 ancom 257 . . 3 ((Fun (𝑅 ∩ (𝐴 × 𝐵)) ∧ ran (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵) ↔ (ran (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵 ∧ Fun (𝑅 ∩ (𝐴 × 𝐵))))
26 reu5 2539 . . . 4 (∃!𝑥𝐴 𝑥𝑅𝑦 ↔ (∃𝑥𝐴 𝑥𝑅𝑦 ∧ ∃*𝑥𝐴 𝑥𝑅𝑦))
2726ralbii 2347 . . 3 (∀𝑦𝐵 ∃!𝑥𝐴 𝑥𝑅𝑦 ↔ ∀𝑦𝐵 (∃𝑥𝐴 𝑥𝑅𝑦 ∧ ∃*𝑥𝐴 𝑥𝑅𝑦))
2824, 25, 273bitr4i 205 . 2 ((Fun (𝑅 ∩ (𝐴 × 𝐵)) ∧ ran (𝑅 ∩ (𝐴 × 𝐵)) = 𝐵) ↔ ∀𝑦𝐵 ∃!𝑥𝐴 𝑥𝑅𝑦)
291, 4, 283bitr2i 201 1 ((𝑅 ∩ (𝐴 × 𝐵)) Fn 𝐵 ↔ ∀𝑦𝐵 ∃!𝑥𝐴 𝑥𝑅𝑦)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   ∧ w3a 896   = wceq 1259   ∈ wcel 1409  ∃*wmo 1917  ∀wral 2323  ∃wrex 2324  ∃!wreu 2325  ∃*wrmo 2326   ∩ cin 2944   class class class wbr 3792   × cxp 4371  ◡ccnv 4372  dom cdm 4373  ran crn 4374  Fun wfun 4924   Fn wfn 4925 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3903  ax-pow 3955  ax-pr 3972 This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-reu 2330  df-rmo 2331  df-v 2576  df-un 2950  df-in 2952  df-ss 2959  df-pw 3389  df-sn 3409  df-pr 3410  df-op 3412  df-br 3793  df-opab 3847  df-id 4058  df-xp 4379  df-rel 4380  df-cnv 4381  df-co 4382  df-dm 4383  df-rn 4384  df-res 4385  df-ima 4386  df-fun 4932  df-fn 4933 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator