![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elmpocl | Structured version Visualization version GIF version |
Description: If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
Ref | Expression |
---|---|
elmpocl.f | ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Ref | Expression |
---|---|
elmpocl | ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elmpocl.f | . . . . . 6 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | |
2 | df-mpo 7024 | . . . . . 6 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
3 | 1, 2 | eqtri 2818 | . . . . 5 ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
4 | 3 | dmeqi 5662 | . . . 4 ⊢ dom 𝐹 = dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
5 | dmoprabss 7115 | . . . 4 ⊢ dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} ⊆ (𝐴 × 𝐵) | |
6 | 4, 5 | eqsstri 3924 | . . 3 ⊢ dom 𝐹 ⊆ (𝐴 × 𝐵) |
7 | elfvdm 6573 | . . . 4 ⊢ (𝑋 ∈ (𝐹‘〈𝑆, 𝑇〉) → 〈𝑆, 𝑇〉 ∈ dom 𝐹) | |
8 | df-ov 7022 | . . . 4 ⊢ (𝑆𝐹𝑇) = (𝐹‘〈𝑆, 𝑇〉) | |
9 | 7, 8 | eleq2s 2900 | . . 3 ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → 〈𝑆, 𝑇〉 ∈ dom 𝐹) |
10 | 6, 9 | sseldi 3889 | . 2 ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → 〈𝑆, 𝑇〉 ∈ (𝐴 × 𝐵)) |
11 | opelxp 5482 | . 2 ⊢ (〈𝑆, 𝑇〉 ∈ (𝐴 × 𝐵) ↔ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵)) | |
12 | 10, 11 | sylib 219 | 1 ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2080 〈cop 4480 × cxp 5444 dom cdm 5446 ‘cfv 6228 (class class class)co 7019 {coprab 7020 ∈ cmpo 7021 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-sep 5097 ax-nul 5104 ax-pow 5160 ax-pr 5224 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ral 3109 df-rex 3110 df-rab 3113 df-v 3438 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-nul 4214 df-if 4384 df-sn 4475 df-pr 4477 df-op 4481 df-uni 4748 df-br 4965 df-opab 5027 df-xp 5452 df-dm 5456 df-iota 6192 df-fv 6236 df-ov 7022 df-oprab 7023 df-mpo 7024 |
This theorem is referenced by: elmpocl1 7250 elmpocl2 7251 elovmpo 7252 elovmporab 7253 elovmporab1 7254 el2mpocsbcl 7639 ixxssixx 12602 funcrcl 16962 natrcl 17049 ismhm 17776 isghm 18099 isga 18162 isslw 18463 isrhm 19163 rimrcl 19166 islmhm 19489 iscn2 21530 elflim2 22256 isfcls 22301 isnmhm 23038 limcrcl 24155 ewlkprop 27068 wwlknbp 27302 wspthnp 27310 iscvm 32108 mclsrcl 32410 mgmhmrcl 43544 intop 43602 rnghmrcl 43652 rngimrcl 43660 |
Copyright terms: Public domain | W3C validator |