Theorem intmin 4968

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.)

Assertion

Ref	Expression
intmin	⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} = 𝐴)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem intmin

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3484	. . . . 5 ⊢ 𝑦 ∈ V
2	1	elintrab 4960	. . . 4 ⊢ (𝑦 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ↔ ∀𝑥 ∈ 𝐵 (𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥))
3		ssid 4006	. . . . 5 ⊢ 𝐴 ⊆ 𝐴
4		sseq2 4010	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐴))
5		eleq2 2830	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴))
6	4, 5	imbi12d 344	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥) ↔ (𝐴 ⊆ 𝐴 → 𝑦 ∈ 𝐴)))
7	6	rspcv 3618	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥) → (𝐴 ⊆ 𝐴 → 𝑦 ∈ 𝐴)))
8	3, 7	mpii 46	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴))
9	2, 8	biimtrid 242	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑦 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} → 𝑦 ∈ 𝐴))
10	9	ssrdv 3989	. 2 ⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ⊆ 𝐴)
11		ssintub 4966	. . 3 ⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}
12	11	a1i 11	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥})
13	10, 12	eqssd 4001	1 ⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∀wral 3061  {crab 3436   ⊆ wss 3951  ∩ cint 4946

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-ss 3968  df-int 4947

This theorem is referenced by:  intmin2  4975  ordintdif  6434  uniordint  7821  onsucmin  7841  naddrid  8721  naddasslem1  8732  naddasslem2  8733  rankonidlem  9868  rankval4  9907  harsucnn  10038  mrcid  17656  lspid  20980  aspid  21895  cldcls  23050  spanid  31366  chsupid  31431  fldgenidfld  33319  igenidl2  38072  pclidN  39898  diaocN  41127  onuniintrab  43238  topclat  48887  toplatlub  48889  toplatjoin  48891