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

Metamath Proof Explorer

Theorem rankxplim3

Description: The rank of a Cartesian product is a limit ordinal iff its union is. (Contributed by NM, 19-Sep-2006)

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

Proof

Step Hyp Ref Expression
1 rankxplim.1 
 |-  A e. _V
2 rankxplim.2 
 |-  B e. _V
3 limuni2 
 |-  ( Lim ( rank ` ( A X. B ) ) -> Lim U. ( rank ` ( A X. B ) ) )
4 0ellim 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> (/) e. U. ( rank ` ( A X. B ) ) )
5 n0i 
 |-  ( (/) e. U. ( rank ` ( A X. B ) ) -> -. U. ( rank ` ( A X. B ) ) = (/) )
6 unieq 
 |-  ( ( rank ` ( A X. B ) ) = (/) -> U. ( rank ` ( A X. B ) ) = U. (/) )
7 uni0 
 |-  U. (/) = (/)
8 6 7 eqtrdi 
 |-  ( ( rank ` ( A X. B ) ) = (/) -> U. ( rank ` ( A X. B ) ) = (/) )
9 8 con3i 
 |-  ( -. U. ( rank ` ( A X. B ) ) = (/) -> -. ( rank ` ( A X. B ) ) = (/) )
10 4 5 9 3syl 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> -. ( rank ` ( A X. B ) ) = (/) )
11 rankon 
 |-  ( rank ` ( A u. B ) ) e. On
12 11 onsuci 
 |-  suc ( rank ` ( A u. B ) ) e. On
13 12 onsuci 
 |-  suc suc ( rank ` ( A u. B ) ) e. On
14 13 elexi 
 |-  suc suc ( rank ` ( A u. B ) ) e. _V
15 14 sucid 
 |-  suc suc ( rank ` ( A u. B ) ) e. suc suc suc ( rank ` ( A u. B ) )
16 13 onsuci 
 |-  suc suc suc ( rank ` ( A u. B ) ) e. On
17 ontri1 
 |-  ( ( suc suc suc ( rank ` ( A u. B ) ) e. On /\ suc suc ( rank ` ( A u. B ) ) e. On ) -> ( suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) <-> -. suc suc ( rank ` ( A u. B ) ) e. suc suc suc ( rank ` ( A u. B ) ) ) )
18 16 13 17 mp2an 
 |-  ( suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) <-> -. suc suc ( rank ` ( A u. B ) ) e. suc suc suc ( rank ` ( A u. B ) ) )
19 18 con2bii 
 |-  ( suc suc ( rank ` ( A u. B ) ) e. suc suc suc ( rank ` ( A u. B ) ) <-> -. suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) )
20 15 19 mpbi 
 |-  -. suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) )
21 1 2 rankxpu 
 |-  ( rank ` ( A X. B ) ) C_ suc suc ( rank ` ( A u. B ) )
22 sstr 
 |-  ( ( suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) /\ ( rank ` ( A X. B ) ) C_ suc suc ( rank ` ( A u. B ) ) ) -> suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) )
23 21 22 mpan2 
 |-  ( suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) -> suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) )
24 20 23 mto 
 |-  -. suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) )
25 reeanv 
 |-  ( E. x e. On E. y e. On ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) <-> ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) )
26 simprl 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> ( rank ` ( A u. B ) ) = suc x )
27 simpr 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( rank ` ( A u. B ) ) = suc x ) -> ( rank ` ( A u. B ) ) = suc x )
28 df-ne 
 |-  ( ( A X. B ) =/= (/) <-> -. ( A X. B ) = (/) )
29 1 2 xpex 
 |-  ( A X. B ) e. _V
30 29 rankeq0 
 |-  ( ( A X. B ) = (/) <-> ( rank ` ( A X. B ) ) = (/) )
31 30 notbii 
 |-  ( -. ( A X. B ) = (/) <-> -. ( rank ` ( A X. B ) ) = (/) )
