![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvimacnv | Structured version Visualization version GIF version |
Description: The argument of a function value belongs to the preimage of any class containing the function value. Raph Levien remarks: "This proof is unsatisfying, because it seems to me that funimass2 6641 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.) |
Ref | Expression |
---|---|
fvimacnv | ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funfvop 7064 | . . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ⟨𝐴, (𝐹‘𝐴)⟩ ∈ 𝐹) | |
2 | fvex 6915 | . . . . . . 7 ⊢ (𝐹‘𝐴) ∈ V | |
3 | opelcnvg 5887 | . . . . . . 7 ⊢ (((𝐹‘𝐴) ∈ V ∧ 𝐴 ∈ dom 𝐹) → (⟨(𝐹‘𝐴), 𝐴⟩ ∈ ◡𝐹 ↔ ⟨𝐴, (𝐹‘𝐴)⟩ ∈ 𝐹)) | |
4 | 2, 3 | mpan 688 | . . . . . 6 ⊢ (𝐴 ∈ dom 𝐹 → (⟨(𝐹‘𝐴), 𝐴⟩ ∈ ◡𝐹 ↔ ⟨𝐴, (𝐹‘𝐴)⟩ ∈ 𝐹)) |
5 | 4 | adantl 480 | . . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (⟨(𝐹‘𝐴), 𝐴⟩ ∈ ◡𝐹 ↔ ⟨𝐴, (𝐹‘𝐴)⟩ ∈ 𝐹)) |
6 | 1, 5 | mpbird 256 | . . . 4 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ⟨(𝐹‘𝐴), 𝐴⟩ ∈ ◡𝐹) |
7 | elimasng 6097 | . . . . . 6 ⊢ (((𝐹‘𝐴) ∈ V ∧ 𝐴 ∈ dom 𝐹) → (𝐴 ∈ (◡𝐹 “ {(𝐹‘𝐴)}) ↔ ⟨(𝐹‘𝐴), 𝐴⟩ ∈ ◡𝐹)) | |
8 | 2, 7 | mpan 688 | . . . . 5 ⊢ (𝐴 ∈ dom 𝐹 → (𝐴 ∈ (◡𝐹 “ {(𝐹‘𝐴)}) ↔ ⟨(𝐹‘𝐴), 𝐴⟩ ∈ ◡𝐹)) |
9 | 8 | adantl 480 | . . . 4 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐴 ∈ (◡𝐹 “ {(𝐹‘𝐴)}) ↔ ⟨(𝐹‘𝐴), 𝐴⟩ ∈ ◡𝐹)) |
10 | 6, 9 | mpbird 256 | . . 3 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → 𝐴 ∈ (◡𝐹 “ {(𝐹‘𝐴)})) |
11 | 2 | snss 4794 | . . . . 5 ⊢ ((𝐹‘𝐴) ∈ 𝐵 ↔ {(𝐹‘𝐴)} ⊆ 𝐵) |
12 | imass2 6111 | . . . . 5 ⊢ ({(𝐹‘𝐴)} ⊆ 𝐵 → (◡𝐹 “ {(𝐹‘𝐴)}) ⊆ (◡𝐹 “ 𝐵)) | |
13 | 11, 12 | sylbi 216 | . . . 4 ⊢ ((𝐹‘𝐴) ∈ 𝐵 → (◡𝐹 “ {(𝐹‘𝐴)}) ⊆ (◡𝐹 “ 𝐵)) |
14 | 13 | sseld 3981 | . . 3 ⊢ ((𝐹‘𝐴) ∈ 𝐵 → (𝐴 ∈ (◡𝐹 “ {(𝐹‘𝐴)}) → 𝐴 ∈ (◡𝐹 “ 𝐵))) |
15 | 10, 14 | syl5com 31 | . 2 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 → 𝐴 ∈ (◡𝐹 “ 𝐵))) |
16 | fvimacnvi 7066 | . . . 4 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (◡𝐹 “ 𝐵)) → (𝐹‘𝐴) ∈ 𝐵) | |
17 | 16 | ex 411 | . . 3 ⊢ (Fun 𝐹 → (𝐴 ∈ (◡𝐹 “ 𝐵) → (𝐹‘𝐴) ∈ 𝐵)) |
18 | 17 | adantr 479 | . 2 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐴 ∈ (◡𝐹 “ 𝐵) → (𝐹‘𝐴) ∈ 𝐵)) |
19 | 15, 18 | impbid 211 | 1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∈ wcel 2098 Vcvv 3473 ⊆ wss 3949 {csn 4632 ⟨cop 4638 ◡ccnv 5681 dom cdm 5682 “ cima 5685 Fun wfun 6547 ‘cfv 6553 |
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 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-12 2166 ax-ext 2699 ax-sep 5303 ax-nul 5310 ax-pr 5433 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-ral 3059 df-rex 3068 df-rab 3431 df-v 3475 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4327 df-if 4533 df-sn 4633 df-pr 4635 df-op 4639 df-uni 4913 df-br 5153 df-opab 5215 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-iota 6505 df-fun 6555 df-fn 6556 df-fv 6561 |
This theorem is referenced by: funimass3 7068 elpreima 7072 iinpreima 7083 isr0 23669 rnelfmlem 23884 rnelfm 23885 fmfnfmlem2 23887 fmfnfmlem4 23889 fmfnfm 23890 metustid 24491 metustsym 24492 metustexhalf 24493 xppreima 32461 rhmpreimaidl 33166 dstfrvel 34134 ballotlemrv 34180 bj-fvimacnv0 36806 bj-isrvec 36814 grpokerinj 37407 diaintclN 40571 dibintclN 40680 dihintcl 40857 aks6d1c2lem4 41638 aks6d1c6lem2 41683 arearect 42692 areaquad 42693 |
Copyright terms: Public domain | W3C validator |