Theorem scott0 4717

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 1809	. . 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 2293	. . 3 |- {x e. (/) | A.y e. A (rank` x) (_ (rank` y)} = (/)
3	1, 2	syl6eq 1523	. 2 |- (A = (/) -> {x e. A | A.y e. A (rank` x) (_ (rank` y)} = (/))
4		ne0 2288	. . . . . . . . 9 |- (A =/= (/) <-> E.x x e. A)
5		hbre1 1689	. . . . . . . . . 10 |- (E.x e. A (rank` x) = (rank` x) -> A.xE.x e. A (rank` x) = (rank` x))
6		eqid 1475	. . . . . . . . . . 11 |- (rank` x) = (rank` x)
7		ra4e 1695	. . . . . . . . . . 11 |- ((x e. A /\ (rank` x) = (rank` x)) -> E.x e. A (rank` x) = (rank` x))
8	6, 7	mpan2 696	. . . . . . . . . 10 |- (x e. A -> E.x e. A (rank` x) = (rank` x))
9	5, 8	19.23ai 1064	. . . . . . . . 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 3732	. . . . . . . . . . . 12 |- (rank` x) e. V
12		eqeq1 1481	. . . . . . . . . . . . 13 |- (y = (rank` x) -> (y = (rank` x) <-> (rank` x) = (rank` x)))
13	12	anbi2d 616	. . . . . . . . . . . 12 |- (y = (rank` x) -> ((x e. A /\ y = (rank` x)) <-> (x e. A /\ (rank` x) = (rank` x))))
14	11, 13	cla4ev 1869	. . . . . . . . . . 11 |- ((x e. A /\ (rank` x) = (rank` x)) -> E.y(x e. A /\ y = (rank` x)))
15	14	19.22i 1040	. . . . . . . . . 10 |- (E.x(x e. A /\ (rank` x) = (rank` x)) -> E.xE.y(x e. A /\ y = (rank` x)))
16		excom 1046	. . . . . . . . . 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 1650	. . . . . . . . 9 |- (E.x e. A (rank` x) = (rank` x) <-> E.x(x e. A /\ (rank` x) = (rank` x)))
19		df-rex 1650	. . . . . . . . . 10 |- (E.x e. A y = (rank` x) <-> E.x(x e. A /\ y = (rank` x)))
20	19	exbii 1051	. . . . . . . . 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 2290	. . . . . . 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 1466	. . . . . . . . . 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 971	. . . . . . . . . 10 |- (z e. On -> A.y z e. On)
27	25, 26	dfss2f 2060	. . . . . . . . 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 1465	. . . . . . . . . 10 |- (y e. {y | E.x e. A y = (rank` x)} <-> E.x e. A y = (rank` x))
29		rankon 4671	. . . . . . . . . . . . 13 |- (rank` x) e. On
30		eleq1 1534	. . . . . . . . . . . . 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 1743	. . . . . . . . . 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 988	. . . . . . . 8 |- {y | E.x e. A y = (rank` x)} (_ On
36		onint 3006	. . . . . . . 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 695	. . . . . . 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 2588	. . . . . . 7 |- |^|_x e. A (rank` x) = |^|{y | E.x e. A y = (rank` x)}
39	37, 38	syl5eqel 1552	. . . . . 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 2585	. . . . . . . . 9 |- (y e. |^|_x e. A (rank` x) -> A.x y e. |^|_x e. A (rank` x))
42	41	hbeleq 1567	. . . . . . . 8 |- (y = |^|_x e. A (rank` x) -> A.x y = |^|_x e. A (rank` x))
43		eqeq1 1481	. . . . . . . 8 |- (y = |^|_x e. A (rank` x) -> (y = (rank` x) <-> |^|_x e. A (rank` x) = (rank` x)))
44	42, 43	rexbid 1662	. . . . . . 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 1899	. . . . . 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 592	. . . . 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 2082	. . . . . . . 8 |- (|^|_x e. A (rank` x) = (rank` x) -> (|^|_x e. A (rank` x) (_ (rank` y) <-> (rank` x) (_ (rank` y)))
48		ssid 2080	. . . . . . . . . 10 |- (rank` y) (_ (rank` y)
49		fveq2 3724	. . . . . . . . . . . 12 |- (x = y -> (rank` x) = (rank` y))
50	49	sseq1d 2088	. . . . . . . . . . 11 |- (x = y -> ((rank` x) (_ (rank` y) <-> (rank` y) (_ (rank` y)))
51	50	rcla4ev 1877	. . . . . . . . . 10 |- ((y e. A /\ (rank` y) (_ (rank` y)) -> E.x e. A (rank` x) (_ (rank` y))
52	48, 51	mpan2 696	. . . . . . . . 9 |- (y e. A -> E.x e. A (rank` x) (_ (rank` y))
53		iinss 2600	. . . . . . . . 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 1713	. . . . . 6 |- (|^|_x e. A (rank` x) = (rank` x) -> A.y e. A (rank` x) (_ (rank` y))
57	56	r19.22si 1734	. . . . 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 2292	. . . 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 1625	. 2 |- ({x e. A | A.y e. A (rank` x