Theorem alephdom

Description: Relationship between inclusion of ordinal numbers and dominance of infinite initial ordinals. (Contributed by Jeff Hankins, 23-Oct-2009)

	Ref	Expression
Assertion	alephdom	|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( aleph ` A ) ~<_ ( aleph ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		onsseleq	|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
2		alephord	|- ( ( A e. On /\ B e. On ) -> ( A e. B <-> ( aleph ` A ) ~< ( aleph ` B ) ) )
3		sdomdom	|- ( ( aleph ` A ) ~< ( aleph ` B ) -> ( aleph ` A ) ~<_ ( aleph ` B ) )
4	2 3	syl6bi	|- ( ( A e. On /\ B e. On ) -> ( A e. B -> ( aleph ` A ) ~<_ ( aleph ` B ) ) )
5		fvex	|- ( aleph ` A ) e. _V
6		fveq2	|- ( A = B -> ( aleph ` A ) = ( aleph ` B ) )
7		eqeng	|- ( ( aleph ` A ) e. _V -> ( ( aleph ` A ) = ( aleph ` B ) -> ( aleph ` A ) ~~ ( aleph ` B ) ) )
8	5 6 7	mpsyl	|- ( A = B -> ( aleph ` A ) ~~ ( aleph ` B ) )
9	8	a1i	|- ( ( A e. On /\ B e. On ) -> ( A = B -> ( aleph ` A ) ~~ ( aleph ` B ) ) )
10		endom	|- ( ( aleph ` A ) ~~ ( aleph ` B ) -> ( aleph ` A ) ~<_ ( aleph ` B ) )
11	9 10	syl6	|- ( ( A e. On /\ B e. On ) -> ( A = B -> ( aleph ` A ) ~<_ ( aleph ` B ) ) )
12	4 11	jaod	|- ( ( A e. On /\ B e. On ) -> ( ( A e. B \/ A = B ) -> ( aleph ` A ) ~<_ ( aleph ` B ) ) )
13	1 12	sylbid	|- ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( aleph ` A ) ~<_ ( aleph ` B ) ) )
14		eloni	|- ( B e. On -> Ord B )
15		eloni	|- ( A e. On -> Ord A )
16		ordtri2or	|- ( ( Ord B /\ Ord A ) -> ( B e. A \/ A C_ B ) )
17	14 15 16	syl2anr	|- ( ( A e. On /\ B e. On ) -> ( B e. A \/ A C_ B ) )
18	17	ord	|- ( ( A e. On /\ B e. On ) -> ( -. B e. A -> A C_ B ) )
19	18	con1d	|- ( ( A e. On /\ B e. On ) -> ( -. A C_ B -> B e. A ) )
20		alephord	|- ( ( B e. On /\ A e. On ) -> ( B e. A <-> ( aleph ` B ) ~< ( aleph ` A ) ) )
21	20	ancoms	|- ( ( A e. On /\ B e. On ) -> ( B e. A <-> ( aleph ` B ) ~< ( aleph ` A ) ) )
22		sdomnen	|- ( ( aleph ` B ) ~< ( aleph ` A ) -> -. ( aleph ` B ) ~~ ( aleph ` A ) )
23		sdomdom	|- ( ( aleph ` B ) ~< ( aleph ` A ) -> ( aleph ` B ) ~<_ ( aleph ` A ) )
24		sbth	|- ( ( ( aleph ` B ) ~<_ ( aleph ` A ) /\ ( aleph ` A ) ~<_ ( aleph ` B ) ) -> ( aleph ` B ) ~~ ( aleph ` A ) )
25	24	ex	|- ( ( aleph ` B ) ~<_ ( aleph ` A ) -> ( ( aleph ` A ) ~<_ ( aleph ` B ) -> ( aleph ` B ) ~~ ( aleph ` A ) ) )
26	23 25	syl	|- ( ( aleph ` B ) ~< ( aleph ` A ) -> ( ( aleph ` A ) ~<_ ( aleph ` B ) -> ( aleph ` B ) ~~ ( aleph ` A ) ) )
27	22 26	mtod	|- ( ( aleph ` B ) ~< ( aleph ` A ) -> -. ( aleph ` A ) ~<_ ( aleph ` B ) )
28	21 27	syl6bi	|- ( ( A e. On /\ B e. On ) -> ( B e. A -> -. ( aleph ` A ) ~<_ ( aleph ` B ) ) )
29	19 28	syld	|- ( ( A e. On /\ B e. On ) -> ( -. A C_ B -> -. ( aleph ` A ) ~<_ ( aleph ` B ) ) )
30	13 29	impcon4bid	|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( aleph ` A ) ~<_ ( aleph ` B ) ) )