Metamath Proof Explorer

Theorem rankxplim

Description: The rank of a Cartesian product when the rank of the union of its arguments is a limit ordinal. Part of Exercise 4 of Kunen p. 107. See rankxpsuc for the successor case. (Contributed by NM, 19-Sep-2006)

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

Proof

Step Hyp Ref Expression
1 rankxplim.1 
 |-  A e. _V
2 rankxplim.2 
 |-  B e. _V
3 pwuni 
 |-  <. x , y >. C_ ~P U. <. x , y >.
4 vex 
 |-  x e. _V
5 vex 
 |-  y e. _V
6 4 5 uniop 
 |-  U. <. x , y >. = { x , y }
7 6 pweqi 
 |-  ~P U. <. x , y >. = ~P { x , y }
8 3 7 sseqtri 
 |-  <. x , y >. C_ ~P { x , y }
9 pwuni 
 |-  { x , y } C_ ~P U. { x , y }
10 4 5 unipr 
 |-  U. { x , y } = ( x u. y )
11 10 pweqi 
 |-  ~P U. { x , y } = ~P ( x u. y )
12 9 11 sseqtri 
 |-  { x , y } C_ ~P ( x u. y )
13 12 sspwi 
 |-  ~P { x , y } C_ ~P ~P ( x u. y )
14 8 13 sstri 
 |-  <. x , y >. C_ ~P ~P ( x u. y )
15 4 5 unex 
 |-  ( x u. y ) e. _V
16 15 pwex 
 |-  ~P ( x u. y ) e. _V
17 16 pwex 
 |-  ~P ~P ( x u. y ) e. _V
18 17 rankss 
 |-  ( <. x , y >. C_ ~P ~P ( x u. y ) -> ( rank ` <. x , y >. ) C_ ( rank ` ~P ~P ( x u. y ) ) )
19 14 18 ax-mp 
 |-  ( rank ` <. x , y >. ) C_ ( rank ` ~P ~P ( x u. y ) )
20 1 rankel 
 |-  ( x e. A -> ( rank ` x ) e. ( rank ` A ) )
21 2 rankel 
 |-  ( y e. B -> ( rank ` y ) e. ( rank ` B ) )
22 4 5 1 2 rankelun 
 |-  ( ( ( rank ` x ) e. ( rank ` A ) /\ ( rank ` y ) e. ( rank ` B ) ) -> ( rank ` ( x u. y ) ) e. ( rank ` ( A u. B ) ) )
23 20 21 22 syl2an 
 |-  ( ( x e. A /\ y e. B ) -> ( rank ` ( x u. y ) ) e. ( rank ` ( A u. B ) ) )
24 23 adantl 
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ ( x e. A /\ y e. B ) ) -> ( rank ` ( x u. y ) ) e. ( rank ` ( A u. B ) ) )
25 ranklim 
 |-  ( Lim ( rank ` ( A u. B ) ) -> ( ( rank ` ( x u. y ) ) e. ( rank ` ( A u. B ) ) <-> ( rank ` ~P ( x u. y ) ) e. ( rank ` ( A u. B ) ) ) )
26 ranklim 
 |-  ( Lim ( rank ` ( A u. B ) ) -> ( ( rank ` ~P ( x u. y ) ) e. ( rank ` ( A u. B ) ) <-> ( rank ` ~P ~P ( x u. y ) ) e. ( rank ` ( A u. B ) ) ) )
27 25 26 bitrd 
 |-  ( Lim ( rank ` ( A u. B ) ) -> ( ( rank ` ( x u. y ) ) e. ( rank ` ( A u. B ) ) <-> ( rank ` ~P ~P ( x u. y ) ) e. ( rank ` ( A u. B ) ) ) )
28 27 adantr 
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ ( x e. A /\ y e. B ) ) -> ( ( rank ` ( x u. y ) ) e. ( rank ` ( A u. B ) ) <-> ( rank ` ~P ~P ( x u. y ) ) e. ( rank ` ( A u. B ) ) ) )
29 24 28 mpbid 
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ ( x e. A /\ y e. B ) ) -> ( rank ` ~P ~P ( x u. y ) ) e. ( rank ` ( A u. B ) ) )
30 rankon 
 |-  ( rank ` <. x , y >. ) e. On
31 rankon 
 |-  ( rank ` ( A u. B ) ) e. On
32 ontr2 
 |-  ( ( ( rank ` <. x , y >. ) e. On /\ ( rank ` ( A u. B ) ) e. On ) -> ( ( ( rank ` <. x , y >. ) C_ ( rank ` ~P ~P ( x u. y ) ) /\ ( rank ` ~P ~P ( x u. y ) ) e. ( rank ` ( A u. B ) ) ) -> ( rank ` <. x , y >. ) e. ( rank ` ( A u. B ) ) ) )
33 30 31 32 mp2an 
 |-  ( ( ( rank ` <. x , y >. ) C_ ( rank ` ~P ~P ( x u. y ) ) /\ ( rank ` ~P ~P ( x u. y ) ) e. ( rank ` ( A u. B ) ) ) -> ( rank ` <. x , y >. ) e. ( rank ` ( A u. B ) ) )
34 19 29 33 sylancr 
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ ( x e. A /\ y e. B ) ) -> ( rank ` <. x , y >. ) e. ( rank ` ( A u. B ) ) )
35 30 31 onsucssi 
 |-  ( ( rank ` <. x , y >. ) e. ( rank ` ( A u. B ) ) <-> suc ( rank ` <. x , y >. ) C_ ( rank ` ( A u. B ) ) )
36 34 35 sylib 
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ ( x e. A /\ y e. B ) ) -> suc ( rank ` <. x , y >. ) C_ ( rank ` ( A u. B ) ) )
37 36 ralrimivva 
 |-  ( Lim ( rank ` ( A u. B ) ) -> A. x e. A A. y e. B suc ( rank ` <. x , y >. ) C_ ( rank ` ( A u. B ) ) )
38 fveq2 
 |-  ( z = <. x , y >. -> ( rank ` z ) = ( rank ` <. x , y >. ) )
39 suceq 
 |-  ( ( rank ` z ) = ( rank ` <. x , y >. ) -> suc ( rank ` z ) = suc ( rank ` <. x , y >. ) )
40 38 39 syl 
 |-  ( z = <. x , y >. -> suc ( rank ` z ) = suc ( rank ` <. x , y >. ) )
41 40 sseq1d 
 |-  ( z = <. x , y >. -> ( suc ( rank ` z ) C_ ( rank ` ( A u. B ) ) <-> suc ( rank ` <. x , y >. ) C_ ( rank ` ( A u. B ) ) ) )
42 41 ralxp 
 |-  ( A. z e. ( A X. B ) suc ( rank ` z ) C_ ( rank ` ( A u. B ) ) <-> A. x e. A A. y e. B suc ( rank ` <. x , y >. ) C_ ( rank ` ( A u. B ) ) )
43 1 2 xpex 
 |-  ( A X. B ) e. _V
44 43 rankbnd 
 |-  ( A. z e. ( A X. B ) suc ( rank ` z ) C_ ( rank ` ( A u. B ) ) <-> ( rank ` ( A X. B ) ) C_ ( rank ` ( A u. B ) ) )
45 42 44 bitr3i 
 |-  ( A. x e. A A. y e. B suc ( rank ` <. x , y >. ) C_ ( rank ` ( A u. B ) ) <-> ( rank ` ( A X. B ) ) C_ ( rank ` ( A u. B ) ) )
46 37 45 sylib 
 |-  ( Lim ( rank ` ( A u. B ) ) -> ( rank ` ( A X. B ) ) C_ ( rank ` ( A u. B ) ) )
47 46 adantr 
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ ( A X. B ) =/= (/) ) -> ( rank ` ( A X. B ) ) C_ ( rank ` ( A u. B ) ) )
48 1 2 rankxpl 
 |-  ( ( A X. B ) =/= (/) -> ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) )
49 48 adantl 
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ ( A X. B ) =/= (/) ) -> ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) )
50 47 49 eqssd 
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ ( A X. B ) =/= (/) ) -> ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) )