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

Theorem dffo4 5231
Description: Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)
Assertion
Ref Expression
dffo4 (𝐹:AontoB ↔ (𝐹:AB y B x A x𝐹y))
Distinct variable groups:   x,y,A   x,B,y   x,𝐹,y

Proof of Theorem dffo4
StepHypRef Expression
1 dffo2 5026 . . 3 (𝐹:AontoB ↔ (𝐹:AB ran 𝐹 = B))
2 simpl 102 . . . 4 ((𝐹:AB ran 𝐹 = B) → 𝐹:AB)
3 vex 2532 . . . . . . . . . 10 y V
43elrn 4495 . . . . . . . . 9 (y ran 𝐹x x𝐹y)
5 eleq2 2077 . . . . . . . . 9 (ran 𝐹 = B → (y ran 𝐹y B))
64, 5syl5bbr 183 . . . . . . . 8 (ran 𝐹 = B → (x x𝐹yy B))
76biimpar 281 . . . . . . 7 ((ran 𝐹 = B y B) → x x𝐹y)
87adantll 445 . . . . . 6 (((𝐹:AB ran 𝐹 = B) y B) → x x𝐹y)
9 ffn 4963 . . . . . . . . . . 11 (𝐹:AB𝐹 Fn A)
10 fnbr 4918 . . . . . . . . . . . 12 ((𝐹 Fn A x𝐹y) → x A)
1110ex 108 . . . . . . . . . . 11 (𝐹 Fn A → (x𝐹yx A))
129, 11syl 14 . . . . . . . . . 10 (𝐹:AB → (x𝐹yx A))
1312ancrd 309 . . . . . . . . 9 (𝐹:AB → (x𝐹y → (x A x𝐹y)))
1413eximdv 1736 . . . . . . . 8 (𝐹:AB → (x x𝐹yx(x A x𝐹y)))
15 df-rex 2284 . . . . . . . 8 (x A x𝐹yx(x A x𝐹y))
1614, 15syl6ibr 151 . . . . . . 7 (𝐹:AB → (x x𝐹yx A x𝐹y))
1716ad2antrr 457 . . . . . 6 (((𝐹:AB ran 𝐹 = B) y B) → (x x𝐹yx A x𝐹y))
188, 17mpd 13 . . . . 5 (((𝐹:AB ran 𝐹 = B) y B) → x A x𝐹y)
1918ralrimiva 2364 . . . 4 ((𝐹:AB ran 𝐹 = B) → y B x A x𝐹y)
202, 19jca 290 . . 3 ((𝐹:AB ran 𝐹 = B) → (𝐹:AB y B x A x𝐹y))
211, 20sylbi 114 . 2 (𝐹:AontoB → (𝐹:AB y B x A x𝐹y))
22 fnbrfvb 5130 . . . . . . . . 9 ((𝐹 Fn A x A) → ((𝐹x) = yx𝐹y))
2322biimprd 147 . . . . . . . 8 ((𝐹 Fn A x A) → (x𝐹y → (𝐹x) = y))
24 eqcom 2018 . . . . . . . 8 ((𝐹x) = yy = (𝐹x))
2523, 24syl6ib 150 . . . . . . 7 ((𝐹 Fn A x A) → (x𝐹yy = (𝐹x)))
269, 25sylan 267 . . . . . 6 ((𝐹:AB x A) → (x𝐹yy = (𝐹x)))
2726reximdva 2393 . . . . 5 (𝐹:AB → (x A x𝐹yx A y = (𝐹x)))
2827ralimdv 2360 . . . 4 (𝐹:AB → (y B x A x𝐹yy B x A y = (𝐹x)))
2928imdistani 419 . . 3 ((𝐹:AB y B x A x𝐹y) → (𝐹:AB y B x A y = (𝐹x)))
30 dffo3 5230 . . 3 (𝐹:AontoB ↔ (𝐹:AB y B x A y = (𝐹x)))
3129, 30sylibr 137 . 2 ((𝐹:AB y B x A x𝐹y) → 𝐹:AontoB)
3221, 31impbii 117 1 (𝐹:AontoB ↔ (𝐹:AB y B x A x𝐹y))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1226  wex 1357   wcel 1369  wral 2278  wrex 2279   class class class wbr 3730  ran crn 4264   Fn wfn 4815  wf 4816  ontowfo 4818  cfv 4820
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 614  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1358  ax-ie2 1359  ax-8 1371  ax-10 1372  ax-11 1373  ax-i12 1374  ax-bnd 1375  ax-4 1376  ax-14 1381  ax-17 1395  ax-i9 1399  ax-ial 1403  ax-i5r 1404  ax-ext 1998  ax-sep 3841  ax-pow 3893  ax-pr 3910
This theorem depends on definitions:  df-bi 110  df-3an 871  df-tru 1229  df-nf 1326  df-sb 1622  df-eu 1879  df-mo 1880  df-clab 2003  df-cleq 2009  df-clel 2012  df-nfc 2143  df-ral 2283  df-rex 2284  df-v 2531  df-sbc 2736  df-un 2893  df-in 2895  df-ss 2902  df-pw 3328  df-sn 3348  df-pr 3349  df-op 3351  df-uni 3547  df-br 3731  df-opab 3785  df-mpt 3786  df-id 3996  df-xp 4269  df-rel 4270  df-cnv 4271  df-co 4272  df-dm 4273  df-rn 4274  df-iota 4785  df-fun 4822  df-fn 4823  df-f 4824  df-fo 4826  df-fv 4828
This theorem is referenced by:  dffo5  5232
  Copyright terms: Public domain W3C validator