Theorem scott0s 6153

Description: Theorem scheme version of scott0 6151. The collection of all x of minimum rank such that ph(x) is true, is not empty iff there is an x such that ph(x) holds.

Assertion

Ref	Expression
scott0s	|- (E.xph <-> {x | (ph /\ A.y([y / x]ph -> (rank` x) C_ (rank` y)))} =/= (/))

Distinct variable groups:   x,y   ph,y

Proof of Theorem scott0s

Step	Hyp	Ref	Expression
1		abn0 3131	. 2 |- ({x | ph} =/= (/) <-> E.xph)
2		scott0 6151	. . . 4 |- ({x | ph} = (/) <-> {z e. {x | ph} | A.y e. {x | ph} (rank` z) C_ (rank` y)} = (/))
3		ax-17 1634	. . . . . . 7 |- (y e. {x | ph} -> A.z y e. {x | ph})
4		hbab1 2160	. . . . . . 7 |- (y e. {x | ph} -> A.x y e. {x | ph})
5		ax-17 1634	. . . . . . . 8 |- ((rank` z) C_ (rank` y) -> A.x(rank` z) C_ (rank` y))
6	4, 5	hbral 2426	. . . . . . 7 |- (A.y e. {x | ph} (rank` z) C_ (rank` y) -> A.xA.y e. {x | ph} (rank` z) C_ (rank` y))
7		ax-17 1634	. . . . . . 7 |- (A.y e. {x | ph} (rank` x) C_ (rank` y) -> A.zA.y e. {x | ph} (rank` x) C_ (rank` y))
8		fveq2 4804	. . . . . . . . 9 |- (z = x -> (rank` z) = (rank` x))
9	8	sseq1d 2903	. . . . . . . 8 |- (z = x -> ((rank` z) C_ (rank` y) <-> (rank` x) C_ (rank` y)))
10	9	ralbidv 2403	. . . . . . 7 |- (z = x -> (A.y e. {x | ph} (rank` z) C_ (rank` y) <-> A.y e. {x | ph} (rank` x) C_ (rank` y)))
11	3, 4, 6, 7, 10	cbvrab 2693	. . . . . 6 |- {z e. {x | ph} | A.y e. {x | ph} (rank` z) C_ (rank` y)} = {x e. {x | ph} | A.y e. {x | ph} (rank` x) C_ (rank` y)}
12		df-rab 2392	. . . . . 6 |- {x e. {x | ph} | A.y e. {x | ph} (rank` x) C_ (rank` y)} = {x | (x e. {x | ph} /\ A.y e. {x | ph} (rank` x) C_ (rank` y))}
13		abid 2159	. . . . . . . 8 |- (x e. {x | ph} <-> ph)
14		df-ral 2389	. . . . . . . . 9 |- (A.y e. {x | ph} (rank` x) C_ (rank` y) <-> A.y(y e. {x | ph} -> (rank` x) C_ (rank` y)))
15		df-clab 2158	. . . . . . . . . . 11 |- (y e. {x | ph} <-> [y / x]ph)
16	15	imbi1i 375	. . . . . . . . . 10 |- ((y e. {x | ph} -> (rank` x) C_ (rank` y)) <-> ([y / x]ph -> (rank` x) C_ (rank` y)))
17	16	albii 1664	. . . . . . . . 9 |- (A.y(y e. {x | ph} -> (rank` x) C_ (rank` y)) <-> A.y([y / x]ph -> (rank` x) C_ (rank` y)))
18	14, 17	bitri 306	. . . . . . . 8 |- (A.y e. {x | ph} (rank` x) C_ (rank` y) <-> A.y([y / x]ph -> (rank` x) C_ (rank` y)))
19	13, 18	anbi12i 806	. . . . . . 7 |- ((x e. {x | ph} /\ A.y e. {x | ph} (rank` x) C_ (rank` y)) <-> (ph /\ A.y([y / x]ph -> (rank` x) C_ (rank` y))))
20	19	abbii 2284	. . . . . 6 |- {x | (x e. {x | ph} /\ A.y e. {x | ph} (rank` x) C_ (rank` y))} = {x | (ph /\ A.y([y / x]ph -> (rank` x) C_ (rank` y)))}
21	11, 12, 20	3eqtri 2194	. . . . 5 |- {z e. {x | ph} | A.y e. {x | ph} (rank` z) C_ (rank` y)} = {x | (ph /\ A.y([y / x]ph -> (rank` x) C_ (rank` y)))}
22	21	eqeq1i 2177	. . . 4 |- ({z e. {x | ph} | A.y e. {x | ph} (rank` z) C_ (rank` y)} = (/) <-> {x | (ph /\ A.y([y / x]ph -> (rank` x) C_ (rank` y)))} = (/))
23	2, 22	bitri 306	. . 3 |- ({x | ph} = (/) <-> {x | (ph /\ A.y([y / x]ph -> (rank` x) C_ (rank` y)))} = (/))
24	23	necon3bii 2326	. 2 |- ({x | ph} =/= (/) <-> {x | (ph /\ A.y([y / x]ph -> (rank` x) C_ (rank` y)))} =/= (/))
25	1, 24	bitr3i 309	1 |- (E.xph <-> {x | (ph /\ A.y([y / x]ph -> (rank` x) C_ (rank` y)))} =/= (/))

Syntax hints:   -> wi 3   <-> wb 231   /\ wa 433  A.wal 1613   = wceq 1615   e. wcel 1617  E.wex 1644  [wsbc 1843  {cab 2157   =/= wne 2295  A.wral 2385  {crab 2388   C_ wss 2859  (/)c0 3114  ` cfv 4163  rankcrnk 6030

This theorem is referenced by:  hta 6162

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-rab 2392  df-v 2571  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-int 3433  df-iin 3471  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fv 4179  df-rank 6032

Copyright terms: Public domain