Theorem scott0 4689

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, contains at least one representative with the property, if there is one. In other words, the collection is empty iff no set has the property (i.e. A is empty).

Assertion

Ref	Expression
scott0	|- (A = (/) <-> {x e. A | A.y e. A (rank` x) (_ (rank` y)} = (/))

Distinct variable group:   x,y,A

Proof of Theorem scott0

Step	Hyp	Ref	Expression
1		rabeq 1800	. . 3 |- (A = (/) -> {x e. A | A.y e. A (rank` x) (_ (rank` y)} = {x e. (/) | A.y e. A (rank` x) (_ (rank` y)})
2		rab0 2283	. . 3 |- {x e. (/) | A.y e. A (rank` x) (_ (rank` y)} = (/)
3	1, 2	syl6eq 1515	. 2 |- (A = (/) -> {x e. A | A.y e. A (rank` x) (_ (rank` y)} = (/))
4		ne0 2278	. . . . . . . . 9 |- (A =/= (/) <-> E.x x e. A)
5		hbre1 1681	. . . . . . . . . 10 |- (E.x e. A (rank` x) = (rank` x) -> A.xE.x e. A (rank` x) = (rank` x))
6		eqid 1468	. . . . . . . . . . 11 |- (rank` x) = (rank` x)
7		ra4e 1687	. . . . . . . . . . 11 |- ((x e. A /\ (rank` x) = (rank` x)) -> E.x e. A (rank` x) = (rank` x))
8	6, 7	mpan2 694	. . . . . . . . . 10 |- (x e. A -> E.x e. A (rank` x) = (rank` x))
9	5, 8	19.23ai 1060	. . . . . . . . 9 |- (E.x x e. A -> E.x e. A (rank` x) = (rank` x))
10	4, 9	sylbi 199	. . . . . . . 8 |- (A =/= (/) -> E.x e. A (rank` x) = (rank` x))
11		fvex 3717	. . . . . . . . . . . 12 |- (rank` x) e. V
12		eqeq1 1473	. . . . . . . . . . . . 13 |- (y = (rank` x) -> (y = (rank` x) <-> (rank` x) = (rank` x)))
13	12	anbi2d 614	. . . . . . . . . . . 12 |- (y = (rank` x) -> ((x e. A /\ y = (rank` x)) <-> (x e. A /\ (rank` x) = (rank` x))))
14	11, 13	cla4ev 1860	. . . . . . . . . . 11 |- ((x e. A /\ (rank` x) = (rank` x)) -> E.y(x e. A /\ y = (rank` x)))
15	14	19.22i 1036	. . . . . . . . . 10 |- (E.x(x e. A /\ (rank` x) = (rank` x)) -> E.xE.y(x e. A /\ y = (rank` x)))
16		excom 1042	. . . . . . . . . 10 |- (E.yE.x(x e. A /\ y = (rank` x)) <-> E.xE.y(x e. A /\ y = (rank` x)))
17	15, 16	sylibr 200	. . . . . . . . 9 |- (E.x(x e. A /\ (rank` x) = (rank` x)) -> E.yE.x(x e. A /\ y = (rank` x)))
18		df-rex 1642	. . . . . . . . 9 |- (E.x e. A (rank` x) = (rank` x) <-> E.x(x e. A /\ (rank` x) = (rank` x)))
19		df-rex 1642	. . . . . . . . . 10 |- (E.x e. A y = (rank` x) <-> E.x(x e. A /\ y = (rank` x)))
20	19	exbii 1047	. . . . . . . . 9 |- (E.yE.x e. A y = (rank` x) <-> E.yE.x(x e. A /\ y = (rank` x)))
21	17, 18, 20	3imtr4 219	. . . . . . . 8 |- (E.x e. A (rank` x) = (rank` x) -> E.yE.x e. A y = (rank` x))
22	10, 21	syl 10	. . . . . . 7 |- (A =/= (/) -> E.yE.x e. A y = (rank` x))
23		abn0 2280	. . . . . . 7 |- ({y | E.x e. A y = (rank` x)} =/= (/) <-> E.yE.x e. A y = (rank` x))
24	22, 23	sylibr 200	. . . . . 6 |- (A =/= (/) -> {y | E.x e. A y = (rank` x)} =/= (/))
25		hbab1 1459	. . . . . . . . . 10 |- (z e. {y | E.x e. A y = (rank` x)} -> A.y z e. {y | E.x e. A y = (rank` x)})
26		ax-17 968	. . . . . . . . . 10 |- (z e. On -> A.y z e. On)
27	25, 26	dfss2f 2050	. . . . . . . . 9 |- ({y | E.x e. A y = (rank` x)} (_ On <-> A.y(y e. {y | E.x e. A y = (rank` x)} -> y e. On))
28		abid 1458	. . . . . . . . . 10 |- (y e. {y | E.x e. A y = (rank` x)} <-> E.x e. A y = (rank` x))
29		rankon 4643	. . . . . . . . . . . . 13 |- (rank` x) e. On
30		eleq1 1526	. . . . . . . . . . . . 13 |- (y = (rank` x) -> (y e. On <-> (rank` x) e. On))
31	29, 30	mpbiri 194	. . . . . . . . . . . 12 |- (y = (rank` x) -> y e. On)
32	31	a1i 8	. . . . . . . . . . 11 |- (x e. A -> (y = (rank` x) -> y e. On))
33	32	r19.23aiv 1735	. . . . . . . . . 10 |- (E.x e. A y = (rank` x) -> y e. On)
34	28, 33	sylbi 199	. . . . . . . . 9 |- (y e. {y | E.x e. A y = (rank` x)} -> y e. On)
35	27, 34	mpgbir 985	. . . . . . . 8 |- {y | E.x e. A y = (rank` x)} (_ On
36		onint 2996	. . . . . . . 8 |- (({y | E.x e. A y = (rank` x)} (_ On /\ {y | E.x e. A y = (rank` x)} =/= (/)) -> |^|{y | E.x e. A y = (rank` x)} e. {y | E.x e. A y = (rank` x)})
37	35, 36	mpan 693	. . . . . . 7 |- ({y | E.x e. A y = (rank` x)} =/= (/) -> |^|{y | E.x e. A y = (rank` x)} e. {y | E.x e. A y = (rank` x)})
38	11	dfiin2 2578	. . . . . . 7 |- |^|_x e. A (rank` x) = |^|{y | E.x e. A y = (rank` x)}
39	37, 38	syl5eqel 1544	. . . . . 6 |- ({y | E.x e. A y = (rank` x)} =/= (/) -> |^|_x e. A (rank` x) e. {y | E.x e. A y = (rank` x)})
40	24, 39	syl 10	. . . . 5 |- (A =/= (/) -> |^|_x e. A (rank` x) e. {y | E.x e. A y = (rank` x)})
41		hbii1 2575	. . . . . . . . 9 |- (y e. |^|_x e. A (rank` x) -> A.x y e. |^|_x e. A (rank` x))
42	41	hbeleq 1559	. . . . . . . 8 |- (y = |^|_x e. A (rank` x) -> A.x y = |^|_x e. A (rank` x))
43		eqeq1 1473	. . . . . . . 8 |- (y = |^|_x e. A (rank` x) -> (y = (rank` x) <-> |^|_x e. A (rank` x) = (rank` x)))
44	42, 43	rexbid 1654	. . . . . . 7 |- (y = |^|_x e. A (rank` x) -> (E.x e. A y = (rank` x) <-> E.x e. A |^|_x e. A (rank` x) = (rank` x)))
45	44	elabg 1890	. . . . . 6 |- (|^|_x e. A (rank` x) e. {y | E.x e. A y = (rank` x)} -> (|^|_x e. A (rank` x) e. {y | E.x e. A y = (rank` x)} <-> E.x e. A |^|_x e. A (rank` x) = (rank` x)))
46	45	ibi 590	. . . . 5 |- (|^|_x e. A (rank` x) e. {y | E.x e. A y = (rank` x)} -> E.x e. A |^|_x e. A (rank` x) = (rank` x))
47		sseq1 2072	. . . . . . . 8 |- (|^|_x e. A (rank` x) = (rank` x) -> (|^|_x e. A (rank` x) (_ (rank` y) <-> (rank` x) (_ (rank` y)))
48		ssid 2070	. . . . . . . . . 10 |- (rank` y) (_ (rank` y)
49		fveq2 3709	. . . . . . . . . . . 12 |- (x = y -> (rank` x) = (rank` y))
50	49	sseq1d 2078	. . . . . . . . . . 11 |- (x = y -> ((rank` x) (_ (rank` y) <-> (rank` y) (_ (rank` y)))
51	50	rcla4ev 1868	. . . . . . . . . 10 |- ((y e. A /\ (rank` y) (_ (rank` y)) -> E.x e. A (rank` x) (_ (rank` y))
52	48, 51	mpan2 694	. . . . . . . . 9 |- (y e. A -> E.x e. A (rank` x) (_ (rank` y))
53		iinss 2590	. . . . . . . . 9 |- (E.x e. A (rank` x) (_ (rank` y) -> |^|_x e. A (rank` x) (_ (rank` y))
54	52, 53	syl 10	. . . . . . . 8 |- (y e. A -> |^|_x e. A (rank` x) (_ (rank` y))
55	47, 54	syl5bi 208	. . . . . . 7 |- (|^|_x e. A (rank` x) = (rank` x) -> (y e. A -> (rank` x) (_ (rank` y)))
56	55	r19.21aiv 1705	. . . . . 6 |- (|^|_x e. A (rank` x) = (rank` x) -> A.y e. A (rank` x) (_ (rank` y))
57	56	r19.22si 1726	. . . . 5 |- (E.x e. A |^|_x e. A (rank` x) = (rank` x) -> E.x e. A A.y e. A (rank` x) (_ (rank` y))
58	40, 46, 57	3syl 20	. . . 4 |- (A =/= (/) -> E.x e. A A.y e. A (rank` x) (_ (rank` y))
59		rabn0 2282	. . . 4 |- ({x e. A | A.y e. A (rank` x) (_ (rank` y)} =/= (/) <-> E.x e. A A.y e. A (rank` x) (_ (rank` y))
60	58, 59	sylibr 200	. . 3 |- (A =/= (/) -> {x e. A | A.y e. A (rank` x) (_ (rank` y)} =/= (/))
61	60	necon4i 1617	. 2 |- ({x e. A | A.y e. A (rank` x) (_