Theorem scott0 3542

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(s):   x,y,A

Proof of Theorem scott0

Step	Hyp	Ref	Expression
1		rabeq 1346	. . 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 1718	. . 3 |- {x e. (/) | A.y e. A (rank` x) (_ (rank` y)} = (/)
3	1, 2	syl6eq 1140	. 2 |- (A = (/) -> {x e. A | A.y e. A (rank` x) (_ (rank` y)} = (/))
4		n0 1714	. . . . . . . . 9 |- (-. A = (/) <-> E.x x e. A)
5		hbre1 1239	. . . . . . . . . 10 |- (E.x e. A (rank` x) = (rank` x) -> A.xE.x e. A (rank` x) = (rank` x))
6		cleqid 1102	. . . . . . . . . . 11 |- (rank` x) = (rank` x)
7		ra4e 1244	. . . . . . . . . . 11 |- ((x e. A /\ (rank` x) = (rank` x)) -> E.x e. A (rank` x) = (rank` x))
8	6, 7	mpan2 519	. . . . . . . . . 10 |- (x e. A -> E.x e. A (rank` x) = (rank` x))
9	5, 8	19.23ai 746	. . . . . . . . 9 |- (E.x x e. A -> E.x e. A (rank` x) = (rank` x))
10	4, 9	sylbi 174	. . . . . . . 8 |- (-. A = (/) -> E.x e. A (rank` x) = (rank` x))
11		fvex 2838	. . . . . . . . . . . 12 |- (rank` x) e. V
12		cleq1 1107	. . . . . . . . . . . . 13 |- (y = (rank` x) -> (y = (rank` x) <-> (rank` x) = (rank` x)))
13	12	anbi2d 468	. . . . . . . . . . . 12 |- (y = (rank` x) -> ((x e. A /\ y = (rank` x)) <-> (x e. A /\ (rank` x) = (rank` x))))
14	11, 13	cla4ev 1401	. . . . . . . . . . 11 |- ((x e. A /\ (rank` x) = (rank` x)) -> E.y(x e. A /\ y = (rank` x)))
15	14	19.22i 723	. . . . . . . . . 10 |- (E.x(x e. A /\ (rank` x) = (rank` x)) -> E.xE.y(x e. A /\ y = (rank` x)))
16		excom 728	. . . . . . . . . 10 |- (E.yE.x(x e. A /\ y = (rank` x)) <-> E.xE.y(x e. A /\ y = (rank` x)))
17	15, 16	sylibr 175	. . . . . . . . 9 |- (E.x(x e. A /\ (rank` x) = (rank` x)) -> E.yE.x(x e. A /\ y = (rank` x)))
18		df-rex 1206	. . . . . . . . 9 |- (E.x e. A (rank` x) = (rank` x) <-> E.x(x e. A /\ (rank` x) = (rank` x)))
19		df-rex 1206	. . . . . . . . . 10 |- (E.x e. A y = (rank` x) <-> E.x(x e. A /\ y = (rank` x)))
20	19	biex 733	. . . . . . . . 9 |- (E.yE.x e. A y = (rank` x) <-> E.yE.x(x e. A /\ y = (rank` x)))
21	17, 18, 20	3imtr4 192	. . . . . . . 8 |- (E.x e. A (rank` x) = (rank` x) -> E.yE.x e. A y = (rank` x))
22	10, 21	syl 12	. . . . . . 7 |- (-. A = (/) -> E.yE.x e. A y = (rank` x))
23		abn0 1715	. . . . . . 7 |- (-. {y | E.x e. A y = (rank` x)} = (/) <-> E.yE.x e. A y = (rank` x))
24	22, 23	sylibr 175	. . . . . 6 |- (-. A = (/) -> -. {y | E.x e. A y = (rank` x)} = (/))
25		hbab1 1095	. . . . . . . . . 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 925	. . . . . . . . . 10 |- (z e. On -> A.y z e. On)
27	25, 26	dfss2f 1499	. . . . . . . . 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 1094	. . . . . . . . . 10 |- (y e. {y | E.x e. A y = (rank` x)} <-> E.x e. A y = (rank` x))
29		rankon 3515	. . . . . . . . . . . . 13 |- (rank` x) e. On
30		eleq1 1149	. . . . . . . . . . . . 13 |- (y = (rank` x) -> (y e. On <-> (rank` x) e. On))
31	29, 30	mpbiri 169	. . . . . . . . . . . 12 |- (y = (rank` x) -> y e. On)
32	31	a1i 7	. . . . . . . . . . 11 |- (x e. A -> (y = (rank` x) -> y e. On))
33	32	r19.23aiv 1284	. . . . . . . . . 10 |- (E.x e. A y = (rank` x) -> y e. On)
34	28, 33	sylbi 174	. . . . . . . . 9 |- (y e. {y | E.x e. A y = (rank` x)} -> y e. On)
35	27, 34	mpgbir 686	. . . . . . . 8 |- {y | E.x e. A y = (rank` x)} (_ On
36		onint 2261	. . . . . . . 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 518	. . . . . . 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 2015	. . . . . . . 8 |- |^|x e. A (rank` x) = |^|{y | E.x e. A y = (rank` x)}
39	38	eleq1i 1152	. . . . . . 7 |- (|^|x e. A (rank` x) e. {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)})
40	37, 39	sylibr 175	. . . . . 6 |- (-. {y | E.x e. A y = (rank` x)} = (/) -> |^|x e. A (rank` x) e. {y | E.x e. A y = (rank` x)})
41	24, 40	syl 12	. . . . 5 |- (-. A = (/) -> |^|x e. A (rank` x) e. {y | E.x e. A y = (rank` x)})
42		hbii1 2013	. . . . . . . . 9 |- (y e. |^|x e. A (rank` x) -> A.x y e. |^|x e. A (rank` x))
43	42	hbeleq 1173	. . . . . . . 8 |- (y = |^|x e. A (rank` x) -> A.x y = |^|x e. A (rank` x))
44		cleq1 1107	. . . . . . . 8 |- (y = |^|x e. A (rank` x) -> (y = (rank` x) <-> |^|x e. A (rank` x) = (rank` x)))
45	43, 44	birexd 1218	. . . . . . 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)))
46	45	elabg 1417	. . . . . 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)))
47	46	ibi 449	. . . . 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))
48		sseq1 1521	. . . . . . . 8 |- (|^|x e. A (rank` x) = (rank` x) -> (|^|x e. A (rank` x) (_ (rank` y) <-> (rank` x) (_ (rank` y)))
49		ssid 1519	. . . . . . . . . 10 |- (rank` y) (_ (rank` y)
50		fveq2 2832	. . . . . . . . . . . 12 |- (x = y -> (rank` x) = (rank` y))
51	50	sseq1d 1527	. . . . . . . . . . 11 |- (x = y -> ((rank` x) (_ (rank` y) <-> (rank` y) (_ (rank` y)))
52	51	rcla4ev 1403	. . . . . . . . . 10 |- ((y e. A /\ (rank` y) (_ (rank` y)) -> E.x e. A (rank` x) (_ (rank` y))
53	49, 52	mpan2 519	. . . . . . . . 9 |- (y e. A -> E.x e. A (rank` x) (_ (rank` y))
54		iinss 2025	. . . . . . . . 9 |- (E.x e. A (rank` x) (_ (rank` y) -> |^|x e. A (rank` x) (_ (rank` y))
55	53, 54	syl 12	. . . . . . . 8 |- (y e. A -> |^|x e. A (rank` x) (_ (rank` y))
56	48, 55	syl5bi 183	. . . . . . 7 |- (|^|x e. A (rank` x) = (rank` x) -> (y e. A -> (rank` x) (_ (rank` y)))
57	56	r19.21aiv 1259	. . . . . 6 |- (|^|x e. A (rank` x) = (rank` x) -> A.y e. A (rank` x) (_ (rank` y))
58	57	r19.22si 1275	. . . . 5 |- (E.x e. A |^|x e. A (rank` x) = (rank` x) -> E.x e. A A.y e. A (rank` x) (_ (rank` y))
59	41, 47, 58	3syl 21	. . . 4 |- (-. A = (/) -> E.x e. A A.y e. A (rank` x) (_ (rank` y))
60		rabn0 1716	. . . 4 |- (-. {x e. A | A.y e. A (rank` x) (_ (rank` y)} = (/) <-> E.x e. A A.y e. A (rank` x) (_ (rank` y))
61	59, 60	sylibr 175	. . 3 |- (-. A = (/) -> -. {x e. A | A.y e. A (rank` x) (_ (rank` y)} = (/))
62	61	a3i 69	. 2 |- ({x e. A | A.y e. A (rank` x) (_