Theorem intmin 4931

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 3457	. . . . 5 ⊢ 𝑦 ∈ V
2	1	elintrab 4923	. . . 4 ⊢ (𝑦 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ↔ ∀𝑥 ∈ 𝐵 (𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥))
3		ssid 3956	. . . . 5 ⊢ 𝐴 ⊆ 𝐴
4		sseq2 3960	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐴))
5		eleq2 2851	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴))
6	4, 5	imbi12d 347	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥) ↔ (𝐴 ⊆ 𝐴 → 𝑦 ∈ 𝐴)))
7	6	rspcv 3575	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥) → (𝐴 ⊆ 𝐴 → 𝑦 ∈ 𝐴)))
8	3, 7	mpii 47	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴))
9	2, 8	biimtrid 245	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑦 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} → 𝑦 ∈ 𝐴))
10	9	ssrdv 3940	. 2 ⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ⊆ 𝐴)
11		ssintub 4929	. . 3 ⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}
12	11	a1i 11	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥})
13	10, 12	eqssd 3951	1 ⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3078  {crab 3414   ⊆ wss 3902  ∩ cint 4910

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-ss 3919  df-int 4911

This theorem is used by:  intmin2  4938  ordintdif  6413  uniordint  7804  onsucmin  7821  naddrid  8676  naddasslem1  8687  naddasslem2  8688  rankonidlem  9814  rankval4  9853  harsucnn  10007  mrcid  17707  lspid  21172  aspid  22095  cldcls  23273  spanid  31836  chsupid  31901  fldgenidfld  33766  rankval4b  35615  nmulrid  36785  igenidl2  38823  pclidN  40777  diaocN  42006  onuniintrab  44075  topclat  49932  toplatlub  49934  toplatjoin  49936