![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > intmin | Structured version Visualization version GIF version |
Description: Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Ref | Expression |
---|---|
intmin | ⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3481 | . . . . 5 ⊢ 𝑦 ∈ V | |
2 | 1 | elintrab 4964 | . . . 4 ⊢ (𝑦 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ↔ ∀𝑥 ∈ 𝐵 (𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥)) |
3 | ssid 4017 | . . . . 5 ⊢ 𝐴 ⊆ 𝐴 | |
4 | sseq2 4021 | . . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐴)) | |
5 | eleq2 2827 | . . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴)) | |
6 | 4, 5 | imbi12d 344 | . . . . . 6 ⊢ (𝑥 = 𝐴 → ((𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥) ↔ (𝐴 ⊆ 𝐴 → 𝑦 ∈ 𝐴))) |
7 | 6 | rspcv 3617 | . . . . 5 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥) → (𝐴 ⊆ 𝐴 → 𝑦 ∈ 𝐴))) |
8 | 3, 7 | mpii 46 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴)) |
9 | 2, 8 | biimtrid 242 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑦 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} → 𝑦 ∈ 𝐴)) |
10 | 9 | ssrdv 4000 | . 2 ⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ⊆ 𝐴) |
11 | ssintub 4970 | . . 3 ⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} | |
12 | 11 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}) |
13 | 10, 12 | eqssd 4012 | 1 ⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1536 ∈ wcel 2105 ∀wral 3058 {crab 3432 ⊆ wss 3962 ∩ cint 4950 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1539 df-ex 1776 df-nf 1780 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-ss 3979 df-int 4951 |
This theorem is referenced by: intmin2 4979 ordintdif 6435 uniordint 7820 onsucmin 7840 naddrid 8719 naddasslem1 8730 naddasslem2 8731 rankonidlem 9865 rankval4 9904 harsucnn 10035 mrcid 17657 lspid 20997 aspid 21912 cldcls 23065 spanid 31375 chsupid 31440 fldgenidfld 33298 igenidl2 38051 pclidN 39878 diaocN 41107 onuniintrab 43214 topclat 48786 toplatlub 48788 toplatjoin 48790 |
Copyright terms: Public domain | W3C validator |