![]() |
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 3476 | . . . . 5 ⊢ 𝑦 ∈ V | |
2 | 1 | elintrab 4965 | . . . 4 ⊢ (𝑦 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ↔ ∀𝑥 ∈ 𝐵 (𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥)) |
3 | ssid 4005 | . . . . 5 ⊢ 𝐴 ⊆ 𝐴 | |
4 | sseq2 4009 | . . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐴)) | |
5 | eleq2 2820 | . . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴)) | |
6 | 4, 5 | imbi12d 343 | . . . . . 6 ⊢ (𝑥 = 𝐴 → ((𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥) ↔ (𝐴 ⊆ 𝐴 → 𝑦 ∈ 𝐴))) |
7 | 6 | rspcv 3609 | . . . . 5 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥) → (𝐴 ⊆ 𝐴 → 𝑦 ∈ 𝐴))) |
8 | 3, 7 | mpii 46 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴)) |
9 | 2, 8 | biimtrid 241 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑦 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} → 𝑦 ∈ 𝐴)) |
10 | 9 | ssrdv 3989 | . 2 ⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ⊆ 𝐴) |
11 | ssintub 4971 | . . 3 ⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} | |
12 | 11 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}) |
13 | 10, 12 | eqssd 4000 | 1 ⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2104 ∀wral 3059 {crab 3430 ⊆ wss 3949 ∩ cint 4951 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-tru 1542 df-ex 1780 df-nf 1784 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-in 3956 df-ss 3966 df-int 4952 |
This theorem is referenced by: intmin2 4980 ordintdif 6415 uniordint 7793 onsucmin 7813 naddrid 8686 naddasslem1 8697 naddasslem2 8698 rankonidlem 9827 rankval4 9866 harsucnn 9997 mrcid 17563 lspid 20739 aspid 21650 cldcls 22768 spanid 30865 chsupid 30930 fldgenidfld 32675 igenidl2 37238 pclidN 39072 diaocN 40301 onuniintrab 42279 topclat 47712 toplatlub 47714 toplatjoin 47716 |
Copyright terms: Public domain | W3C validator |