Metamath Proof Explorer

Theorem alephadd

Description: The sum 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 alephadd 
|- ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( aleph ` A ) e. _V
2 fvex 
 |-  ( aleph ` B ) e. _V
3 djuex 
 |-  ( ( ( aleph ` A ) e. _V /\ ( aleph ` B ) e. _V ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) e. _V )
4 1 2 3 mp2an 
 |-  ( ( aleph ` A ) |_| ( aleph ` B ) ) e. _V
5 alephfnon 
 |-  aleph Fn On
6 5 fndmi 
 |-  dom aleph = On
7 6 eleq2i 
 |-  ( A e. dom aleph <-> A e. On )
8 7 notbii 
 |-  ( -. A e. dom aleph <-> -. A e. On )
9 6 eleq2i 
 |-  ( B e. dom aleph <-> B e. On )
10 9 notbii 
 |-  ( -. B e. dom aleph <-> -. B e. On )
11 df-dju 
 |-  ( (/) |_| (/) ) = ( ( { (/) } X. (/) ) u. ( { 1o } X. (/) ) )
12 xpundir 
 |-  ( ( { (/) } u. { 1o } ) X. (/) ) = ( ( { (/) } X. (/) ) u. ( { 1o } X. (/) ) )
13 xp0 
 |-  ( ( { (/) } u. { 1o } ) X. (/) ) = (/)
14 11 12 13 3eqtr2i 
 |-  ( (/) |_| (/) ) = (/)
15 ndmfv 
 |-  ( -. A e. dom aleph -> ( aleph ` A ) = (/) )
16 ndmfv 
 |-  ( -. B e. dom aleph -> ( aleph ` B ) = (/) )
17 djueq12 
 |-  ( ( ( aleph ` A ) = (/) /\ ( aleph ` B ) = (/) ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) = ( (/) |_| (/) ) )
18 15 16 17 syl2an 
 |-  ( ( -. A e. dom aleph /\ -. B e. dom aleph ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) = ( (/) |_| (/) ) )
19 15 adantr 
 |-  ( ( -. A e. dom aleph /\ -. B e. dom aleph ) -> ( aleph ` A ) = (/) )
20 16 adantl 
 |-  ( ( -. A e. dom aleph /\ -. B e. dom aleph ) -> ( aleph ` B ) = (/) )
21 19 20 uneq12d 
 |-  ( ( -. A e. dom aleph /\ -. B e. dom aleph ) -> ( ( aleph ` A ) u. ( aleph ` B ) ) = ( (/) u. (/) ) )
22 un0 
 |-  ( (/) u. (/) ) = (/)
23 21 22 eqtrdi 
 |-  ( ( -. A e. dom aleph /\ -. B e. dom aleph ) -> ( ( aleph ` A ) u. ( aleph ` B ) ) = (/) )
24 14 18 23 3eqtr4a 
 |-  ( ( -. A e. dom aleph /\ -. B e. dom aleph ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) = ( ( aleph ` A ) u. ( aleph ` B ) ) )
25 8 10 24 syl2anbr 
 |-  ( ( -. A e. On /\ -. B e. On ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) = ( ( aleph ` A ) u. ( aleph ` B ) ) )
26 eqeng 
 |-  ( ( ( aleph ` A ) |_| ( aleph ` B ) ) e. _V -> ( ( ( aleph ` A ) |_| ( aleph ` B ) ) = ( ( aleph ` A ) u. ( aleph ` B ) ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) ) ) )
27 4 25 26 mpsyl 
 |-  ( ( -. A e. On /\ -. B e. On ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) ) )
28 27 ex 
 |-  ( -. A e. On -> ( -. B e. On -> ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) ) ) )
29 alephgeom 
 |-  ( A e. On <-> _om C_ ( aleph ` A ) )
30 ssdomg 
 |-  ( ( aleph ` A ) e. _V -> ( _om C_ ( aleph ` A ) -> _om ~<_ ( aleph ` A ) ) )
31 1 30 ax-mp 
 |-  ( _om C_ ( aleph ` A ) -> _om ~<_ ( aleph ` A ) )
32 alephon 
 |-  ( aleph ` A ) e. On
33 onenon 
 |-  ( ( aleph ` A ) e. On -> ( aleph ` A ) e. dom card )
34 32 33 ax-mp 
 |-  ( aleph ` A ) e. dom card
35 alephon 
 |-  ( aleph ` B ) e. On
36 onenon 
 |-  ( ( aleph ` B ) e. On -> ( aleph ` B ) e. dom card )
37 35 36 ax-mp 
 |-  ( aleph ` B ) e. dom card
38 infdju 
 |-  ( ( ( aleph ` A ) e. dom card /\ ( aleph ` B ) e. dom card /\ _om ~<_ ( aleph ` A ) ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) ) )
39 34 37 38 mp3an12 
 |-  ( _om ~<_ ( aleph ` A ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) ) )
40 31 39 syl 
 |-  ( _om C_ ( aleph ` A ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) ) )
41 29 40 sylbi 
 |-  ( A e. On -> ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) ) )
42 alephgeom 
 |-  ( B e. On <-> _om C_ ( aleph ` B ) )
43 ssdomg 
 |-  ( ( aleph ` B ) e. _V -> ( _om C_ ( aleph ` B ) -> _om ~<_ ( aleph ` B ) ) )
44 2 43 ax-mp 
 |-  ( _om C_ ( aleph ` B ) -> _om ~<_ ( aleph ` B ) )
45 djucomen 
 |-  ( ( ( aleph ` A ) e. _V /\ ( aleph ` B ) e. _V ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` B ) |_| ( aleph ` A ) ) )
46 1 2 45 mp2an 
 |-  ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` B ) |_| ( aleph ` A ) )
47 infdju 
 |-  ( ( ( aleph ` B ) e. dom card /\ ( aleph ` A ) e. dom card /\ _om ~<_ ( aleph ` B ) ) -> ( ( aleph ` B ) |_| ( aleph ` A ) ) ~~ ( ( aleph ` B ) u. ( aleph ` A ) ) )
48 37 34 47 mp3an12 
 |-  ( _om ~<_ ( aleph ` B ) -> ( ( aleph ` B ) |_| ( aleph ` A ) ) ~~ ( ( aleph ` B ) u. ( aleph ` A ) ) )
49 entr 
 |-  ( ( ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` B ) |_| ( aleph ` A ) ) /\ ( ( aleph ` B ) |_| ( aleph ` A ) ) ~~ ( ( aleph ` B ) u. ( aleph ` A ) ) ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` B ) u. ( aleph ` A ) ) )
50 46 48 49 sylancr 
 |-  ( _om ~<_ ( aleph ` B ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` B ) u. ( aleph ` A ) ) )
51 uncom 
 |-  ( ( aleph ` B ) u. ( aleph ` A ) ) = ( ( aleph ` A ) u. ( aleph ` B ) )
52 50 51 breqtrdi 
 |-  ( _om ~<_ ( aleph ` B ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) ) )
53 44 52 syl 
 |-  ( _om C_ ( aleph ` B ) -> ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) ) )
54 42 53 sylbi 
 |-  ( B e. On -> ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) ) )
55 28 41 54 pm2.61ii 
 |-  ( ( aleph ` A ) |_| ( aleph ` B ) ) ~~ ( ( aleph ` A ) u. ( aleph ` B ) )