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

Theorem fncnv 4906
Description: Single-rootedness (see funcnv 4901) of a class cut down by a cross product. (Contributed by NM, 5-Mar-2007.)
Assertion
Ref Expression
fncnv ((𝑅 ∩ (A × B)) Fn By B ∃!x A x𝑅y)
Distinct variable groups:   x,y,A   x,B,y   x,𝑅,y

Proof of Theorem fncnv
StepHypRef Expression
1 df-fn 4847 . 2 ((𝑅 ∩ (A × B)) Fn B ↔ (Fun (𝑅 ∩ (A × B)) dom (𝑅 ∩ (A × B)) = B))
2 df-rn 4298 . . . 4 ran (𝑅 ∩ (A × B)) = dom (𝑅 ∩ (A × B))
32eqeq1i 2044 . . 3 (ran (𝑅 ∩ (A × B)) = B ↔ dom (𝑅 ∩ (A × B)) = B)
43anbi2i 430 . 2 ((Fun (𝑅 ∩ (A × B)) ran (𝑅 ∩ (A × B)) = B) ↔ (Fun (𝑅 ∩ (A × B)) dom (𝑅 ∩ (A × B)) = B))
5 rninxp 4706 . . . . 5 (ran (𝑅 ∩ (A × B)) = By B x A x𝑅y)
65anbi1i 431 . . . 4 ((ran (𝑅 ∩ (A × B)) = B y B ∃*x A x𝑅y) ↔ (y B x A x𝑅y y B ∃*x A x𝑅y))
7 funcnv 4901 . . . . . 6 (Fun (𝑅 ∩ (A × B)) ↔ y ran (𝑅 ∩ (A × B))∃*x x(𝑅 ∩ (A × B))y)
8 raleq 2499 . . . . . . 7 (ran (𝑅 ∩ (A × B)) = B → (y ran (𝑅 ∩ (A × B))∃*x x(𝑅 ∩ (A × B))yy B ∃*x x(𝑅 ∩ (A × B))y))
9 biimt 230 . . . . . . . . 9 (y B → (∃*x A x𝑅y ↔ (y B∃*x A x𝑅y)))
10 moanimv 1972 . . . . . . . . . 10 (∃*x(y B (x A x𝑅y)) ↔ (y B∃*x(x A x𝑅y)))
11 brinxp2 4349 . . . . . . . . . . . 12 (x(𝑅 ∩ (A × B))y ↔ (x A y B x𝑅y))
12 3anan12 896 . . . . . . . . . . . 12 ((x A y B x𝑅y) ↔ (y B (x A x𝑅y)))
1311, 12bitri 173 . . . . . . . . . . 11 (x(𝑅 ∩ (A × B))y ↔ (y B (x A x𝑅y)))
1413mobii 1934 . . . . . . . . . 10 (∃*x x(𝑅 ∩ (A × B))y∃*x(y B (x A x𝑅y)))
15 df-rmo 2308 . . . . . . . . . . 11 (∃*x A x𝑅y∃*x(x A x𝑅y))
1615imbi2i 215 . . . . . . . . . 10 ((y B∃*x A x𝑅y) ↔ (y B∃*x(x A x𝑅y)))
1710, 14, 163bitr4i 201 . . . . . . . . 9 (∃*x x(𝑅 ∩ (A × B))y ↔ (y B∃*x A x𝑅y))
189, 17syl6rbbr 188 . . . . . . . 8 (y B → (∃*x x(𝑅 ∩ (A × B))y∃*x A x𝑅y))
1918ralbiia 2332 . . . . . . 7 (y B ∃*x x(𝑅 ∩ (A × B))yy B ∃*x A x𝑅y)
208, 19syl6bb 185 . . . . . 6 (ran (𝑅 ∩ (A × B)) = B → (y ran (𝑅 ∩ (A × B))∃*x x(𝑅 ∩ (A × B))yy B ∃*x A x𝑅y))
217, 20syl5bb 181 . . . . 5 (ran (𝑅 ∩ (A × B)) = B → (Fun (𝑅 ∩ (A × B)) ↔ y B ∃*x A x𝑅y))
2221pm5.32i 427 . . . 4 ((ran (𝑅 ∩ (A × B)) = B Fun (𝑅 ∩ (A × B))) ↔ (ran (𝑅 ∩ (A × B)) = B y B ∃*x A x𝑅y))
23 r19.26 2435 . . . 4 (y B (x A x𝑅y ∃*x A x𝑅y) ↔ (y B x A x𝑅y y B ∃*x A x𝑅y))
246, 22, 233bitr4i 201 . . 3 ((ran (𝑅 ∩ (A × B)) = B Fun (𝑅 ∩ (A × B))) ↔ y B (x A x𝑅y ∃*x A x𝑅y))
25 ancom 253 . . 3 ((Fun (𝑅 ∩ (A × B)) ran (𝑅 ∩ (A × B)) = B) ↔ (ran (𝑅 ∩ (A × B)) = B Fun (𝑅 ∩ (A × B))))
26 reu5 2516 . . . 4 (∃!x A x𝑅y ↔ (x A x𝑅y ∃*x A x𝑅y))
2726ralbii 2324 . . 3 (y B ∃!x A x𝑅yy B (x A x𝑅y ∃*x A x𝑅y))
2824, 25, 273bitr4i 201 . 2 ((Fun (𝑅 ∩ (A × B)) ran (𝑅 ∩ (A × B)) = B) ↔ y B ∃!x A x𝑅y)
291, 4, 283bitr2i 197 1 ((𝑅 ∩ (A × B)) Fn By B ∃!x A x𝑅y)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 884   = wceq 1242   wcel 1390  ∃*wmo 1898  wral 2300  wrex 2301  ∃!wreu 2302  ∃*wrmo 2303  cin 2910   class class class wbr 3754   × cxp 4285  ccnv 4286  dom cdm 4287  ran crn 4288  Fun wfun 4838   Fn wfn 4839
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3865  ax-pow 3917  ax-pr 3934
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-reu 2307  df-rmo 2308  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3352  df-sn 3372  df-pr 3373  df-op 3375  df-br 3755  df-opab 3809  df-id 4020  df-xp 4293  df-rel 4294  df-cnv 4295  df-co 4296  df-dm 4297  df-rn 4298  df-res 4299  df-ima 4300  df-fun 4846  df-fn 4847
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator