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

Metamath Proof Explorer

Theorem rankxplim2

Description: If the rank of a Cartesian product is a limit ordinal, so is the rank of the union of its arguments. (Contributed by NM, 19-Sep-2006)

Ref Expression
Hypotheses rankxplim.1 
|- A e. _V
rankxplim.2 
|- B e. _V
Assertion rankxplim2 
|- ( Lim ( rank ` ( A X. B ) ) -> Lim ( rank ` ( A u. B ) ) )

Proof

Step Hyp Ref Expression
1 rankxplim.1 
 |-  A e. _V
2 rankxplim.2 
 |-  B e. _V
3 0ellim 
 |-  ( Lim ( rank ` ( A X. B ) ) -> (/) e. ( rank ` ( A X. B ) ) )
4 n0i 
 |-  ( (/) e. ( rank ` ( A X. B ) ) -> -. ( rank ` ( A X. B ) ) = (/) )
5 3 4 syl 
 |-  ( Lim ( rank ` ( A X. B ) ) -> -. ( rank ` ( A X. B ) ) = (/) )
6 df-ne 
 |-  ( ( A X. B ) =/= (/) <-> -. ( A X. B ) = (/) )
7 1 2 xpex 
 |-  ( A X. B ) e. _V
8 7 rankeq0 
 |-  ( ( A X. B ) = (/) <-> ( rank ` ( A X. B ) ) = (/) )
9 8 notbii 
 |-  ( -. ( A X. B ) = (/) <-> -. ( rank ` ( A X. B ) ) = (/) )
10 6 9 bitr2i 
 |-  ( -. ( rank ` ( A X. B ) ) = (/) <-> ( A X. B ) =/= (/) )
11 5 10 sylib 
 |-  ( Lim ( rank ` ( A X. B ) ) -> ( A X. B ) =/= (/) )
12 limuni2 
 |-  ( Lim ( rank ` ( A X. B ) ) -> Lim U. ( rank ` ( A X. B ) ) )
13 limuni2 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> Lim U. U. ( rank ` ( A X. B ) ) )
14 12 13 syl 
 |-  ( Lim ( rank ` ( A X. B ) ) -> Lim U. U. ( rank ` ( A X. B ) ) )
15 rankuni 
 |-  ( rank ` U. U. ( A X. B ) ) = U. ( rank ` U. ( A X. B ) )
16 rankuni 
 |-  ( rank ` U. ( A X. B ) ) = U. ( rank ` ( A X. B ) )
17 16 unieqi 
 |-  U. ( rank ` U. ( A X. B ) ) = U. U. ( rank ` ( A X. B ) )
18 15 17 eqtr2i 
 |-  U. U. ( rank ` ( A X. B ) ) = ( rank ` U. U. ( A X. B ) )
19 unixp 
 |-  ( ( A X. B ) =/= (/) -> U. U. ( A X. B ) = ( A u. B ) )
20 19 fveq2d 
 |-  ( ( A X. B ) =/= (/) -> ( rank ` U. U. ( A X. B ) ) = ( rank ` ( A u. B ) ) )
21 18 20 eqtrid 
 |-  ( ( A X. B ) =/= (/) -> U. U. ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) )
22 limeq 
 |-  ( U. U. ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) -> ( Lim U. U. ( rank ` ( A X. B ) ) <-> Lim ( rank ` ( A u. B ) ) ) )
23 21 22 syl 
 |-  ( ( A X. B ) =/= (/) -> ( Lim U. U. ( rank ` ( A X. B ) ) <-> Lim ( rank ` ( A u. B ) ) ) )
24 14 23 imbitrid 
 |-  ( ( A X. B ) =/= (/) -> ( Lim ( rank ` ( A X. B ) ) -> Lim ( rank ` ( A u. B ) ) ) )
25 11 24 mpcom 
 |-  ( Lim ( rank ` ( A X. B ) ) -> Lim ( rank ` ( A u. B ) ) )