This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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