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

Theorem funimass4 5339
Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Raph Levien, 20-Nov-2006.)
Assertion
Ref Expression
funimass4 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → ((𝐹𝐴) ⊆ 𝐵 ↔ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹

Proof of Theorem funimass4
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dfss2 3012 . 2 ((𝐹𝐴) ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ (𝐹𝐴) → 𝑦𝐵))
2 eqcom 2090 . . . . . . . . . 10 (𝑦 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝑦)
3 ssel 3017 . . . . . . . . . . . 12 (𝐴 ⊆ dom 𝐹 → (𝑥𝐴𝑥 ∈ dom 𝐹))
4 funbrfvb 5331 . . . . . . . . . . . . 13 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((𝐹𝑥) = 𝑦𝑥𝐹𝑦))
54ex 113 . . . . . . . . . . . 12 (Fun 𝐹 → (𝑥 ∈ dom 𝐹 → ((𝐹𝑥) = 𝑦𝑥𝐹𝑦)))
63, 5syl9 71 . . . . . . . . . . 11 (𝐴 ⊆ dom 𝐹 → (Fun 𝐹 → (𝑥𝐴 → ((𝐹𝑥) = 𝑦𝑥𝐹𝑦))))
76imp31 252 . . . . . . . . . 10 (((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) ∧ 𝑥𝐴) → ((𝐹𝑥) = 𝑦𝑥𝐹𝑦))
82, 7syl5bb 190 . . . . . . . . 9 (((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) ∧ 𝑥𝐴) → (𝑦 = (𝐹𝑥) ↔ 𝑥𝐹𝑦))
98rexbidva 2377 . . . . . . . 8 ((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) → (∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ ∃𝑥𝐴 𝑥𝐹𝑦))
10 vex 2622 . . . . . . . . 9 𝑦 ∈ V
1110elima 4766 . . . . . . . 8 (𝑦 ∈ (𝐹𝐴) ↔ ∃𝑥𝐴 𝑥𝐹𝑦)
129, 11syl6rbbr 197 . . . . . . 7 ((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) → (𝑦 ∈ (𝐹𝐴) ↔ ∃𝑥𝐴 𝑦 = (𝐹𝑥)))
1312imbi1d 229 . . . . . 6 ((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) → ((𝑦 ∈ (𝐹𝐴) → 𝑦𝐵) ↔ (∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵)))
14 r19.23v 2481 . . . . . 6 (∀𝑥𝐴 (𝑦 = (𝐹𝑥) → 𝑦𝐵) ↔ (∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵))
1513, 14syl6bbr 196 . . . . 5 ((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) → ((𝑦 ∈ (𝐹𝐴) → 𝑦𝐵) ↔ ∀𝑥𝐴 (𝑦 = (𝐹𝑥) → 𝑦𝐵)))
1615albidv 1752 . . . 4 ((𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹) → (∀𝑦(𝑦 ∈ (𝐹𝐴) → 𝑦𝐵) ↔ ∀𝑦𝑥𝐴 (𝑦 = (𝐹𝑥) → 𝑦𝐵)))
1716ancoms 264 . . 3 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (∀𝑦(𝑦 ∈ (𝐹𝐴) → 𝑦𝐵) ↔ ∀𝑦𝑥𝐴 (𝑦 = (𝐹𝑥) → 𝑦𝐵)))
18 ralcom4 2641 . . . 4 (∀𝑥𝐴𝑦(𝑦 = (𝐹𝑥) → 𝑦𝐵) ↔ ∀𝑦𝑥𝐴 (𝑦 = (𝐹𝑥) → 𝑦𝐵))
19 ssel2 3018 . . . . . . . . 9 ((𝐴 ⊆ dom 𝐹𝑥𝐴) → 𝑥 ∈ dom 𝐹)
2019anim2i 334 . . . . . . . 8 ((Fun 𝐹 ∧ (𝐴 ⊆ dom 𝐹𝑥𝐴)) → (Fun 𝐹𝑥 ∈ dom 𝐹))
21203impb 1139 . . . . . . 7 ((Fun 𝐹𝐴 ⊆ dom 𝐹𝑥𝐴) → (Fun 𝐹𝑥 ∈ dom 𝐹))
22 funfvex 5306 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ V)
23 nfv 1466 . . . . . . . 8 𝑦(𝐹𝑥) ∈ 𝐵
24 eleq1 2150 . . . . . . . 8 (𝑦 = (𝐹𝑥) → (𝑦𝐵 ↔ (𝐹𝑥) ∈ 𝐵))
2523, 24ceqsalg 2647 . . . . . . 7 ((𝐹𝑥) ∈ V → (∀𝑦(𝑦 = (𝐹𝑥) → 𝑦𝐵) ↔ (𝐹𝑥) ∈ 𝐵))
2621, 22, 253syl 17 . . . . . 6 ((Fun 𝐹𝐴 ⊆ dom 𝐹𝑥𝐴) → (∀𝑦(𝑦 = (𝐹𝑥) → 𝑦𝐵) ↔ (𝐹𝑥) ∈ 𝐵))
27263expa 1143 . . . . 5 (((Fun 𝐹𝐴 ⊆ dom 𝐹) ∧ 𝑥𝐴) → (∀𝑦(𝑦 = (𝐹𝑥) → 𝑦𝐵) ↔ (𝐹𝑥) ∈ 𝐵))
2827ralbidva 2376 . . . 4 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (∀𝑥𝐴𝑦(𝑦 = (𝐹𝑥) → 𝑦𝐵) ↔ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
2918, 28syl5bbr 192 . . 3 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (∀𝑦𝑥𝐴 (𝑦 = (𝐹𝑥) → 𝑦𝐵) ↔ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
3017, 29bitrd 186 . 2 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (∀𝑦(𝑦 ∈ (𝐹𝐴) → 𝑦𝐵) ↔ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
311, 30syl5bb 190 1 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → ((𝐹𝐴) ⊆ 𝐵 ↔ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3a 924  wal 1287   = wceq 1289  wcel 1438  wral 2359  wrex 2360  Vcvv 2619  wss 2997   class class class wbr 3837  dom cdm 4428  cima 4431  Fun wfun 4996  cfv 5002
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-sbc 2839  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-opab 3892  df-id 4111  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-iota 4967  df-fun 5004  df-fn 5005  df-fv 5010
This theorem is referenced by:  funimass3  5399  funimass5  5400  funconstss  5401  funimassov  5776  phimullem  11283
  Copyright terms: Public domain W3C validator