Theorem infenomsub 5889

Description: An infinite ordinal is equinumerous to an infinite initial ordinal. (Contributed by Jeff Hankins, 23-Oct-2009.)

Assertion

Ref	Expression
infenomsub	|- ((A e. On /\ om C_ A) -> E.x e. ran aleph x ~~ A)

Distinct variable group:   x,A

Proof of Theorem infenomsub

Step	Hyp	Ref	Expression
1		alephfnon 5873	. . . 4 |- aleph Fn On
2	1	a1i 8	. . 3 |- ((A e. On /\ om C_ A) -> aleph Fn On)
3		omsubindss 5888	. . . . . . 7 |- (A e. On -> A C_ (aleph` A))
4		ssdomg 5467	. . . . . . 7 |- (A e. On -> (A C_ (aleph` A) -> A ~<_ (aleph` A)))
5	3, 4	mpd 29	. . . . . 6 |- (A e. On -> A ~<_ (aleph` A))
6		fveq2 4681	. . . . . . . 8 |- (y = A -> (aleph` y) = (aleph` A))
7	6	breq2d 3350	. . . . . . 7 |- (y = A -> (A ~<_ (aleph` y) <-> A ~<_ (aleph` A)))
8	7	rcla4ev 2381	. . . . . 6 |- ((A e. On /\ A ~<_ (aleph` A)) -> E.y e. On A ~<_ (aleph` y))
9	5, 8	mpdan 768	. . . . 5 |- (A e. On -> E.y e. On A ~<_ (aleph` y))
10	9	adantr 425	. . . 4 |- ((A e. On /\ om C_ A) -> E.y e. On A ~<_ (aleph` y))
11		onintrab2 3883	. . . 4 |- (E.y e. On A ~<_ (aleph` y) <-> |^|{y e. On | A ~<_ (aleph` y)} e. On)
12	10, 11	sylib 215	. . 3 |- ((A e. On /\ om C_ A) -> |^|{y e. On | A ~<_ (aleph` y)} e. On)
13		fnfvelrn 4786	. . 3 |- ((aleph Fn On /\ |^|{y e. On | A ~<_ (aleph` y)} e. On) -> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) e. ran aleph)
14	2, 12, 13	syl11anc 524	. 2 |- ((A e. On /\ om C_ A) -> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) e. ran aleph)
15		eloni 3667	. . . . 5 |- (|^|{y e. On | A ~<_ (aleph` y)} e. On -> Ord |^|{y e. On | A ~<_ (aleph` y)})
16		ordzsl 3927	. . . . . 6 |- (Ord |^|{y e. On | A ~<_ (aleph` y)} <-> (|^|{y e. On | A ~<_ (aleph` y)} = (/) \/ E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)}))
17		3orass 861	. . . . . 6 |- ((|^|{y e. On | A ~<_ (aleph` y)} = (/) \/ E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)}) <-> (|^|{y e. On | A ~<_ (aleph` y)} = (/) \/ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})))
18	16, 17	bitri 190	. . . . 5 |- (Ord |^|{y e. On | A ~<_ (aleph` y)} <-> (|^|{y e. On | A ~<_ (aleph` y)} = (/) \/ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})))
19	15, 18	sylib 215	. . . 4 |- (|^|{y e. On | A ~<_ (aleph` y)} e. On -> (|^|{y e. On | A ~<_ (aleph` y)} = (/) \/ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})))
20	12, 19	syl 12	. . 3 |- ((A e. On /\ om C_ A) -> (|^|{y e. On | A ~<_ (aleph` y)} = (/) \/ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})))
21		fveq2 4681	. . . . . . . . . 10 |- (|^|{y e. On | A ~<_ (aleph` y)} = (/) -> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) = (aleph` (/)))
22	21	breq1d 3348	. . . . . . . . 9 |- (|^|{y e. On | A ~<_ (aleph` y)} = (/) -> ((aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~<_ A <-> (aleph` (/)) ~<_ A))
23		aleph0 5874	. . . . . . . . . . 11 |- (aleph` (/)) = om
24	23	sseq1i 2641	. . . . . . . . . 10 |- ((aleph` (/)) C_ A <-> om C_ A)
25		fvex 4689	. . . . . . . . . . 11 |- (aleph` (/)) e. _V
26		ssdomg 5467	. . . . . . . . . . 11 |- ((aleph` (/)) e. _V -> ((aleph` (/)) C_ A -> (aleph` (/)) ~<_ A))
27	25, 26	ax-mp 7	. . . . . . . . . 10 |- ((aleph` (/)) C_ A -> (aleph` (/)) ~<_ A)
28	24, 27	sylbir 218	. . . . . . . . 9 |- (om C_ A -> (aleph` (/)) ~<_ A)
29	22, 28	syl5bir 227	. . . . . . . 8 |- (|^|{y e. On | A ~<_ (aleph` y)} = (/) -> (om C_ A -> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~<_ A))
30		ax-17 1317	. . . . . . . . . . . 12 |- (x e. A -> A.y x e. A)
31		ax-17 1317	. . . . . . . . . . . 12 |- (x e. ~<_ -> A.y x e. ~<_ )
32		ax-17 1317	. . . . . . . . . . . . 13 |- (x e. aleph -> A.y x e. aleph)
33		hbrab1 2257	. . . . . . . . . . . . . 14 |- (x e. {y e. On | A ~<_ (aleph` y)} -> A.y x e. {y e. On | A ~<_ (aleph` y)})
34	33	hbint 3225	. . . . . . . . . . . . 13 |- (x e. |^|{y e. On | A ~<_ (aleph` y)} -> A.y x e. |^|{y e. On | A ~<_ (aleph` y)})
35	32, 34	hbfv 4686	. . . . . . . . . . . 12 |- (x e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}) -> A.y x e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}))
36	30, 31, 35	hbbr 3381	. . . . . . . . . . 11 |- (A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)}) -> A.y A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)}))
37		fveq2 4681	. . . . . . . . . . . 12 |- (y = |^|{y e. On | A ~<_ (aleph` y)} -> (aleph` y) = (aleph` |^|{y e. On | A ~<_ (aleph` y)}))
38	37	breq2d 3350	. . . . . . . . . . 11 |- (y = |^|{y e. On | A ~<_ (aleph` y)} -> (A ~<_ (aleph` y) <-> A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)})))
39	36, 38	onminsb 3879	. . . . . . . . . 10 |- (E.y e. On A ~<_ (aleph` y) -> A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)}))
40	9, 39	syl 12	. . . . . . . . 9 |- (A e. On -> A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)}))
41	40	a1i 8	. . . . . . . 8 |- (|^|{y e. On | A ~<_ (aleph` y)} = (/) -> (A e. On -> A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)})))
42	29, 41	anim12d 617	. . . . . . 7 |- (|^|{y e. On | A ~<_ (aleph` y)} = (/) -> ((om C_ A /\ A e. On) -> ((aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~<_ A /\ A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)}))))
43	42	com12 14	. . . . . 6 |- ((om C_ A /\ A e. On) -> (|^|{y e. On | A ~<_ (aleph` y)} = (/) -> ((aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~<_ A /\ A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)}))))
44	43	ancoms 484	. . . . 5 |- ((A e. On /\ om C_ A) -> (|^|{y e. On | A ~<_ (aleph` y)} = (/) -> ((aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~<_ A /\ A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)}))))
45		sbthbg 5521	. . . . . 6 |- (A e. On -> (((aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~<_ A /\ A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)})) <-> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~~ A))
46	45	adantr 425	. . . . 5 |- ((A e. On /\ om C_ A) -> (((aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~<_ A /\ A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)})) <-> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~~ A))
47	44, 46	sylibd 219	. . . 4 |- ((A e. On /\ om C_ A) -> (|^|{y e. On | A ~<_ (aleph` y)} = (/) -> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~~ A))
48		fvex 4689	. . . . . . 7 |- (aleph` |^|{y e. On | A ~<_ (aleph` y)}) e. _V
49	48	a1i 8	. . . . . 6 |- (((A e. On /\ om C_ A) /\ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})) -> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) e. _V)
50		bren2 5448	. . . . . . 7 |- (A ~~ (aleph` |^|{y e. On | A ~<_ (aleph` y)}) <-> (A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)}) /\ -. A ~< (aleph` |^|{y e. On | A ~<_ (aleph` y)})))
51	10, 39	syl 12	. . . . . . . 8 |- ((A e. On /\ om C_ A) -> A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)}))
52	51	adantr 425	. . . . . . 7 |- (((A e. On /\ om C_ A) /\ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})) -> A ~<_ (aleph` |^|{y e. On | A ~<_ (aleph` y)}))
53		simplr 449	. . . . . . . . . . . . . . 15 |- (((A e. On /\ z e. On) /\ |^|{y e. On | A ~<_ (aleph` y)} = suc z) -> z e. On)
54		visset 2295	. . . . . . . . . . . . . . . . . 18 |- z e. _V
55	54	sucid 3744	. . . . . . . . . . . . . . . . 17 |- z e. suc z
56		eleq2 1958	. . . . . . . . . . . . . . . . 17 |- (|^|{y e. On | A ~<_ (aleph` y)} = suc z -> (z e. |^|{y e. On | A ~<_ (aleph` y)} <-> z e. suc z))
57	55, 56	mpbiri 211	. . . . . . . . . . . . . . . 16 |- (|^|{y e. On | A ~<_ (aleph` y)} = suc z -> z e. |^|{y e. On | A ~<_ (aleph` y)})
58	57	adantl 424	. . . . . . . . . . . . . . 15 |- (((A e. On /\ z e. On) /\ |^|{y e. On | A ~<_ (aleph` y)} = suc z) -> z e. |^|{y e. On | A ~<_ (aleph` y)})
59		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (y = z -> (aleph` y) = (aleph` z))
60	59	breq2d 3350	. . . . . . . . . . . . . . . 16 |- (y = z -> (A ~<_ (aleph` y) <-> A ~<_ (aleph` z)))
61	60	onnminsb 3885	. . . . . . . . . . . . . . 15 |- (z e. On -> (z e. |^|{y e. On | A ~<_ (aleph` y)} -> -. A ~<_ (aleph` z)))
62	53, 58, 61	sylc 83	. . . . . . . . . . . . . 14 |- (((A e. On /\ z e. On) /\ |^|{y e. On | A ~<_ (aleph` y)} = suc z) -> -. A ~<_ (aleph` z))
63		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (|^|{y e. On | A ~<_ (aleph` y)} = suc z -> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) = (aleph` suc z))
64	63	eleq2d 1964	. . . . . . . . . . . . . . . 16 |- (|^|{y e. On | A ~<_ (aleph` y)} = suc z -> (A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}) <-> A e. (aleph` suc z)))
65		omsubsuc2 5878	. . . . . . . . . . . . . . . . . 18 |- (z e. On -> (aleph` suc z) = {y e. On | y ~<_ (aleph` z)})
66	65	eleq2d 1964	. . . . . . . . . . . . . . . . 17 |- (z e. On -> (A e. (aleph` suc z) <-> A e. {y e. On | y ~<_ (aleph` z)}))
67	66	adantl 424	. . . . . . . . . . . . . . . 16 |- ((A e. On /\ z e. On) -> (A e. (aleph` suc z) <-> A e. {y e. On | y ~<_ (aleph` z)}))
68	64, 67	sylan9bbr 600	. . . . . . . . . . . . . . 15 |- (((A e. On /\ z e. On) /\ |^|{y e. On | A ~<_ (aleph` y)} = suc z) -> (A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}) <-> A e. {y e. On | y ~<_ (aleph` z)}))
69		breq1 3341	. . . . . . . . . . . . . . . . 17 |- (y = A -> (y ~<_ (aleph` z) <-> A ~<_ (aleph` z)))
70	69	elrab 2414	. . . . . . . . . . . . . . . 16 |- (A e. {y e. On | y ~<_ (aleph` z)} <-> (A e. On /\ A ~<_ (aleph` z)))
71	70	simprbi 353	. . . . . . . . . . . . . . 15 |- (A e. {y e. On | y ~<_ (aleph` z)} -> A ~<_ (aleph` z))
72	68, 71	syl6bi 231	. . . . . . . . . . . . . 14 |- (((A e. On /\ z e. On) /\ |^|{y e. On | A ~<_ (aleph` y)} = suc z) -> (A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}) -> A ~<_ (aleph` z)))
73	62, 72	mtod 123	. . . . . . . . . . . . 13 |- (((A e. On /\ z e. On) /\ |^|{y e. On | A ~<_ (aleph` y)} = suc z) -> -. A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}))
74	73	exp31 407	. . . . . . . . . . . 12 |- (A e. On -> (z e. On -> (|^|{y e. On | A ~<_ (aleph` y)} = suc z -> -. A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}))))
75	74	r19.23adv 2215	. . . . . . . . . . 11 |- (A e. On -> (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z -> -. A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)})))
76	9, 11	sylib 215	. . . . . . . . . . . . . . . . . 18 |- (A e. On -> |^|{y e. On | A ~<_ (aleph` y)} e. On)
77		onelon 3683	. . . . . . . . . . . . . . . . . . 19 |- ((|^|{y e. On | A ~<_ (aleph` y)} e. On /\ z e. |^|{y e. On | A ~<_ (aleph` y)}) -> z e. On)
78	77	ex 402	. . . . . . . . . . . . . . . . . 18 |- (|^|{y e. On | A ~<_ (aleph` y)} e. On -> (z e. |^|{y e. On | A ~<_ (aleph` y)} -> z e. On))
79	76, 78	syl 12	. . . . . . . . . . . . . . . . 17 |- (A e. On -> (z e. |^|{y e. On | A ~<_ (aleph` y)} -> z e. On))
80	79, 61	syli 65	. . . . . . . . . . . . . . . 16 |- (A e. On -> (z e. |^|{y e. On | A ~<_ (aleph` y)} -> -. A ~<_ (aleph` z)))
81	80	adantr 425	. . . . . . . . . . . . . . 15 |- ((A e. On /\ Lim |^|{y e. On | A ~<_ (aleph` y)}) -> (z e. |^|{y e. On | A ~<_ (aleph` y)} -> -. A ~<_ (aleph` z)))
82	81	r19.21aiv 2175	. . . . . . . . . . . . . 14 |- ((A e. On /\ Lim |^|{y e. On | A ~<_ (aleph` y)}) -> A.z e. |^|{y e. On | A ~<_ (aleph` y)} -. A ~<_ (aleph` z))
83		ralnex 2113	. . . . . . . . . . . . . 14 |- (A.z e. |^|{y e. On | A ~<_ (aleph` y)} -. A ~<_ (aleph` z) <-> -. E.z e. |^|{y e. On | A ~<_ (aleph` y)}A ~<_ (aleph` z))
84	82, 83	sylib 215	. . . . . . . . . . . . 13 |- ((A e. On /\ Lim |^|{y e. On | A ~<_ (aleph` y)}) -> -. E.z e. |^|{y e. On | A ~<_ (aleph` y)}A ~<_ (aleph` z))
85		alephlim 5875	. . . . . . . . . . . . . . . 16 |- ((|^|{y e. On | A ~<_ (aleph` y)} e. On /\ Lim |^|{y e. On | A ~<_ (aleph` y)}) -> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) = U_z e. |^|{y e. On | A ~<_ (aleph` y)} (aleph` z))
86	85	eleq2d 1964	. . . . . . . . . . . . . . 15 |- ((|^|{y e. On | A ~<_ (aleph` y)} e. On /\ Lim |^|{y e. On | A ~<_ (aleph` y)}) -> (A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}) <-> A e. U_z e. |^|{y e. On | A ~<_ (aleph` y)} (aleph` z)))
87	86, 76	sylan 497	. . . . . . . . . . . . . 14 |- ((A e. On /\ Lim |^|{y e. On | A ~<_ (aleph` y)}) -> (A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}) <-> A e. U_z e. |^|{y e. On | A ~<_ (aleph` y)} (aleph` z)))
88		ssdomg 5467	. . . . . . . . . . . . . . . . . . . 20 |- (A e. On -> (A C_ (aleph` z) -> A ~<_ (aleph` z)))
89	88	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- ((A e. On /\ z e. |^|{y e. On | A ~<_ (aleph` y)}) -> (A C_ (aleph` z) -> A ~<_ (aleph` z)))
90		alephon 5876	. . . . . . . . . . . . . . . . . . . 20 |- (aleph` z) e. On
91		onelss 3705	. . . . . . . . . . . . . . . . . . . 20 |- ((aleph` z) e. On -> (A e. (aleph` z) -> A C_ (aleph` z)))
92	90, 91	ax-mp 7	. . . . . . . . . . . . . . . . . . 19 |- (A e. (aleph` z) -> A C_ (aleph` z))
93	89, 92	syl5 20	. . . . . . . . . . . . . . . . . 18 |- ((A e. On /\ z e. |^|{y e. On | A ~<_ (aleph` y)}) -> (A e. (aleph` z) -> A ~<_ (aleph` z)))
94	93	ex 402	. . . . . . . . . . . . . . . . 17 |- (A e. On -> (z e. |^|{y e. On | A ~<_ (aleph` y)} -> (A e. (aleph` z) -> A ~<_ (aleph` z))))
95	94	adantr 425	. . . . . . . . . . . . . . . 16 |- ((A e. On /\ Lim |^|{y e. On | A ~<_ (aleph` y)}) -> (z e. |^|{y e. On | A ~<_ (aleph` y)} -> (A e. (aleph` z) -> A ~<_ (aleph` z))))
96	95	reximdvai 2201	. . . . . . . . . . . . . . 15 |- ((A e. On /\ Lim |^|{y e. On | A ~<_ (aleph` y)}) -> (E.z e. |^|{y e. On | A ~<_ (aleph` y)}A e. (aleph` z) -> E.z e. |^|{y e. On | A ~<_ (aleph` y)}A ~<_ (aleph` z)))
97		eliun 3259	. . . . . . . . . . . . . . 15 |- (A e. U_z e. |^|{y e. On | A ~<_ (aleph` y)} (aleph` z) <-> E.z e. |^|{y e. On | A ~<_ (aleph` y)}A e. (aleph` z))
98	96, 97	syl5ib 223	. . . . . . . . . . . . . 14 |- ((A e. On /\ Lim |^|{y e. On | A ~<_ (aleph` y)}) -> (A e. U_z e. |^|{y e. On | A ~<_ (aleph` y)} (aleph` z) -> E.z e. |^|{y e. On | A ~<_ (aleph` y)}A ~<_ (aleph` z)))
99	87, 98	sylbid 220	. . . . . . . . . . . . 13 |- ((A e. On /\ Lim |^|{y e. On | A ~<_ (aleph` y)}) -> (A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}) -> E.z e. |^|{y e. On | A ~<_ (aleph` y)}A ~<_ (aleph` z)))
100	84, 99	mtod 123	. . . . . . . . . . . 12 |- ((A e. On /\ Lim |^|{y e. On | A ~<_ (aleph` y)}) -> -. A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}))
101	100	ex 402	. . . . . . . . . . 11 |- (A e. On -> (Lim |^|{y e. On | A ~<_ (aleph` y)} -> -. A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)})))
102	75, 101	jaod 469	. . . . . . . . . 10 |- (A e. On -> ((E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)}) -> -. A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)})))
103	102	imp 377	. . . . . . . . 9 |- ((A e. On /\ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})) -> -. A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}))
104		simpl 346	. . . . . . . . . 10 |- ((A e. On /\ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})) -> A e. On)
105	76	adantr 425	. . . . . . . . . 10 |- ((A e. On /\ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})) -> |^|{y e. On | A ~<_ (aleph` y)} e. On)
106		elomsubsd 5885	. . . . . . . . . 10 |- ((A e. On /\ |^|{y e. On | A ~<_ (aleph` y)} e. On) -> (A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}) <-> A ~< (aleph` |^|{y e. On | A ~<_ (aleph` y)})))
107	104, 105, 106	syl11anc 524	. . . . . . . . 9 |- ((A e. On /\ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})) -> (A e. (aleph` |^|{y e. On | A ~<_ (aleph` y)}) <-> A ~< (aleph` |^|{y e. On | A ~<_ (aleph` y)})))
108	103, 107	mtbid 782	. . . . . . . 8 |- ((A e. On /\ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})) -> -. A ~< (aleph` |^|{y e. On | A ~<_ (aleph` y)}))
109	108	adantlr 429	. . . . . . 7 |- (((A e. On /\ om C_ A) /\ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})) -> -. A ~< (aleph` |^|{y e. On | A ~<_ (aleph` y)}))
110	50, 52, 109	sylanbrc 527	. . . . . 6 |- (((A e. On /\ om C_ A) /\ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})) -> A ~~ (aleph` |^|{y e. On | A ~<_ (aleph` y)}))
111		ensymg 5470	. . . . . 6 |- ((aleph` |^|{y e. On | A ~<_ (aleph` y)}) e. _V -> (A ~~ (aleph` |^|{y e. On | A ~<_ (aleph` y)}) -> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~~ A))
112	49, 110, 111	sylc 83	. . . . 5 |- (((A e. On /\ om C_ A) /\ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})) -> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~~ A)
113	112	ex 402	. . . 4 |- ((A e. On /\ om C_ A) -> ((E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)}) -> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~~ A))
114	47, 113	jaod 469	. . 3 |- ((A e. On /\ om C_ A) -> ((|^|{y e. On | A ~<_ (aleph` y)} = (/) \/ (E.z e. On |^|{y e. On | A ~<_ (aleph` y)} = suc z \/ Lim |^|{y e. On | A ~<_ (aleph` y)})) -> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~~ A))
115	20, 114	mpd 29	. 2 |- ((A e. On /\ om C_ A) -> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~~ A)
116		breq1 3341	. . 3 |- (x = (aleph` |^|{y e. On | A ~<_ (aleph` y)}) -> (x ~~ A <-> (aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~~ A))
117	116	rcla4ev 2381	. 2 |- (((aleph` |^|{y e. On | A ~<_ (aleph` y)}) e. ran aleph /\ (aleph` |^|{y e. On | A ~<_ (aleph` y)}) ~~ A) -> E.x e. ran aleph x ~~ A)
118	14, 115, 117	syl11anc 524	1 |- ((A e. On /\ om C_ A) -> E.x e. ran aleph x ~~ A)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   \/ w3o 857   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   C_ wss 2593  (/)c0 2875  |^|cint 3214  U_ciun 3255   class class class wbr 3338  Ord word 3656  Oncon0 3657  Lim wlim 3658  suc csuc 3659  omcom 3949  ran crn 3987   Fn wfn 3993  ` cfv 3998   ~~ cen 5423   ~<_ cdom 5424   ~< csdm 5425  alephcale 5860

This theorem is referenced by:  omsubinit 5890  omsubinitOLD 15399

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-iso 4015  df-oprab 4887  df-rdg 5140  df-er 5318  df-en 5427  df-dom 5428  df-sdom 5429  df-fin 5430  df-aleph 5863

Copyright terms: Public domain