Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem scottex 4688

Description: Scott's trick collects all sets that have a certain property and are of smallest possible rank. This theorem shows that the resulting collection, expressed as in Equation 9.3 of [Jech] p. 72, is a set.

Assertion

Ref	Expression
scottex

Distinct variable group:   ,,

---

Proof of Theorem scottex

Step	Hyp	Ref	Expression
1		0ex 2701	. . . 4
2		eleq1 1526	. . . 4
3	1, 2	mpbiri 194	. . 3
4		rabexg 2714	. . 3
5	3, 4	syl 10	. 2
6		n0 2279	. . 3
7		hbra1 1679	. . . . . 6
8		ax-17 968	. . . . . 6
9	7, 8	hbrab 1765	. . . . 5
10		ax-17 968	. . . . 5
11	9, 10	hbel 1558	. . . 4
12		ra4 1686	. . . . . . . . 9
13	12	com12 11	. . . . . . . 8
14	13	a1d 12	. . . . . . 7
15	14	r19.21aiv 1705	. . . . . 6
16		ss2rab 2113	. . . . . 6
17	15, 16	sylibr 200	. . . . 5
18		rankon 4643	. . . . . . . 8
19		fveq2 3709	. . . . . . . . . . . 12
20	19	sseq1d 2078	. . . . . . . . . . 11
21	20	elrab 1896	. . . . . . . . . 10
22	21	pm3.27bi 326	. . . . . . . . 9
23	22	rgen 1690	. . . . . . . 8
24		sseq2 2073	. . . . . . . . . 10
25	24	ralbidv 1655	. . . . . . . . 9
26	25	rcla4ev 1868	. . . . . . . 8
27	18, 23, 26	mp2an 695	. . . . . . 7
28		bndrank 4654	. . . . . . 7
29	27, 28	ax-mp 7	. . . . . 6
30	29	ssex 2709	. . . . 5
31	17, 30	syl 10	. . . 4
32	11, 31	19.23ai 1060	. . 3
33	6, 32	sylbi 199	. 2
34	5, 33	pm2.61i 126	1

Colors of variables: wff set class

Syntax hints:   wn 2   wi 3   wceq 953   wcel 955  wex 977  wral 1637  wrex 1638  crab 1640  cvv 1802   wss 2037  c0 2270  con0 2938  cfv 3172  crnk 4614

This theorem is referenced by:  scottexs 4690  cplem2 4693  kardex 4697

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-reg 4565  ax-inf2 4597

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-rab 1644  df-v 1803  df-sbc 1932  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-if 2352  df-pw 2392  df-sn 2402  df-pr 2403  df-tp 2405  df-op 2406  df-uni 2494  df-int 2524  df-iun 2558  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-id 2824  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941  df-on 2942  df-lim 2943  df-suc 2944  df-om 3122  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-fv 3188  df-rdg 3917  df-r1 4615  df-rank 4616

Copyright terms: Public domain