Theorem alephmul

Description: The product of two alephs is their maximum. Equation 6.1 of Jech p. 42. (Contributed by NM, 29-Sep-2004) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	alephmul	|- ( ( A e. On /\ B e. On ) -> ( ( aleph ` A ) X. ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		alephgeom	|- ( A e. On <-> _om C_ ( aleph ` A ) )
2		fvex	|- ( aleph ` A ) e. _V
3		ssdomg	|- ( ( aleph ` A ) e. _V -> ( _om C_ ( aleph ` A ) -> _om ~<_ ( aleph ` A ) ) )
4	2 3	ax-mp	|- ( _om C_ ( aleph ` A ) -> _om ~<_ ( aleph ` A ) )
5	1 4	sylbi	|- ( A e. On -> _om ~<_ ( aleph ` A ) )
6		alephon	|- ( aleph ` A ) e. On
7		onenon	|- ( ( aleph ` A ) e. On -> ( aleph ` A ) e. dom card )
8	6 7	ax-mp	|- ( aleph ` A ) e. dom card
9	5 8	jctil	|- ( A e. On -> ( ( aleph ` A ) e. dom card /\ _om ~<_ ( aleph ` A ) ) )
10		alephgeom	|- ( B e. On <-> _om C_ ( aleph ` B ) )
11		fvex	|- ( aleph ` B ) e. _V
12		ssdomg	|- ( ( aleph ` B ) e. _V -> ( _om C_ ( aleph ` B ) -> _om ~<_ ( aleph ` B ) ) )
13	11 12	ax-mp	|- ( _om C_ ( aleph ` B ) -> _om ~<_ ( aleph ` B ) )
14		infn0	|- ( _om ~<_ ( aleph ` B ) -> ( aleph ` B ) =/= (/) )
15	13 14	syl	|- ( _om C_ ( aleph ` B ) -> ( aleph ` B ) =/= (/) )
16	10 15	sylbi	|- ( B e. On -> ( aleph ` B ) =/= (/) )
17		alephon	|- ( aleph ` B ) e. On
18		onenon	|- ( ( aleph ` B ) e. On -> ( aleph ` B ) e. dom card )
19	17 18	ax-mp	|- ( aleph ` B ) e. dom card
20	16 19	jctil	|- ( B e. On -> ( ( aleph ` B ) e. dom card /\ ( aleph ` B ) =/= (/) ) )
21		infxp	|- ( ( ( ( aleph ` A ) e. dom card /\ _om ~<_ ( aleph ` A ) ) /\ ( ( aleph ` B ) e. dom card /\ ( aleph ` B ) =/= (/) ) ) -> ( ( aleph ` A ) X. ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) ) )
22	9 20 21	syl2an	|- ( ( A e. On /\ B e. On ) -> ( ( aleph ` A ) X. ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) ) )