32 28 31 bitr2i 
 |-  ( -. ( rank ` ( A X. B ) ) = (/) <-> ( A X. B ) =/= (/) )
33 10 32 sylib 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( A X. B ) =/= (/) )
34 unixp 
 |-  ( ( A X. B ) =/= (/) -> U. U. ( A X. B ) = ( A u. B ) )
35 33 34 syl 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> U. U. ( A X. B ) = ( A u. B ) )
36 35 fveq2d 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( rank ` U. U. ( A X. B ) ) = ( rank ` ( A u. B ) ) )
37 rankuni 
 |-  ( rank ` U. U. ( A X. B ) ) = U. ( rank ` U. ( A X. B ) )
38 rankuni 
 |-  ( rank ` U. ( A X. B ) ) = U. ( rank ` ( A X. B ) )
39 38 unieqi 
 |-  U. ( rank ` U. ( A X. B ) ) = U. U. ( rank ` ( A X. B ) )
40 37 39 eqtri 
 |-  ( rank ` U. U. ( A X. B ) ) = U. U. ( rank ` ( A X. B ) )
41 36 40 eqtr3di 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( rank ` ( A u. B ) ) = U. U. ( rank ` ( A X. B ) ) )
42 eqimss 
 |-  ( ( rank ` ( A u. B ) ) = U. U. ( rank ` ( A X. B ) ) -> ( rank ` ( A u. B ) ) C_ U. U. ( rank ` ( A X. B ) ) )
43 41 42 syl 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( rank ` ( A u. B ) ) C_ U. U. ( rank ` ( A X. B ) ) )
44 43 adantr 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( rank ` ( A u. B ) ) = suc x ) -> ( rank ` ( A u. B ) ) C_ U. U. ( rank ` ( A X. B ) ) )
45 27 44 eqsstrrd 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( rank ` ( A u. B ) ) = suc x ) -> suc x C_ U. U. ( rank ` ( A X. B ) ) )
46 45 adantrr 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc x C_ U. U. ( rank ` ( A X. B ) ) )
47 limuni 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> U. ( rank ` ( A X. B ) ) = U. U. ( rank ` ( A X. B ) ) )
48 47 adantr 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> U. ( rank ` ( A X. B ) ) = U. U. ( rank ` ( A X. B ) ) )
49 46 48 sseqtrrd 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc x C_ U. ( rank ` ( A X. B ) ) )
50 vex 
 |-  x e. _V
51 rankon 
 |-  ( rank ` ( A X. B ) ) e. On
52 51 onordi 
 |-  Ord ( rank ` ( A X. B ) )
53 orduni 
 |-  ( Ord ( rank ` ( A X. B ) ) -> Ord U. ( rank ` ( A X. B ) ) )
54 52 53 ax-mp 
 |-  Ord U. ( rank ` ( A X. B ) )
55 ordelsuc 
 |-  ( ( x e. _V /\ Ord U. ( rank ` ( A X. B ) ) ) -> ( x e. U. ( rank ` ( A X. B ) ) <-> suc x C_ U. ( rank ` ( A X. B ) ) ) )
56 50 54 55 mp2an 
 |-  ( x e. U. ( rank ` ( A X. B ) ) <-> suc x C_ U. ( rank ` ( A X. B ) ) )
57 49 56 sylibr 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> x e. U. ( rank ` ( A X. B ) ) )
58 limsuc 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( x e. U. ( rank ` ( A X. B ) ) <-> suc x e. U. ( rank ` ( A X. B ) ) ) )
59 58 adantr 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> ( x e. U. ( rank ` ( A X. B ) ) <-> suc x e. U. ( rank ` ( A X. B ) ) ) )
60 57 59 mpbid 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc x e. U. ( rank ` ( A X. B ) ) )
61 26 60 eqeltrd 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) )
62 limsuc 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) <-> suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) ) )
63 62 adantr 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> ( ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) <-> suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) ) )
64 61 63 mpbid 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) )
65 ordsucelsuc 
 |-  ( Ord U. ( rank ` ( A X. B ) ) -> ( suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) <-> suc suc ( rank ` ( A u. B ) ) e. suc U. ( rank ` ( A X. B ) ) ) )
66 54 65 ax-mp 
 |-  ( suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) <-> suc suc ( rank ` ( A u. B ) ) e. suc U. ( rank ` ( A X. B ) ) )
67 64 66 sylib 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc suc ( rank ` ( A u. B ) ) e. suc U. ( rank ` ( A X. B ) ) )
68 onsucuni2 
 |-  ( ( ( rank ` ( A X. B ) ) e. On /\ ( rank ` ( A X. B ) ) = suc y ) -> suc U. ( rank ` ( A X. B ) ) = ( rank ` ( A X. B ) ) )
69 51 68 mpan 
 |-  ( ( rank ` ( A X. B ) ) = suc y -> suc U. ( rank ` ( A X. B ) ) = ( rank ` ( A X. B ) ) )
70 69 ad2antll 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc U. ( rank ` ( A X. B ) ) = ( rank ` ( A X. B ) ) )
71 67 70 eleqtrd 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc suc ( rank ` ( A u. B ) ) e. ( rank ` ( A X. B ) ) )
72 13 51 onsucssi 
 |-  ( suc suc ( rank ` ( A u. B ) ) e. ( rank ` ( A X. B ) ) <-> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) )
73 71 72 sylib 
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) )
74 73 ex 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) )
75 74 a1d 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( ( x e. On /\ y e. On ) -> ( ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) ) )
76 75 rexlimdvv 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( E. x e. On E. y e. On ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) )
77 25 76 biimtrrid 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) )
78 24 77 mtoi 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) )
79 ianor 
 |-  ( -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) <-> ( -. E. x e. On ( rank ` ( A u. B ) ) = suc x \/ -. E. y e. On ( rank ` ( A X. B ) ) = suc y ) )
80 un00 
 |-  ( ( A = (/) /\ B = (/) ) <-> ( A u. B ) = (/) )
81 animorl 
 |-  ( ( A = (/) /\ B = (/) ) -> ( A = (/) \/ B = (/) ) )
82 80 81 sylbir 
 |-  ( ( A u. B ) = (/) -> ( A = (/) \/ B = (/) ) )
