Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > relelfvdm | GIF version |
Description: If a function value has a member, the argument belongs to the domain. (Contributed by Jim Kingdon, 22-Jan-2019.) |
Ref | Expression |
---|---|
relelfvdm | ⊢ ((Rel 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → 𝐵 ∈ dom 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfv 5468 | . . . . . 6 ⊢ (𝐴 ∈ (𝐹‘𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ ∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥))) | |
2 | exsimpr 1598 | . . . . . 6 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ ∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥)) → ∃𝑥∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥)) | |
3 | 1, 2 | sylbi 120 | . . . . 5 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ∃𝑥∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥)) |
4 | equsb1 1765 | . . . . . . . 8 ⊢ [𝑥 / 𝑦]𝑦 = 𝑥 | |
5 | spsbbi 1824 | . . . . . . . 8 ⊢ (∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → ([𝑥 / 𝑦]𝐵𝐹𝑦 ↔ [𝑥 / 𝑦]𝑦 = 𝑥)) | |
6 | 4, 5 | mpbiri 167 | . . . . . . 7 ⊢ (∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → [𝑥 / 𝑦]𝐵𝐹𝑦) |
7 | nfv 1508 | . . . . . . . 8 ⊢ Ⅎ𝑦 𝐵𝐹𝑥 | |
8 | breq2 3971 | . . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝐵𝐹𝑦 ↔ 𝐵𝐹𝑥)) | |
9 | 7, 8 | sbie 1771 | . . . . . . 7 ⊢ ([𝑥 / 𝑦]𝐵𝐹𝑦 ↔ 𝐵𝐹𝑥) |
10 | 6, 9 | sylib 121 | . . . . . 6 ⊢ (∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → 𝐵𝐹𝑥) |
11 | 10 | eximi 1580 | . . . . 5 ⊢ (∃𝑥∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → ∃𝑥 𝐵𝐹𝑥) |
12 | 3, 11 | syl 14 | . . . 4 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ∃𝑥 𝐵𝐹𝑥) |
13 | 12 | anim2i 340 | . . 3 ⊢ ((Rel 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → (Rel 𝐹 ∧ ∃𝑥 𝐵𝐹𝑥)) |
14 | 19.42v 1886 | . . 3 ⊢ (∃𝑥(Rel 𝐹 ∧ 𝐵𝐹𝑥) ↔ (Rel 𝐹 ∧ ∃𝑥 𝐵𝐹𝑥)) | |
15 | 13, 14 | sylibr 133 | . 2 ⊢ ((Rel 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → ∃𝑥(Rel 𝐹 ∧ 𝐵𝐹𝑥)) |
16 | releldm 4823 | . . 3 ⊢ ((Rel 𝐹 ∧ 𝐵𝐹𝑥) → 𝐵 ∈ dom 𝐹) | |
17 | 16 | exlimiv 1578 | . 2 ⊢ (∃𝑥(Rel 𝐹 ∧ 𝐵𝐹𝑥) → 𝐵 ∈ dom 𝐹) |
18 | 15, 17 | syl 14 | 1 ⊢ ((Rel 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → 𝐵 ∈ dom 𝐹) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∀wal 1333 ∃wex 1472 [wsb 1742 ∈ wcel 2128 class class class wbr 3967 dom cdm 4588 Rel wrel 4593 ‘cfv 5172 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-14 2131 ax-ext 2139 ax-sep 4084 ax-pow 4137 ax-pr 4171 |
This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ral 2440 df-rex 2441 df-v 2714 df-un 3106 df-in 3108 df-ss 3115 df-pw 3546 df-sn 3567 df-pr 3568 df-op 3570 df-uni 3775 df-br 3968 df-opab 4028 df-xp 4594 df-rel 4595 df-dm 4598 df-iota 5137 df-fv 5180 |
This theorem is referenced by: mptrcl 5552 elfvmptrab1 5564 elmpocl 6020 oprssdmm 6121 mpoxopn0yelv 6188 eluzel2 9449 hashinfom 10663 istopon 12481 istps 12500 topontopn 12505 eltg4i 12525 eltg3 12527 tg1 12529 tg2 12530 tgclb 12535 cldrcl 12572 neiss2 12612 lmrcl 12661 cnprcl2k 12676 metflem 12819 xmetf 12820 ismet2 12824 xmeteq0 12829 xmettri2 12831 xmetpsmet 12839 xmetres2 12849 blfvalps 12855 blex 12857 blvalps 12858 blval 12859 blfps 12879 blf 12880 mopnval 12912 isxms2 12922 comet 12969 |
Copyright terms: Public domain | W3C validator |