![]() |
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 5513 | . . . . . 6 ⊢ (𝐴 ∈ (𝐹‘𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ ∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥))) | |
2 | exsimpr 1618 | . . . . . 6 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ ∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥)) → ∃𝑥∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥)) | |
3 | 1, 2 | sylbi 121 | . . . . 5 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ∃𝑥∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥)) |
4 | equsb1 1785 | . . . . . . . 8 ⊢ [𝑥 / 𝑦]𝑦 = 𝑥 | |
5 | spsbbi 1844 | . . . . . . . 8 ⊢ (∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → ([𝑥 / 𝑦]𝐵𝐹𝑦 ↔ [𝑥 / 𝑦]𝑦 = 𝑥)) | |
6 | 4, 5 | mpbiri 168 | . . . . . . 7 ⊢ (∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → [𝑥 / 𝑦]𝐵𝐹𝑦) |
7 | nfv 1528 | . . . . . . . 8 ⊢ Ⅎ𝑦 𝐵𝐹𝑥 | |
8 | breq2 4007 | . . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝐵𝐹𝑦 ↔ 𝐵𝐹𝑥)) | |
9 | 7, 8 | sbie 1791 | . . . . . . 7 ⊢ ([𝑥 / 𝑦]𝐵𝐹𝑦 ↔ 𝐵𝐹𝑥) |
10 | 6, 9 | sylib 122 | . . . . . 6 ⊢ (∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → 𝐵𝐹𝑥) |
11 | 10 | eximi 1600 | . . . . 5 ⊢ (∃𝑥∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → ∃𝑥 𝐵𝐹𝑥) |
12 | 3, 11 | syl 14 | . . . 4 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ∃𝑥 𝐵𝐹𝑥) |
13 | 12 | anim2i 342 | . . 3 ⊢ ((Rel 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → (Rel 𝐹 ∧ ∃𝑥 𝐵𝐹𝑥)) |
14 | 19.42v 1906 | . . 3 ⊢ (∃𝑥(Rel 𝐹 ∧ 𝐵𝐹𝑥) ↔ (Rel 𝐹 ∧ ∃𝑥 𝐵𝐹𝑥)) | |
15 | 13, 14 | sylibr 134 | . 2 ⊢ ((Rel 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → ∃𝑥(Rel 𝐹 ∧ 𝐵𝐹𝑥)) |
16 | releldm 4862 | . . 3 ⊢ ((Rel 𝐹 ∧ 𝐵𝐹𝑥) → 𝐵 ∈ dom 𝐹) | |
17 | 16 | exlimiv 1598 | . 2 ⊢ (∃𝑥(Rel 𝐹 ∧ 𝐵𝐹𝑥) → 𝐵 ∈ dom 𝐹) |
18 | 15, 17 | syl 14 | 1 ⊢ ((Rel 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → 𝐵 ∈ dom 𝐹) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∀wal 1351 ∃wex 1492 [wsb 1762 ∈ wcel 2148 class class class wbr 4003 dom cdm 4626 Rel wrel 4631 ‘cfv 5216 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-14 2151 ax-ext 2159 ax-sep 4121 ax-pow 4174 ax-pr 4209 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-v 2739 df-un 3133 df-in 3135 df-ss 3142 df-pw 3577 df-sn 3598 df-pr 3599 df-op 3601 df-uni 3810 df-br 4004 df-opab 4065 df-xp 4632 df-rel 4633 df-dm 4636 df-iota 5178 df-fv 5224 |
This theorem is referenced by: mptrcl 5598 elfvmptrab1 5610 elmpocl 6068 oprssdmm 6171 mpoxopn0yelv 6239 eluzel2 9531 hashinfom 10753 basmex 12515 basmexd 12516 ismgmn0 12731 istopon 13404 istps 13423 topontopn 13428 eltg4i 13448 eltg3 13450 tg1 13452 tg2 13453 tgclb 13458 cldrcl 13495 neiss2 13535 lmrcl 13584 cnprcl2k 13599 metflem 13742 xmetf 13743 ismet2 13747 xmeteq0 13752 xmettri2 13754 xmetpsmet 13762 xmetres2 13772 blfvalps 13778 blex 13780 blvalps 13781 blval 13782 blfps 13802 blf 13803 mopnval 13835 isxms2 13845 comet 13892 |
Copyright terms: Public domain | W3C validator |