Theorem alephval3 4968

Description: An alternate way to express the value of the aleph function: it is the least infinite cardinal different from all values at smaller arguments. Definition of aleph in [Enderton] p. 212 and definition of aleph in [BellMachover] p. 490 .

Assertion

Ref	Expression
alephval3	|- (A e. On -> (aleph` A) = |^|{x | ((card` x) = x /\ om (_ x /\ A.y e. A -. x = (aleph` y))})

Distinct variable group:   x,y,A

Proof of Theorem alephval3

Step	Hyp	Ref	Expression
1		cardon 4890	. . . . . 6 |- (card` x) e. On
2		eleq1 1581	. . . . . 6 |- ((card` x) = x -> ((card` x) e. On <-> x e. On))
3	1, 2	mpbii 200	. . . . 5 |- ((card` x) = x -> x e. On)
4	3	3ad2ant1 812	. . . 4 |- (((card` x) = x /\ om (_ x /\ A.y e. A -. x = (aleph` y)) -> x e. On)
5	4	abssi 2173	. . 3 |- {x | ((card` x) = x /\ om (_ x /\ A.y e. A -. x = (aleph` y))} (_ On
6		oneqmini 3074	. . 3 |- ({x | ((card` x) = x /\ om (_ x /\ A.y e. A -. x = (aleph` y))} (_ On -> (((aleph` A) e. {x | ((card` x) = x /\ om (_ x /\ A.y e. A -. x = (aleph` y))} /\ A.z e. (aleph` A) -. z e. {x | ((card` x) = x /\ om (_ x /\ A.y e. A -. x = (aleph` y))}) -> (aleph` A) = |^|{x | ((card` x) = x /\ om (_ x /\ A.y e. A -. x = (aleph` y))}))
7	5, 6	ax-mp 7	. 2 |- (((aleph` A) e. {x | ((card` x) = x /\ om (_ x /\ A.y e. A -. x = (aleph` y))} /\ A.z e. (aleph` A) -. z e. {x | ((card` x) = x /\ om (_ x /\ A.y e. A -. x = (aleph` y))}) -> (aleph` A) = |^|{x | ((card` x) = x /\ om (_ x /\ A.y e. A -. x = (aleph` y))})
8		alephcard 4932	. . . . 5 |- (card` (aleph` A)) = (aleph` A)
9	8	a1i 8	. . . 4 |- (A e. On -> (card` (aleph` A)) = (aleph` A))
10		alephgeom 4947	. . . . 5 |- (A e. On <-> om (_ (aleph` A))
11	10	biimpi 158	. . . 4 |- (A e. On -> om (_ (aleph` A))
12		alephord2i 4942	. . . . . 6 |- (A e. On -> (y e. A -> (aleph` y) e. (aleph` A)))
13		elirr 4659	. . . . . . . 8 |- -. (aleph` y) e. (aleph` y)
14		eleq2 1582	. . . . . . . 8 |- ((aleph` A) = (aleph` y) -> ((aleph` y) e. (aleph` A) <-> (aleph` y) e. (aleph` y)))
15	13, 14	mtbiri 729	. . . . . . 7 |- ((aleph` A) = (aleph` y) -> -. (aleph` y) e. (aleph` A))
16	15	con2i 102	. . . . . 6 |- ((aleph` y) e. (aleph` A) -> -. (aleph` A) = (aleph` y))
17	12, 16	syl6 22	. . . . 5 |- (A e. On -> (y e. A -> -. (aleph` A) = (aleph` y)))
18	17	r19.21aiv 1760	. . . 4 |- (A e. On -> A.y e. A -. (aleph` A) = (aleph` y))
19	9, 11, 18	3jca 831	. . 3 |- (A e. On -> ((card` (aleph` A)) = (aleph` A) /\ om (_ (aleph` A) /\ A.y e. A -. (aleph` A) = (aleph` y)))
20		fvex 3789	. . . 4 |- (aleph` A) e. V
21		fveq2 3781	. . . . . 6 |- (x = (aleph` A) -> (card` x) = (card` (aleph` A)))
22		id 59	. . . . . 6 |- (x = (aleph` A) -> x = (aleph` A))
23	21, 22	eqeq12d 1536	. . . . 5 |- (x = (aleph` A) -> ((card` x) = x <-> (card` (aleph` A)) = (aleph` A)))
24		sseq2 2134	. . . . 5 |- (x = (aleph` A) -> (om (_ x <-> om (_ (aleph` A)))
25		eqeq1 1528	. . . . . . 7 |- (x = (aleph` A) -> (x = (aleph` y) <-> (aleph` A) = (aleph` y)))
26	25	notbid 622	. . . . . 6 |- (x = (aleph` A) -> (-. x = (aleph` y) <-> -. (aleph` A) = (aleph` y)))
27	26	ralbidv 1710	. . . . 5 |- (x = (aleph` A) -> (A.y e. A -. x = (aleph` y) <-> A.y e. A -. (aleph` A) = (aleph` y)))
28	23, 24, 27	3anbi123d 905	. . . 4 |- (x = (aleph` A) -> (((card` x) = x /\ om (_ x /\ A.y e. A -. x = (aleph` y)) <-> ((card` (aleph` A)) = (aleph` A) /\ om (_ (aleph` A) /\ A.y e. A -. (aleph` A) = (aleph` y))))
29	20, 28	elab 1944	. . 3 |- ((aleph` A) e. {x | ((card` x) = x /\ om (_ x /\ A.y e. A -. x = (aleph` y))} <-> ((card` (aleph` A)) = (aleph` A) /\ om (_ (aleph` A) /\ A.y e. A -. (aleph` A) = (aleph` y)))
30	19, 29	sylibr 207	. 2 |- (A e. On -> (aleph` A) e. {x | ((card` x) = x /\ om (_ x /\ A.y e. A -. x = (aleph` y))})
31		eleq1 1581	. . . . . . . . . . . . . . . 16 |- (z = (aleph` y) -> (z e. (aleph` A) <-> (aleph` y) e. (aleph` A)))
32		alephord2 4941	. . . . . . . . . . . . . . . . 17 |- ((y e. On /\ A e. On) -> (y e. A <-> (aleph` y) e. (aleph` A)))
33	32	bicomd 532	. . . . . . . . . . . . . . . 16 |- ((y e. On /\ A e. On) -> ((aleph` y) e. (aleph` A) <-> y e. A))
34	31, 33	sylan9bbr 552	. . . . . . . . . . . . . . 15 |- (((y e. On /\ A e. On) /\ z = (aleph` y)) -> (z e. (aleph` A) <-> y e. A))
35	34	biimpcd 162	. . . . . . . . . . . . . 14 |- (z e. (aleph` A) -> (((y e. On /\ A e. On) /\ z = (aleph` y)) -> y e. A))
36		pm3.27 330	. . . . . . . . . . . . . . 15 |- (((y e. On /\ A e. On) /\ z = (aleph` y)) -> z = (aleph` y))
37	36	a1i 8	. . . . . . . . . . . . . 14 |- (z e. (aleph` A) -> (((y e. On /\ A e. On) /\ z = (aleph` y)) -> z = (aleph` y)))
38	35, 37	jcad 611	. . . . . . . . . . . . 13 |- (z e. (aleph` A) -> (((y e. On /\ A e. On) /\ z = (aleph` y)) -> (y e. A /\ z = (aleph` y))))
39	38	exp4c 389	. . . . . . . . . . . 12 |- (z e. (aleph` A) -> (y e. On -> (A e. On -> (z = (aleph` y) -> (y e. A /\ z = (aleph` y))))))
40	39	com3r 35	. . . . . . . . . . 11 |- (A e. On -> (z e. (aleph` A) -> (y e. On -> (z = (aleph` y) -> (y e. A /\ z = (aleph` y))))))
41	40	imp4b 372	. . . . . . . . . 10 |- ((A e. On /\ z e. (aleph` A)) -> ((y e. On /\ z = (aleph` y)) -> (y e. A /\ z = (aleph` y))))
42	41	r19.22dv2 1783	. . . . . . . . 9 |- ((A e. On /\ z e. (aleph` A)) -> (E.y e. On z = (aleph` y) -> E.y e. A z = (aleph` y)))
43		cardalephex 4951	. . . . . . . . . 10 |- (om (_ z -> ((card` z) = z <-> E.y e. On z = (aleph` y)))
44	43	biimpac 427	. . . . . . . . 9 |- (((card` z) = z /\ om (_ z) -> E.y e. On z = (aleph` y))
45	42, 44	syl5 21	. . . . . . . 8 |- ((A e. On /\ z e. (aleph` A)) -> (((card` z) = z /\ om (_ z) -> E.y e. A z = (aleph` y)))
46	45	imp 357	. . . . . . 7 |- (((A e. On /\ z e. (aleph` A)) /\ ((card` z) = z /\ om (_ z)) -> E.y e. A z = (aleph` y))
47		dfrex2 1703	. . . . . . 7 |- (E.y e. A z = (aleph` y) <-> -. A.y e. A -. z = (aleph` y))
48	46, 47	sylib 205	. . . . . 6 |- (((A e. On /\ z e. (aleph` A)) /\ ((card` z) = z /\ om (_ z)) -> -. A.y e. A -. z = (aleph` y))
49		nan 701	. . . . . 6 |- (((A e. On /\ z e. (aleph` A)) -> -. (((card` z) = z /\ om (_ z) /\ A.y e. A -. z = (aleph` y))) <-> (((A e. On /\ z e. (aleph` A)) /\ ((card` z) = z /\ om (_ z)) -> -. A.y e. A -. z = (aleph` y)))
50	48, 49	mpbir 197	. . . . 5 |- ((A e. On /\ z e. (aleph` A)) -> -. (((card` z) = z /\ om (_ z) /\ A.y e. A -. z = (aleph` y)))
51	50	ex 380	. . . 4 |- (A e. On -> (z e. (aleph` A) -> -. (((card` z) = z /\ om (_ z)