Metamath Proof Explorer


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 ) ) )