83 xpeq0 
 |-  ( ( A X. B ) = (/) <-> ( A = (/) \/ B = (/) ) )
84 82 83 sylibr 
 |-  ( ( A u. B ) = (/) -> ( A X. B ) = (/) )
85 84 con3i 
 |-  ( -. ( A X. B ) = (/) -> -. ( A u. B ) = (/) )
86 31 85 sylbir 
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> -. ( A u. B ) = (/) )
87 1 2 unex 
 |-  ( A u. B ) e. _V
88 87 rankeq0 
 |-  ( ( A u. B ) = (/) <-> ( rank ` ( A u. B ) ) = (/) )
89 88 notbii 
 |-  ( -. ( A u. B ) = (/) <-> -. ( rank ` ( A u. B ) ) = (/) )
90 86 89 sylib 
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> -. ( rank ` ( A u. B ) ) = (/) )
91 11 onordi 
 |-  Ord ( rank ` ( A u. B ) )
92 ordzsl 
 |-  ( Ord ( rank ` ( A u. B ) ) <-> ( ( rank ` ( A u. B ) ) = (/) \/ E. x e. On ( rank ` ( A u. B ) ) = suc x \/ Lim ( rank ` ( A u. B ) ) ) )
93 91 92 mpbi 
 |-  ( ( rank ` ( A u. B ) ) = (/) \/ E. x e. On ( rank ` ( A u. B ) ) = suc x \/ Lim ( rank ` ( A u. B ) ) )
94 93 3ori 
 |-  ( ( -. ( rank ` ( A u. B ) ) = (/) /\ -. E. x e. On ( rank ` ( A u. B ) ) = suc x ) -> Lim ( rank ` ( A u. B ) ) )
95 90 94 sylan 
 |-  ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. E. x e. On ( rank ` ( A u. B ) ) = suc x ) -> Lim ( rank ` ( A u. B ) ) )
96 95 ex 
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( -. E. x e. On ( rank ` ( A u. B ) ) = suc x -> Lim ( rank ` ( A u. B ) ) ) )
97 ordzsl 
 |-  ( Ord ( rank ` ( A X. B ) ) <-> ( ( rank ` ( A X. B ) ) = (/) \/ E. y e. On ( rank ` ( A X. B ) ) = suc y \/ Lim ( rank ` ( A X. B ) ) ) )
98 52 97 mpbi 
 |-  ( ( rank ` ( A X. B ) ) = (/) \/ E. y e. On ( rank ` ( A X. B ) ) = suc y \/ Lim ( rank ` ( A X. B ) ) )
99 98 3ori 
 |-  ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. E. y e. On ( rank ` ( A X. B ) ) = suc y ) -> Lim ( rank ` ( A X. B ) ) )
100 99 ex 
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( -. E. y e. On ( rank ` ( A X. B ) ) = suc y -> Lim ( rank ` ( A X. B ) ) ) )
101 96 100 orim12d 
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( ( -. E. x e. On ( rank ` ( A u. B ) ) = suc x \/ -. E. y e. On ( rank ` ( A X. B ) ) = suc y ) -> ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) ) )
102 79 101 biimtrid 
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) -> ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) ) )
103 102 imp 
 |-  ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) ) -> ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) )
104 simpl 
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ -. ( rank ` ( A X. B ) ) = (/) ) -> Lim ( rank ` ( A u. B ) ) )
105 30 necon3abii 
 |-  ( ( A X. B ) =/= (/) <-> -. ( rank ` ( A X. B ) ) = (/) )
106 1 2 rankxplim 
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ ( A X. B ) =/= (/) ) -> ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) )
107 105 106 sylan2br 
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ -. ( rank ` ( A X. B ) ) = (/) ) -> ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) )
108 limeq 
 |-  ( ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) -> ( Lim ( rank ` ( A X. B ) ) <-> Lim ( rank ` ( A u. B ) ) ) )
109 107 108 syl 
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ -. ( rank ` ( A X. B ) ) = (/) ) -> ( Lim ( rank ` ( A X. B ) ) <-> Lim ( rank ` ( A u. B ) ) ) )
110 104 109 mpbird 
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ -. ( rank ` ( A X. B ) ) = (/) ) -> Lim ( rank ` ( A X. B ) ) )
111 110 expcom 
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( Lim ( rank ` ( A u. B ) ) -> Lim ( rank ` ( A X. B ) ) ) )
112 idd 
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( Lim ( rank ` ( A X. B ) ) -> Lim ( rank ` ( A X. B ) ) ) )
113 111 112 jaod 
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) -> Lim ( rank ` ( A X. B ) ) ) )
114 113 adantr 
 |-  ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) ) -> ( ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) -> Lim ( rank ` ( A X. B ) ) ) )
115 103 114 mpd 
 |-  ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) ) -> Lim ( rank ` ( A X. B ) ) )
116 10 78 115 syl2anc 
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> Lim ( rank ` ( A X. B ) ) )
117 3 116 impbii 
 |-  ( Lim ( rank ` ( A X. B ) ) <-> Lim U. ( rank ` ( A X. B ) ) )