Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  i1f1lem Structured version   Visualization version   GIF version

Theorem i1f1lem 24224
 Description: Lemma for i1f1 24225 and itg11 24226. (Contributed by Mario Carneiro, 18-Jun-2014.)
Hypothesis
Ref Expression
i1f1.1 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 1, 0))
Assertion
Ref Expression
i1f1lem (𝐹:ℝ⟶{0, 1} ∧ (𝐴 ∈ dom vol → (𝐹 “ {1}) = 𝐴))
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝐹(𝑥)

Proof of Theorem i1f1lem
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 1ex 10631 . . . . . 6 1 ∈ V
21prid2 4698 . . . . 5 1 ∈ {0, 1}
3 c0ex 10629 . . . . . 6 0 ∈ V
43prid1 4697 . . . . 5 0 ∈ {0, 1}
52, 4ifcli 4516 . . . 4 if(𝑥𝐴, 1, 0) ∈ {0, 1}
65rgenw 3155 . . 3 𝑥 ∈ ℝ if(𝑥𝐴, 1, 0) ∈ {0, 1}
7 i1f1.1 . . . 4 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 1, 0))
87fmpt 6872 . . 3 (∀𝑥 ∈ ℝ if(𝑥𝐴, 1, 0) ∈ {0, 1} ↔ 𝐹:ℝ⟶{0, 1})
96, 8mpbi 231 . 2 𝐹:ℝ⟶{0, 1}
105a1i 11 . . . . . . 7 ((𝐴 ∈ dom vol ∧ 𝑥 ∈ ℝ) → if(𝑥𝐴, 1, 0) ∈ {0, 1})
1110, 7fmptd 6876 . . . . . 6 (𝐴 ∈ dom vol → 𝐹:ℝ⟶{0, 1})
12 ffn 6513 . . . . . 6 (𝐹:ℝ⟶{0, 1} → 𝐹 Fn ℝ)
13 elpreima 6826 . . . . . 6 (𝐹 Fn ℝ → (𝑦 ∈ (𝐹 “ {1}) ↔ (𝑦 ∈ ℝ ∧ (𝐹𝑦) ∈ {1})))
1411, 12, 133syl 18 . . . . 5 (𝐴 ∈ dom vol → (𝑦 ∈ (𝐹 “ {1}) ↔ (𝑦 ∈ ℝ ∧ (𝐹𝑦) ∈ {1})))
15 fvex 6682 . . . . . . . 8 (𝐹𝑦) ∈ V
1615elsn 4579 . . . . . . 7 ((𝐹𝑦) ∈ {1} ↔ (𝐹𝑦) = 1)
17 eleq1w 2900 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
1817ifbid 4492 . . . . . . . . . 10 (𝑥 = 𝑦 → if(𝑥𝐴, 1, 0) = if(𝑦𝐴, 1, 0))
191, 3ifex 4518 . . . . . . . . . 10 if(𝑦𝐴, 1, 0) ∈ V
2018, 7, 19fvmpt 6767 . . . . . . . . 9 (𝑦 ∈ ℝ → (𝐹𝑦) = if(𝑦𝐴, 1, 0))
2120eqeq1d 2828 . . . . . . . 8 (𝑦 ∈ ℝ → ((𝐹𝑦) = 1 ↔ if(𝑦𝐴, 1, 0) = 1))
22 0ne1 11702 . . . . . . . . . . 11 0 ≠ 1
23 iffalse 4479 . . . . . . . . . . . . 13 𝑦𝐴 → if(𝑦𝐴, 1, 0) = 0)
2423eqeq1d 2828 . . . . . . . . . . . 12 𝑦𝐴 → (if(𝑦𝐴, 1, 0) = 1 ↔ 0 = 1))
2524necon3bbid 3058 . . . . . . . . . . 11 𝑦𝐴 → (¬ if(𝑦𝐴, 1, 0) = 1 ↔ 0 ≠ 1))
2622, 25mpbiri 259 . . . . . . . . . 10 𝑦𝐴 → ¬ if(𝑦𝐴, 1, 0) = 1)
2726con4i 114 . . . . . . . . 9 (if(𝑦𝐴, 1, 0) = 1 → 𝑦𝐴)
28 iftrue 4476 . . . . . . . . 9 (𝑦𝐴 → if(𝑦𝐴, 1, 0) = 1)
2927, 28impbii 210 . . . . . . . 8 (if(𝑦𝐴, 1, 0) = 1 ↔ 𝑦𝐴)
3021, 29syl6bb 288 . . . . . . 7 (𝑦 ∈ ℝ → ((𝐹𝑦) = 1 ↔ 𝑦𝐴))
3116, 30syl5bb 284 . . . . . 6 (𝑦 ∈ ℝ → ((𝐹𝑦) ∈ {1} ↔ 𝑦𝐴))
3231pm5.32i 575 . . . . 5 ((𝑦 ∈ ℝ ∧ (𝐹𝑦) ∈ {1}) ↔ (𝑦 ∈ ℝ ∧ 𝑦𝐴))
3314, 32syl6bb 288 . . . 4 (𝐴 ∈ dom vol → (𝑦 ∈ (𝐹 “ {1}) ↔ (𝑦 ∈ ℝ ∧ 𝑦𝐴)))
34 mblss 24066 . . . . . 6 (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
3534sseld 3970 . . . . 5 (𝐴 ∈ dom vol → (𝑦𝐴𝑦 ∈ ℝ))
3635pm4.71rd 563 . . . 4 (𝐴 ∈ dom vol → (𝑦𝐴 ↔ (𝑦 ∈ ℝ ∧ 𝑦𝐴)))
3733, 36bitr4d 283 . . 3 (𝐴 ∈ dom vol → (𝑦 ∈ (𝐹 “ {1}) ↔ 𝑦𝐴))
3837eqrdv 2824 . 2 (𝐴 ∈ dom vol → (𝐹 “ {1}) = 𝐴)
399, 38pm3.2i 471 1 (𝐹:ℝ⟶{0, 1} ∧ (𝐴 ∈ dom vol → (𝐹 “ {1}) = 𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1530   ∈ wcel 2107   ≠ wne 3021  ∀wral 3143  ifcif 4470  {csn 4564  {cpr 4566   ↦ cmpt 5143  ◡ccnv 5553  dom cdm 5554   “ cima 5557   Fn wfn 6349  ⟶wf 6350  ‘cfv 6354  ℝcr 10530  0cc0 10531  1c1 10532  volcvol 23998 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7574  df-1st 7685  df-2nd 7686  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-er 8284  df-map 8403  df-en 8504  df-dom 8505  df-sdom 8506  df-sup 8900  df-inf 8901  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-n0 11892  df-z 11976  df-uz 12238  df-rp 12385  df-ico 12739  df-icc 12740  df-fz 12888  df-seq 13365  df-exp 13425  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-ovol 23999  df-vol 24000 This theorem is referenced by:  i1f1  24225  itg11  24226
 Copyright terms: Public domain W3C validator